|
33010
|
1 |
#2 := false
|
|
|
2 |
decl uf_1 :: int
|
|
|
3 |
#5 := uf_1
|
|
|
4 |
#7 := 2::int
|
|
|
5 |
#29 := (* 2::int uf_1)
|
|
|
6 |
#4 := 0::int
|
|
|
7 |
#54 := (= 0::int #29)
|
|
|
8 |
#55 := (not #54)
|
|
|
9 |
#61 := (= #29 0::int)
|
|
|
10 |
#104 := (not #61)
|
|
|
11 |
#110 := (iff #104 #55)
|
|
|
12 |
#108 := (iff #61 #54)
|
|
|
13 |
#109 := [commutativity]: #108
|
|
|
14 |
#111 := [monotonicity #109]: #110
|
|
|
15 |
#62 := (<= #29 0::int)
|
|
|
16 |
#100 := (not #62)
|
|
|
17 |
#30 := (<= uf_1 0::int)
|
|
|
18 |
#31 := (not #30)
|
|
|
19 |
#6 := (< 0::int uf_1)
|
|
|
20 |
#32 := (iff #6 #31)
|
|
|
21 |
#33 := [rewrite]: #32
|
|
|
22 |
#27 := [asserted]: #6
|
|
|
23 |
#34 := [mp #27 #33]: #31
|
|
|
24 |
#101 := (or #100 #30)
|
|
|
25 |
#102 := [th-lemma]: #101
|
|
|
26 |
#103 := [unit-resolution #102 #34]: #100
|
|
|
27 |
#105 := (or #104 #62)
|
|
|
28 |
#106 := [th-lemma]: #105
|
|
|
29 |
#107 := [unit-resolution #106 #103]: #104
|
|
|
30 |
#112 := [mp #107 #111]: #55
|
|
|
31 |
#56 := (= uf_1 #29)
|
|
|
32 |
#57 := (not #56)
|
|
|
33 |
#53 := (= 0::int uf_1)
|
|
|
34 |
#50 := (not #53)
|
|
|
35 |
#58 := (and #50 #55 #57)
|
|
|
36 |
#69 := (not #58)
|
|
|
37 |
#42 := (distinct 0::int uf_1 #29)
|
|
|
38 |
#47 := (not #42)
|
|
|
39 |
#9 := (- uf_1 uf_1)
|
|
|
40 |
#8 := (* uf_1 2::int)
|
|
|
41 |
#10 := (distinct uf_1 #8 #9)
|
|
|
42 |
#11 := (not #10)
|
|
|
43 |
#48 := (iff #11 #47)
|
|
|
44 |
#45 := (iff #10 #42)
|
|
|
45 |
#39 := (distinct uf_1 #29 0::int)
|
|
|
46 |
#43 := (iff #39 #42)
|
|
|
47 |
#44 := [rewrite]: #43
|
|
|
48 |
#40 := (iff #10 #39)
|
|
|
49 |
#37 := (= #9 0::int)
|
|
|
50 |
#38 := [rewrite]: #37
|
|
|
51 |
#35 := (= #8 #29)
|
|
|
52 |
#36 := [rewrite]: #35
|
|
|
53 |
#41 := [monotonicity #36 #38]: #40
|
|
|
54 |
#46 := [trans #41 #44]: #45
|
|
|
55 |
#49 := [monotonicity #46]: #48
|
|
|
56 |
#28 := [asserted]: #11
|
|
|
57 |
#52 := [mp #28 #49]: #47
|
|
|
58 |
#80 := (or #42 #69)
|
|
|
59 |
#81 := [def-axiom]: #80
|
|
|
60 |
#82 := [unit-resolution #81 #52]: #69
|
|
|
61 |
#59 := (= uf_1 0::int)
|
|
|
62 |
#83 := (not #59)
|
|
|
63 |
#89 := (iff #83 #50)
|
|
|
64 |
#87 := (iff #59 #53)
|
|
|
65 |
#88 := [commutativity]: #87
|
|
|
66 |
#90 := [monotonicity #88]: #89
|
|
|
67 |
#84 := (or #83 #30)
|
|
|
68 |
#85 := [th-lemma]: #84
|
|
|
69 |
#86 := [unit-resolution #85 #34]: #83
|
|
|
70 |
#91 := [mp #86 #90]: #50
|
|
|
71 |
#64 := -1::int
|
|
|
72 |
#65 := (* -1::int #29)
|
|
|
73 |
#66 := (+ uf_1 #65)
|
|
|
74 |
#68 := (>= #66 0::int)
|
|
|
75 |
#92 := (not #68)
|
|
|
76 |
#93 := (or #92 #30)
|
|
|
77 |
#94 := [th-lemma]: #93
|
|
|
78 |
#95 := [unit-resolution #94 #34]: #92
|
|
|
79 |
#96 := (or #57 #68)
|
|
|
80 |
#97 := [th-lemma]: #96
|
|
|
81 |
#98 := [unit-resolution #97 #95]: #57
|
|
|
82 |
#76 := (or #58 #53 #54 #56)
|
|
|
83 |
#77 := [def-axiom]: #76
|
|
|
84 |
#99 := [unit-resolution #77 #98 #91 #82]: #54
|
|
|
85 |
[unit-resolution #99 #112]: false
|
|
|
86 |
unsat
|