mirror of
https://github.com/Z3Prover/z3
synced 2025-04-17 06:15:37 +00:00
1207 lines
33 KiB
Plaintext
1207 lines
33 KiB
Plaintext
[tool-version] Z3 4.12.3
|
|
[mk-app] #1 true
|
|
[mk-app] #2 false
|
|
[mk-app] #1 true
|
|
[mk-app] #2 false
|
|
[mk-app] #3 pi
|
|
[mk-app] #4 euler
|
|
[mk-var] datatype#0 0
|
|
[mk-var] datatype#1 1
|
|
[mk-app] datatype#2 insert datatype#0 datatype#1
|
|
[mk-app] datatype#3 pattern datatype#2
|
|
[mk-app] datatype#4 head datatype#2
|
|
[mk-app] datatype#5 = datatype#0 datatype#4
|
|
[mk-quant] datatype#6 constructor_accessor_axiom 2 datatype#3 datatype#5
|
|
[attach-var-names] datatype#6 (;k!0) (;List)
|
|
[mk-app] datatype#7 tail datatype#2
|
|
[mk-app] datatype#8 = datatype#1 datatype#7
|
|
[mk-quant] datatype#9 constructor_accessor_axiom 2 datatype#3 datatype#8
|
|
[attach-var-names] datatype#9 (;k!0) (;List)
|
|
[mk-app] #5 bv
|
|
[attach-meaning] #5 bv #b1
|
|
[mk-app] #6 bv
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #6 bv #b0
|
|
[mk-var] #7 0
|
|
[mk-var] #8 1
|
|
[mk-var] #9 2
|
|
[mk-var] #10 3
|
|
[mk-var] #11 4
|
|
[mk-var] #12 5
|
|
[mk-var] #13 6
|
|
[mk-var] #14 7
|
|
[mk-var] #15 8
|
|
[mk-var] #16 9
|
|
[mk-var] #17 10
|
|
[mk-var] #18 11
|
|
[mk-var] #19 12
|
|
[mk-var] #20 13
|
|
[mk-var] #21 14
|
|
[mk-app] #22 + #15 #13
|
|
[attach-enode] #1 0
|
|
[attach-enode] #2 0
|
|
[mk-app] #23 Int
|
|
[attach-meaning] #23 arith 0
|
|
[mk-app] #24 d
|
|
[mk-app] #25 to_real #23
|
|
[mk-app] #26 = #25 #24
|
|
[mk-app] #27 not #26
|
|
[mk-app] #28 Real
|
|
[attach-meaning] #28 arith 0
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #25
|
|
[mk-app] #29 = #25 #28
|
|
[instance] 0000000000000000 #29
|
|
[attach-enode] #29 0
|
|
[end-of-instance]
|
|
[mk-app] #29 Real
|
|
[attach-meaning] #29 arith (- 1)
|
|
[mk-app] #30 * #29 #24
|
|
[mk-app] #31 = #24 #28
|
|
[mk-app] #29 = #28 #24
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #29
|
|
[mk-app] #30 = #29 #31
|
|
[instance] 0000000000000000 #30
|
|
[attach-enode] #30 0
|
|
[end-of-instance]
|
|
[mk-app] #29 not #31
|
|
[mk-app] #30 c
|
|
[mk-app] #32 f
|
|
[mk-app] #33 = #30 #32
|
|
[mk-app] #34 b
|
|
[mk-app] #35 g
|
|
[mk-app] #36 to_int #34
|
|
[mk-app] #37 to_int #35
|
|
[mk-app] #38 mod #36 #37
|
|
[mk-app] #39 e
|
|
[mk-app] #40 to_real #38
|
|
[mk-app] #41 * #40 #39
|
|
[mk-app] #42 + #41
|
|
[mk-app] #43 * #42
|
|
[mk-app] #44 a
|
|
[mk-app] #45 < #43 #28
|
|
[mk-app] #46 < #28 #39
|
|
[mk-app] #47 < #39 #44
|
|
[mk-app] #48 and #45 #46 #47
|
|
[mk-app] #49 <= #28 #34
|
|
[mk-app] #50 <= #34 #35
|
|
[mk-app] #51 and #49 #50
|
|
[mk-app] #52 and #33 #48 #51
|
|
[mk-app] #53 to_int #32
|
|
[mk-app] #54 mod #36 #53
|
|
[mk-app] #55 to_real #54
|
|
[mk-app] #56 + #39 #55
|
|
[mk-app] #57 * #56
|
|
[mk-app] #58 < #25 #57
|
|
[mk-app] #59 < #57 #25
|
|
[mk-app] #60 and #58 #59
|
|
[mk-app] #61 = #52 #60
|
|
[mk-app] #62 not #61
|
|
[mk-app] #63 * #39 #40
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #41
|
|
[mk-app] #64 = #41 #63
|
|
[instance] 0000000000000000 #64
|
|
[attach-enode] #64 0
|
|
[end-of-instance]
|
|
[mk-app] #64 + #63
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #64
|
|
[mk-app] #65 = #64 #63
|
|
[instance] 0000000000000000 #65
|
|
[attach-enode] #65 0
|
|
[end-of-instance]
|
|
[mk-app] #64 * #63
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #64
|
|
[mk-app] #65 = #64 #63
|
|
[instance] 0000000000000000 #65
|
|
[attach-enode] #65 0
|
|
[end-of-instance]
|
|
[mk-app] #64 <= #28 #63
|
|
[mk-app] #65 not #64
|
|
[mk-app] #66 < #63 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #66
|
|
[mk-app] #67 = #66 #65
|
|
[instance] 0000000000000000 #67
|
|
[attach-enode] #67 0
|
|
[end-of-instance]
|
|
[mk-app] #66 Real
|
|
[attach-meaning] #66 arith (- 1)
|
|
[mk-app] #67 * #66 #63
|
|
[mk-app] #68 >= #63 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #64
|
|
[mk-app] #66 = #64 #68
|
|
[instance] 0000000000000000 #66
|
|
[attach-enode] #66 0
|
|
[end-of-instance]
|
|
[mk-app] #66 not #68
|
|
[mk-app] #67 <= #39 #28
|
|
[mk-app] #69 not #67
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #46
|
|
[mk-app] #70 = #46 #69
|
|
[instance] 0000000000000000 #70
|
|
[attach-enode] #70 0
|
|
[end-of-instance]
|
|
[mk-app] #70 <= #44 #39
|
|
[mk-app] #71 not #70
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #47
|
|
[mk-app] #72 = #47 #71
|
|
[instance] 0000000000000000 #72
|
|
[attach-enode] #72 0
|
|
[end-of-instance]
|
|
[mk-app] #72 Real
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #73 * #72 #39
|
|
[mk-app] #74 + #73 #44
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #75 * #72 #44
|
|
[mk-app] #76 + #39 #75
|
|
[mk-app] #73 >= #76 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #70
|
|
[mk-app] #74 = #70 #73
|
|
[instance] 0000000000000000 #74
|
|
[attach-enode] #74 0
|
|
[end-of-instance]
|
|
[mk-app] #74 not #73
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #77 * #72 #34
|
|
[mk-app] #78 >= #34 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #49
|
|
[mk-app] #77 = #49 #78
|
|
[instance] 0000000000000000 #77
|
|
[attach-enode] #77 0
|
|
[end-of-instance]
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #77 * #72 #35
|
|
[mk-app] #79 + #34 #77
|
|
[mk-app] #80 <= #79 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #50
|
|
[mk-app] #81 = #50 #80
|
|
[instance] 0000000000000000 #81
|
|
[attach-enode] #81 0
|
|
[end-of-instance]
|
|
[mk-app] #81 and #33 #66 #69 #74 #78 #80
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #25
|
|
[mk-app] #82 = #25 #28
|
|
[instance] 0000000000000000 #82
|
|
[attach-enode] #82 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #57
|
|
[mk-app] #82 = #57 #56
|
|
[instance] 0000000000000000 #82
|
|
[attach-enode] #82 0
|
|
[end-of-instance]
|
|
[mk-app] #82 <= #56 #28
|
|
[mk-app] #83 not #82
|
|
[mk-app] #84 < #28 #56
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #84
|
|
[mk-app] #85 = #84 #83
|
|
[instance] 0000000000000000 #85
|
|
[attach-enode] #85 0
|
|
[end-of-instance]
|
|
[mk-app] #84 <= #28 #56
|
|
[mk-app] #85 not #84
|
|
[mk-app] #86 < #56 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #86
|
|
[mk-app] #87 = #86 #85
|
|
[instance] 0000000000000000 #87
|
|
[attach-enode] #87 0
|
|
[end-of-instance]
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #86 * #72 #39
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #87 * #72 #55
|
|
[mk-app] #88 + #86 #87
|
|
[mk-app] #86 >= #56 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #84
|
|
[mk-app] #87 = #84 #86
|
|
[instance] 0000000000000000 #87
|
|
[attach-enode] #87 0
|
|
[end-of-instance]
|
|
[mk-app] #87 not #86
|
|
[mk-app] #88 and #83 #87
|
|
[mk-app] #89 = #81 #88
|
|
[mk-app] #90 not #81
|
|
[mk-app] #91 not #89
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #91
|
|
[mk-app] #90 = #91 #91
|
|
[instance] 0000000000000000 #90
|
|
[attach-enode] #90 0
|
|
[end-of-instance]
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #25
|
|
[mk-app] #90 = #25 #28
|
|
[instance] 0000000000000000 #90
|
|
[attach-enode] #90 0
|
|
[end-of-instance]
|
|
[mk-app] #90 = #28 #24
|
|
[mk-app] #92 not #90
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #41
|
|
[mk-app] #93 = #41 #63
|
|
[instance] 0000000000000000 #93
|
|
[attach-enode] #93 0
|
|
[end-of-instance]
|
|
[mk-app] #93 + #63
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #93
|
|
[mk-app] #94 = #93 #63
|
|
[instance] 0000000000000000 #94
|
|
[attach-enode] #94 0
|
|
[end-of-instance]
|
|
[mk-app] #93 * #63
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #93
|
|
[mk-app] #94 = #93 #63
|
|
[instance] 0000000000000000 #94
|
|
[attach-enode] #94 0
|
|
[end-of-instance]
|
|
[mk-app] #93 < #63 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #93
|
|
[mk-app] #94 = #93 #65
|
|
[instance] 0000000000000000 #94
|
|
[attach-enode] #94 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #46
|
|
[mk-app] #93 = #46 #69
|
|
[instance] 0000000000000000 #93
|
|
[attach-enode] #93 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #47
|
|
[mk-app] #93 = #47 #71
|
|
[instance] 0000000000000000 #93
|
|
[attach-enode] #93 0
|
|
[end-of-instance]
|
|
[mk-app] #93 and #33 #65 #69 #71 #49 #50
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #57
|
|
[mk-app] #94 = #57 #56
|
|
[instance] 0000000000000000 #94
|
|
[attach-enode] #94 0
|
|
[end-of-instance]
|
|
[mk-app] #94 < #28 #56
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #94
|
|
[mk-app] #95 = #94 #83
|
|
[instance] 0000000000000000 #95
|
|
[attach-enode] #95 0
|
|
[end-of-instance]
|
|
[mk-app] #94 < #56 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #94
|
|
[mk-app] #95 = #94 #85
|
|
[instance] 0000000000000000 #95
|
|
[attach-enode] #95 0
|
|
[end-of-instance]
|
|
[mk-app] #94 and #83 #85
|
|
[mk-app] #95 = #93 #94
|
|
[mk-app] #96 not #93
|
|
[mk-app] #97 not #95
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #97
|
|
[mk-app] #96 = #97 #97
|
|
[instance] 0000000000000000 #96
|
|
[attach-enode] #96 0
|
|
[end-of-instance]
|
|
[mk-app] #96 not #93
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #97
|
|
[mk-app] #96 = #97 #97
|
|
[instance] 0000000000000000 #96
|
|
[attach-enode] #96 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #56
|
|
[mk-app] #96 = #56 #56
|
|
[instance] 0000000000000000 #96
|
|
[attach-enode] #96 0
|
|
[end-of-instance]
|
|
[mk-app] #96 not #93
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #97
|
|
[mk-app] #96 = #97 #97
|
|
[instance] 0000000000000000 #96
|
|
[attach-enode] #96 0
|
|
[end-of-instance]
|
|
[mk-app] #96 Real
|
|
[attach-meaning] #96 arith 1
|
|
[mk-app] #98 + #28 #96
|
|
[mk-app] #99 k!0
|
|
[mk-app] #100 if #99 #28 #98
|
|
[mk-app] #101 not #99
|
|
[mk-app] #92 + #32 #96
|
|
[mk-app] #102 k!1
|
|
[mk-app] #103 if #102 #32 #92
|
|
[mk-app] #104 k!2
|
|
[mk-app] #105 + #39 #96
|
|
[mk-app] #106 if #104 #39 #105
|
|
[mk-app] #107 not #104
|
|
[mk-app] #108 and #102 #65 #69 #107 #49 #50
|
|
[mk-app] #109 = #108 #94
|
|
[mk-app] #110 not #109
|
|
[mk-app] #93 k!3
|
|
[mk-app] #95 not #93
|
|
[mk-app] #97 k!4
|
|
[mk-app] #111 not #97
|
|
[mk-app] #112 and #102 #65 #69 #97 #49 #50
|
|
[mk-app] #113 = #112 #94
|
|
[mk-app] #114 not #113
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-enode] #1 0
|
|
[attach-enode] #2 0
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #107 * #72 #63
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #64
|
|
[mk-app] #107 = #64 #68
|
|
[instance] 0000000000000000 #107
|
|
[attach-enode] #107 0
|
|
[end-of-instance]
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #107 * #72 #34
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #49
|
|
[mk-app] #107 = #49 #78
|
|
[instance] 0000000000000000 #107
|
|
[attach-enode] #107 0
|
|
[end-of-instance]
|
|
[attach-meaning] #72 arith (- 1)
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #50
|
|
[mk-app] #107 = #50 #80
|
|
[instance] 0000000000000000 #107
|
|
[attach-enode] #107 0
|
|
[end-of-instance]
|
|
[mk-app] #107 and #102 #66 #69 #97 #78 #80
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #101 * #72 #39
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #90 * #72 #55
|
|
[mk-app] #108 + #101 #90
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #84
|
|
[mk-app] #101 = #84 #86
|
|
[instance] 0000000000000000 #101
|
|
[attach-enode] #101 0
|
|
[end-of-instance]
|
|
[mk-app] #101 = #107 #88
|
|
[mk-app] #90 not #107
|
|
[mk-app] #108 not #101
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #108
|
|
[mk-app] #90 = #108 #108
|
|
[instance] 0000000000000000 #90
|
|
[attach-enode] #90 0
|
|
[end-of-instance]
|
|
[begin-check] 0
|
|
[mk-app] #90 Int
|
|
[attach-meaning] #90 arith 1
|
|
[attach-enode] #90 0
|
|
[attach-enode] #96 0
|
|
[attach-enode] #23 0
|
|
[attach-enode] #28 0
|
|
[mk-app] #109 not #107
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #108
|
|
[mk-app] #109 = #108 #108
|
|
[instance] 0000000000000000 #109
|
|
[attach-enode] #109 0
|
|
[end-of-instance]
|
|
[mk-app] #109 not #107
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #108
|
|
[mk-app] #109 = #108 #108
|
|
[instance] 0000000000000000 #109
|
|
[attach-enode] #109 0
|
|
[end-of-instance]
|
|
[mk-app] #109 not #107
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #108
|
|
[mk-app] #109 = #108 #108
|
|
[instance] 0000000000000000 #109
|
|
[attach-enode] #109 0
|
|
[end-of-instance]
|
|
[mk-app] #109 not #102
|
|
[mk-app] #110 not #78
|
|
[mk-app] #115 not #80
|
|
[mk-app] #116 or #67 #68 #109 #110 #111 #115
|
|
[mk-app] #117 not #116
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #107
|
|
[mk-app] #118 = #107 #117
|
|
[instance] 0000000000000000 #118
|
|
[attach-enode] #118 0
|
|
[end-of-instance]
|
|
[mk-app] #118 or #82 #86
|
|
[mk-app] #119 not #118
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #88
|
|
[mk-app] #120 = #88 #119
|
|
[instance] 0000000000000000 #120
|
|
[attach-enode] #120 0
|
|
[end-of-instance]
|
|
[mk-app] #120 = #116 #118
|
|
[mk-app] #121 = #117 #119
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #121
|
|
[mk-app] #122 = #121 #120
|
|
[instance] 0000000000000000 #122
|
|
[attach-enode] #122 0
|
|
[end-of-instance]
|
|
[mk-app] #117 not #116
|
|
[mk-app] #121 not #120
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #121
|
|
[mk-app] #117 = #121 #121
|
|
[instance] 0000000000000000 #117
|
|
[attach-enode] #117 0
|
|
[end-of-instance]
|
|
[mk-app] #107 not #116
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #121
|
|
[mk-app] #107 = #121 #121
|
|
[instance] 0000000000000000 #107
|
|
[attach-enode] #107 0
|
|
[end-of-instance]
|
|
[mk-app] #107 not #116
|
|
[inst-discovered] theory-solving 0000000000000000 basic# ; #121
|
|
[mk-app] #107 = #121 #121
|
|
[instance] 0000000000000000 #107
|
|
[attach-enode] #107 0
|
|
[end-of-instance]
|
|
[assign] #93 justification -1:
|
|
[attach-enode] #39 0
|
|
[attach-enode] #34 0
|
|
[attach-enode] #36 0
|
|
[attach-enode] #35 0
|
|
[attach-enode] #37 0
|
|
[attach-enode] #38 0
|
|
[mk-app] #119 mod #36 #23
|
|
[mk-app] #107 mod0 #36 #23
|
|
[mk-app] #101 = #107 #119
|
|
[attach-enode] #107 0
|
|
[attach-enode] #119 0
|
|
[attach-enode] #101 0
|
|
[mk-app] #108 Int
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #117 * #108 #119
|
|
[mk-app] #122 + #107 #117
|
|
[mk-app] #123 <= #122 #23
|
|
[mk-app] #124 >= #122 #23
|
|
[attach-enode] #108 0
|
|
[attach-enode] #117 0
|
|
[attach-enode] #122 0
|
|
[mk-app] #125 to_real #36
|
|
[mk-app] #126 - #125 #34
|
|
[mk-app] #127 <= #126 #28
|
|
[mk-app] #128 - #34 #125
|
|
[mk-app] #129 >= #128 #96
|
|
[attach-enode] #125 0
|
|
[attach-enode] #126 0
|
|
[attach-enode] #127 0
|
|
[attach-enode] #128 0
|
|
[attach-enode] #129 0
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #127
|
|
[assign] #127 justification -1: 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #129
|
|
[assign] (not #129) justification -1: 0
|
|
[end-of-instance]
|
|
[assign] #101 axiom
|
|
[attach-enode] #40 0
|
|
[attach-enode] #63 0
|
|
[attach-enode] #72 0
|
|
[attach-enode] #77 0
|
|
[attach-enode] #79 0
|
|
[attach-enode] #32 0
|
|
[attach-enode] #53 0
|
|
[attach-enode] #54 0
|
|
[attach-enode] #55 0
|
|
[attach-enode] #56 0
|
|
[assign] (not #120) justification -1:
|
|
[assign] #124 bin 4
|
|
[assign] #123 bin 4
|
|
[mk-app] #130 = #122 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #130
|
|
[end-of-instance]
|
|
[push] 0
|
|
[assign] (not #86) decision axiom
|
|
[assign] #82 bin -15
|
|
[assign] #118 bin 14
|
|
[assign] (not #116) clause -13 -16
|
|
[assign] #80 bin -13
|
|
[assign] #97 bin -13
|
|
[assign] #78 bin -13
|
|
[assign] #102 bin -13
|
|
[assign] (not #68) bin -13
|
|
[assign] (not #67) bin -13
|
|
[mk-app] #130 div #36 #53
|
|
[mk-app] #131 * #53 #130
|
|
[mk-app] #132 + #131 #54
|
|
[mk-app] #133 = #36 #132
|
|
[attach-enode] #130 0
|
|
[mk-app] #134 div0 #36 #53
|
|
[mk-app] #135 = #130 #134
|
|
[attach-enode] #134 0
|
|
[attach-enode] #135 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #136 * #108 #134
|
|
[mk-app] #137 + #130 #136
|
|
[mk-app] #138 <= #137 #23
|
|
[mk-app] #139 >= #137 #23
|
|
[attach-enode] #136 0
|
|
[attach-enode] #137 0
|
|
[assign] #135 axiom
|
|
[attach-enode] #131 0
|
|
[attach-enode] #132 0
|
|
[attach-enode] #133 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #140 * #108 #132
|
|
[mk-app] #141 + #36 #140
|
|
[mk-app] #142 <= #141 #23
|
|
[mk-app] #143 >= #141 #23
|
|
[attach-enode] #140 0
|
|
[attach-enode] #141 0
|
|
[mk-app] #144 - #53
|
|
[mk-app] #145 >= #53 #23
|
|
[mk-app] #146 if #145 #53 #144
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #147 - #54 #146
|
|
[mk-app] #148 = #53 #23
|
|
[attach-enode] #148 0
|
|
[mk-app] #149 = #23 #53
|
|
[mk-app] #150 <= #53 #23
|
|
[attach-enode] #149 0
|
|
[mk-app] #151 >= #54 #23
|
|
[attach-enode] #151 0
|
|
[mk-app] #152 <= #147 #108
|
|
[attach-enode] #145 0
|
|
[attach-enode] #144 0
|
|
[mk-app] #153 = #53 #146
|
|
[mk-app] #154 = #144 #146
|
|
[attach-enode] #146 0
|
|
[attach-enode] #153 0
|
|
[attach-enode] #154 0
|
|
[attach-enode] #147 0
|
|
[attach-enode] #152 0
|
|
[mk-app] #155 - #36 #131
|
|
[mk-app] #156 >= #155 #23
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #157 * #108 #131
|
|
[mk-app] #158 + #36 #157
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #155
|
|
[mk-app] #159 = #155 #158
|
|
[instance] 0000000000000000 #159
|
|
[attach-enode] #159 0
|
|
[end-of-instance]
|
|
[mk-app] #159 >= #158 #23
|
|
[attach-enode] #157 0
|
|
[attach-enode] #158 0
|
|
[attach-enode] #159 0
|
|
[mk-app] #155 div #36 #37
|
|
[mk-app] #156 * #37 #155
|
|
[mk-app] #160 + #156 #38
|
|
[mk-app] #161 = #36 #160
|
|
[attach-enode] #155 0
|
|
[mk-app] #162 div0 #36 #37
|
|
[mk-app] #163 = #155 #162
|
|
[attach-enode] #162 0
|
|
[attach-enode] #163 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #164 * #108 #162
|
|
[mk-app] #165 + #155 #164
|
|
[mk-app] #166 <= #165 #23
|
|
[mk-app] #167 >= #165 #23
|
|
[attach-enode] #164 0
|
|
[attach-enode] #165 0
|
|
[assign] #163 axiom
|
|
[attach-enode] #156 0
|
|
[attach-enode] #160 0
|
|
[attach-enode] #161 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #168 * #108 #160
|
|
[mk-app] #169 + #36 #168
|
|
[mk-app] #170 <= #169 #23
|
|
[mk-app] #171 >= #169 #23
|
|
[attach-enode] #168 0
|
|
[attach-enode] #169 0
|
|
[mk-app] #172 - #37
|
|
[mk-app] #173 >= #37 #23
|
|
[mk-app] #174 if #173 #37 #172
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #175 - #38 #174
|
|
[mk-app] #176 = #37 #23
|
|
[attach-enode] #176 0
|
|
[mk-app] #177 = #23 #37
|
|
[mk-app] #178 <= #37 #23
|
|
[attach-enode] #177 0
|
|
[mk-app] #179 >= #38 #23
|
|
[attach-enode] #179 0
|
|
[mk-app] #180 <= #175 #108
|
|
[attach-enode] #173 0
|
|
[attach-enode] #172 0
|
|
[mk-app] #181 = #37 #174
|
|
[mk-app] #182 = #172 #174
|
|
[attach-enode] #174 0
|
|
[attach-enode] #181 0
|
|
[attach-enode] #182 0
|
|
[attach-enode] #175 0
|
|
[attach-enode] #180 0
|
|
[mk-app] #183 - #36 #156
|
|
[mk-app] #184 >= #183 #23
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #185 * #108 #156
|
|
[mk-app] #186 + #36 #185
|
|
[inst-discovered] theory-solving 0000000000000000 arith# ; #183
|
|
[mk-app] #187 = #183 #186
|
|
[instance] 0000000000000000 #187
|
|
[attach-enode] #187 0
|
|
[end-of-instance]
|
|
[mk-app] #187 >= #186 #23
|
|
[attach-enode] #185 0
|
|
[attach-enode] #186 0
|
|
[attach-enode] #187 0
|
|
[mk-app] #183 to_real #53
|
|
[mk-app] #184 - #183 #32
|
|
[mk-app] #188 <= #184 #28
|
|
[mk-app] #189 - #32 #183
|
|
[mk-app] #190 >= #189 #96
|
|
[attach-enode] #183 0
|
|
[attach-enode] #184 0
|
|
[attach-enode] #188 0
|
|
[attach-enode] #189 0
|
|
[attach-enode] #190 0
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #188
|
|
[assign] #188 justification -1: 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #190
|
|
[assign] (not #190) justification -1: 0
|
|
[end-of-instance]
|
|
[mk-app] #191 to_real #37
|
|
[mk-app] #192 - #191 #35
|
|
[mk-app] #193 <= #192 #28
|
|
[mk-app] #194 - #35 #191
|
|
[mk-app] #195 >= #194 #96
|
|
[attach-enode] #191 0
|
|
[attach-enode] #192 0
|
|
[attach-enode] #193 0
|
|
[attach-enode] #194 0
|
|
[attach-enode] #195 0
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #193
|
|
[assign] #193 justification -1: 0
|
|
[end-of-instance]
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #195
|
|
[assign] (not #195) justification -1: 0
|
|
[end-of-instance]
|
|
[assign] (not #151) clause -28 -14 2
|
|
[assign] #138 clause 19 -18
|
|
[assign] #139 clause 20 -18
|
|
[assign] #166 clause 34 -33
|
|
[assign] #167 clause 35 -33
|
|
[assign] #148 clause 24 28
|
|
[assign] #149 justification -1: 24
|
|
[mk-app] #196 = #54 #119
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #197 + #54 #117
|
|
[mk-app] #198 <= #197 #23
|
|
[mk-app] #199 >= #197 #23
|
|
[assign] #196 justification -1: 24
|
|
[attach-enode] #196 0
|
|
[attach-enode] #197 0
|
|
[assign] #198 justification -1: 52
|
|
[assign] #199 justification -1: 52
|
|
[mk-app] #200 = #137 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[mk-app] #200 = #165 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[assign] #150 clause 26 -25
|
|
[assign] #145 clause 27 -25
|
|
[assign] #153 clause 30 -27
|
|
[mk-app] #200 = #197 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[mk-app] #200 = #23 #144
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[mk-app] #200 = #28 #183
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[mk-app] #200 = #32 #189
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[assign] #154 justification -1: 30 24 26 27
|
|
[push] 1
|
|
[assign] (not #179) decision axiom
|
|
[assign] #176 clause 39 43
|
|
[assign] #177 justification -1: 39
|
|
[mk-app] #200 = #38 #119
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #201 + #38 #117
|
|
[mk-app] #202 <= #201 #23
|
|
[mk-app] #203 >= #201 #23
|
|
[assign] #200 justification -1: 39
|
|
[attach-enode] #200 0
|
|
[attach-enode] #201 0
|
|
[assign] #202 justification -1: 55
|
|
[assign] #203 justification -1: 55
|
|
[mk-app] #204 = #130 #155
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #205 * #108 #155
|
|
[mk-app] #206 + #130 #205
|
|
[mk-app] #207 <= #206 #23
|
|
[mk-app] #208 >= #206 #23
|
|
[assign] #204 justification -1: 39 24
|
|
[attach-enode] #204 0
|
|
[attach-enode] #205 0
|
|
[attach-enode] #206 0
|
|
[assign] #207 justification -1: 58
|
|
[assign] #208 justification -1: 58
|
|
[mk-app] #209 = #144 #172
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #210 * #108 #172
|
|
[mk-app] #211 + #144 #210
|
|
[mk-app] #212 <= #211 #23
|
|
[mk-app] #213 >= #211 #23
|
|
[assign] #209 justification -1: 39 24
|
|
[attach-enode] #209 0
|
|
[attach-enode] #210 0
|
|
[attach-enode] #211 0
|
|
[assign] #212 justification -1: 61
|
|
[assign] #213 justification -1: 61
|
|
[mk-app] #214 = #183 #191
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #215 * #72 #191
|
|
[mk-app] #216 + #183 #215
|
|
[mk-app] #217 <= #216 #28
|
|
[mk-app] #218 >= #216 #28
|
|
[assign] #214 justification -1: 39 24
|
|
[attach-enode] #214 0
|
|
[attach-enode] #215 0
|
|
[attach-enode] #216 0
|
|
[assign] #217 justification -1: 64
|
|
[assign] #218 justification -1: 64
|
|
[mk-app] #219 = #40 #55
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #220 * #72 #55
|
|
[mk-app] #221 + #40 #220
|
|
[mk-app] #222 <= #221 #28
|
|
[mk-app] #223 >= #221 #28
|
|
[assign] #219 justification -1: 24 39
|
|
[attach-enode] #219 0
|
|
[attach-enode] #220 0
|
|
[attach-enode] #221 0
|
|
[assign] #222 justification -1: 67
|
|
[assign] #223 justification -1: 67
|
|
[assign] #178 clause 41 -40
|
|
[assign] #173 clause 42 -40
|
|
[assign] #181 clause 45 -42
|
|
[mk-app] #224 = #201 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #206 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #211 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #216 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #221 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #35 #194
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[push] 2
|
|
[assign] (not #152) decision axiom
|
|
[push] 3
|
|
[assign] (not #143) decision axiom
|
|
[assign] #142 clause 22 23
|
|
[assign] (not #133) clause -21 23
|
|
[assign] (not #159) clause -32 23 -14 2
|
|
[push] 4
|
|
[assign] (not #182) decision axiom
|
|
[push] 5
|
|
[assign] (not #187) decision axiom
|
|
[push] 6
|
|
[assign] (not #171) decision axiom
|
|
[assign] #170 clause 37 38
|
|
[assign] (not #161) clause -36 38
|
|
[push] 7
|
|
[assign] (not #180) decision axiom
|
|
[mk-app] #224 = #36 #197
|
|
[attach-enode] #224 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #225 * #108 #197
|
|
[mk-app] #226 + #36 #225
|
|
[mk-app] #227 <= #226 #23
|
|
[mk-app] #228 >= #226 #23
|
|
[attach-enode] #225 0
|
|
[attach-enode] #226 0
|
|
[push] 8
|
|
[assign] #224 decision axiom
|
|
[assign] #227 clause 71 -70
|
|
[assign] #228 clause 72 -70
|
|
[mk-app] #229 = #125 #183
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #230 * #72 #183
|
|
[mk-app] #231 + #125 #230
|
|
[mk-app] #232 <= #231 #28
|
|
[mk-app] #233 >= #231 #28
|
|
[assign] #229 justification -1: 70 24 54 53
|
|
[attach-enode] #229 0
|
|
[attach-enode] #230 0
|
|
[attach-enode] #231 0
|
|
[assign] #232 justification -1: 73
|
|
[assign] #233 justification -1: 73
|
|
[mk-app] #234 = #226 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #234
|
|
[end-of-instance]
|
|
[mk-app] #234 = #231 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #234
|
|
[end-of-instance]
|
|
[mk-app] #234 not #151
|
|
[mk-app] #235 or #151 #234
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #235
|
|
[end-of-instance]
|
|
[mk-app] #234 <= #131 #23
|
|
[assign] #234 justification -1: 26 27
|
|
[mk-app] #235 <= #156 #23
|
|
[assign] #235 justification -1: 41 42
|
|
[resolve-process] true
|
|
[resolve-lit] 8 #67
|
|
[resolve-lit] 8 (not #82)
|
|
[resolve-lit] 0 (not #234)
|
|
[resolve-lit] 5 #143
|
|
[resolve-lit] 0 (not #228)
|
|
[resolve-lit] 8 (not #199)
|
|
[resolve-process] (not #234)
|
|
[resolve-lit] 8 (not #150)
|
|
[resolve-lit] 8 (not #145)
|
|
[conflict] (not #228) (not #82) #143
|
|
[pop] 5 9
|
|
[attach-enode] #225 0
|
|
[attach-enode] #226 0
|
|
[assign] (not #228) clause -70 23 -14
|
|
[resolve-process] true
|
|
[resolve-lit] 3 (not #78)
|
|
[resolve-lit] 3 (not #198)
|
|
[resolve-lit] 0 #228
|
|
[conflict] #228 (not #78) (not #198)
|
|
[pop] 3 4
|
|
[attach-enode] #225 0
|
|
[attach-enode] #226 0
|
|
[assign] #228 clause 55 -10 -53
|
|
[assign] #143 clause 23 -55 -14
|
|
[mk-app] #200 = #226 #36
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #200
|
|
[end-of-instance]
|
|
[push] 1
|
|
[assign] (not #179) decision axiom
|
|
[assign] #176 clause 39 43
|
|
[assign] #177 justification -1: 39
|
|
[mk-app] #200 = #38 #119
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #201 + #38 #117
|
|
[mk-app] #202 <= #201 #23
|
|
[mk-app] #203 >= #201 #23
|
|
[assign] #200 justification -1: 39
|
|
[attach-enode] #200 0
|
|
[attach-enode] #201 0
|
|
[assign] #202 justification -1: 56
|
|
[assign] #203 justification -1: 56
|
|
[mk-app] #204 = #130 #155
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #205 * #108 #155
|
|
[mk-app] #206 + #130 #205
|
|
[mk-app] #207 <= #206 #23
|
|
[mk-app] #208 >= #206 #23
|
|
[assign] #204 justification -1: 39 24
|
|
[attach-enode] #204 0
|
|
[attach-enode] #205 0
|
|
[attach-enode] #206 0
|
|
[assign] #207 justification -1: 59
|
|
[assign] #208 justification -1: 59
|
|
[mk-app] #209 = #144 #172
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #210 * #108 #172
|
|
[mk-app] #211 + #144 #210
|
|
[mk-app] #212 <= #211 #23
|
|
[mk-app] #213 >= #211 #23
|
|
[assign] #209 justification -1: 39 24
|
|
[attach-enode] #209 0
|
|
[attach-enode] #210 0
|
|
[attach-enode] #211 0
|
|
[assign] #212 justification -1: 62
|
|
[assign] #213 justification -1: 62
|
|
[mk-app] #214 = #183 #191
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #215 * #72 #191
|
|
[mk-app] #216 + #183 #215
|
|
[mk-app] #217 <= #216 #28
|
|
[mk-app] #218 >= #216 #28
|
|
[assign] #214 justification -1: 39 24
|
|
[attach-enode] #214 0
|
|
[attach-enode] #215 0
|
|
[attach-enode] #216 0
|
|
[assign] #217 justification -1: 65
|
|
[assign] #218 justification -1: 65
|
|
[mk-app] #219 = #40 #55
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #220 * #72 #55
|
|
[mk-app] #221 + #40 #220
|
|
[mk-app] #222 <= #221 #28
|
|
[mk-app] #223 >= #221 #28
|
|
[assign] #219 justification -1: 24 39
|
|
[attach-enode] #219 0
|
|
[attach-enode] #220 0
|
|
[attach-enode] #221 0
|
|
[assign] #222 justification -1: 68
|
|
[assign] #223 justification -1: 68
|
|
[assign] #178 clause 41 -40
|
|
[assign] #173 clause 42 -40
|
|
[assign] #181 clause 45 -42
|
|
[mk-app] #224 = #201 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #206 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #211 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #216 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #221 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[mk-app] #224 = #35 #194
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #224
|
|
[end-of-instance]
|
|
[push] 2
|
|
[assign] (not #152) decision axiom
|
|
[push] 3
|
|
[assign] (not #142) decision axiom
|
|
[assign] (not #133) clause -21 22
|
|
[push] 4
|
|
[assign] (not #182) decision axiom
|
|
[push] 5
|
|
[assign] (not #187) decision axiom
|
|
[push] 6
|
|
[assign] (not #171) decision axiom
|
|
[assign] #170 clause 37 38
|
|
[assign] (not #161) clause -36 38
|
|
[push] 7
|
|
[assign] (not #180) decision axiom
|
|
[push] 8
|
|
[assign] (not #159) decision axiom
|
|
[mk-app] #224 = #172 #226
|
|
[attach-enode] #224 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #227 * #108 #226
|
|
[mk-app] #229 + #172 #227
|
|
[mk-app] #230 <= #229 #23
|
|
[mk-app] #231 >= #229 #23
|
|
[attach-enode] #227 0
|
|
[attach-enode] #229 0
|
|
[push] 9
|
|
[assign] #224 decision axiom
|
|
[assign] #230 clause 72 -71
|
|
[assign] #231 clause 73 -71
|
|
[mk-app] #232 = #125 #183
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #233 * #72 #183
|
|
[mk-app] #234 + #125 #233
|
|
[mk-app] #235 <= #234 #28
|
|
[mk-app] #236 >= #234 #28
|
|
[assign] #232 justification -1: 71 24 39 24 53 54 26 27
|
|
[attach-enode] #232 0
|
|
[attach-enode] #233 0
|
|
[attach-enode] #234 0
|
|
[assign] #235 justification -1: 74
|
|
[assign] #236 justification -1: 74
|
|
[mk-app] #237 = #229 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #237
|
|
[end-of-instance]
|
|
[mk-app] #237 = #234 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #237
|
|
[end-of-instance]
|
|
[mk-app] #237 <= #54 #23
|
|
[assign] #237 justification -1: -28
|
|
[mk-app] #238 not #237
|
|
[mk-app] #239 or #237 #238
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #239
|
|
[end-of-instance]
|
|
[mk-app] #238 not #151
|
|
[mk-app] #239 or #151 #238
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #239
|
|
[end-of-instance]
|
|
[mk-app] #238 <= #156 #23
|
|
[assign] #238 justification -1: 41 42
|
|
[resolve-process] true
|
|
[resolve-lit] 0 (not #238)
|
|
[resolve-lit] 8 (not #202)
|
|
[resolve-lit] 3 #171
|
|
[resolve-lit] 9 (not #199)
|
|
[resolve-lit] 9 #151
|
|
[resolve-lit] 0 (not #230)
|
|
[resolve-lit] 8 (not #178)
|
|
[resolve-process] (not #238)
|
|
[resolve-lit] 8 (not #173)
|
|
[conflict] (not #230) (not #202) #171 #151 (not #178) (not #173)
|
|
[pop] 3 10
|
|
[attach-enode] #227 0
|
|
[attach-enode] #229 0
|
|
[assign] (not #230) clause -71 38 -57 28 -41 -42
|
|
[resolve-process] true
|
|
[resolve-lit] 5 (not #173)
|
|
[resolve-lit] 6 (not #228)
|
|
[resolve-lit] 0 #230
|
|
[conflict] #230 (not #173) (not #228)
|
|
[pop] 5 7
|
|
[attach-enode] #227 0
|
|
[attach-enode] #229 0
|
|
[assign] #230 clause 71 -42 -55
|
|
[assign] #171 clause 38 -71 -57 28 -41 -42
|
|
[push] 2
|
|
[assign] (not #152) decision axiom
|
|
[push] 3
|
|
[assign] (not #142) decision axiom
|
|
[assign] (not #133) clause -21 22
|
|
[push] 4
|
|
[assign] (not #182) decision axiom
|
|
[push] 5
|
|
[assign] (not #187) decision axiom
|
|
[push] 6
|
|
[assign] (not #180) decision axiom
|
|
[push] 7
|
|
[assign] (not #170) decision axiom
|
|
[assign] (not #161) clause -36 37
|
|
[push] 8
|
|
[assign] (not #159) decision axiom
|
|
[mk-app] #224 = #197 #226
|
|
[attach-enode] #224 0
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #231 + #197 #227
|
|
[mk-app] #232 <= #231 #23
|
|
[mk-app] #233 >= #231 #23
|
|
[attach-enode] #231 0
|
|
[push] 9
|
|
[assign] #232 decision axiom
|
|
[mk-app] #234 = #231 #229
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #234
|
|
[end-of-instance]
|
|
[push] 10
|
|
[assign] #224 decision axiom
|
|
[assign] #233 clause 74 -72
|
|
[mk-app] #234 = #125 #183
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #235 * #72 #183
|
|
[mk-app] #236 + #125 #235
|
|
[mk-app] #237 <= #236 #28
|
|
[mk-app] #238 >= #236 #28
|
|
[assign] #234 justification -1: 72 24 53 54 54 53
|
|
[attach-enode] #234 0
|
|
[attach-enode] #235 0
|
|
[attach-enode] #236 0
|
|
[assign] #237 justification -1: 75
|
|
[assign] #238 justification -1: 75
|
|
[mk-app] #239 = #231 #23
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #239
|
|
[end-of-instance]
|
|
[mk-app] #239 = #23 #229
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #239
|
|
[end-of-instance]
|
|
[mk-app] #239 = #236 #28
|
|
[inst-discovered] theory-solving 0000000000000000 arith#
|
|
[instance] 0000000000000000 #239
|
|
[end-of-instance]
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[attach-meaning] #108 arith (- 1)
|
|
[mk-app] #239 Int
|
|
[attach-meaning] #239 arith 2
|
|
[mk-app] #240 Int
|
|
[attach-meaning] #240 arith 3
|
|
[mk-app] #241 Real
|
|
[attach-meaning] #241 arith 2
|
|
[mk-app] #242 Real
|
|
[attach-meaning] #242 arith 3
|
|
[mk-app] #243 Int
|
|
[attach-meaning] #243 arith 4
|
|
[mk-app] #244 Int
|
|
[attach-meaning] #244 arith 5
|
|
[mk-app] #245 Int
|
|
[attach-meaning] #245 arith 6
|
|
[mk-app] #246 Int
|
|
[attach-meaning] #246 arith 7
|
|
[mk-app] #247 Int
|
|
[attach-meaning] #247 arith 8
|
|
[mk-app] #248 Int
|
|
[attach-meaning] #248 arith 9
|
|
[mk-app] #249 Int
|
|
[attach-meaning] #249 arith 10
|
|
[mk-app] #250 Real
|
|
[attach-meaning] #250 arith 4
|
|
[mk-app] #251 Real
|
|
[attach-meaning] #251 arith 5
|
|
[mk-app] #252 Int
|
|
[attach-meaning] #252 arith 11
|
|
[mk-app] #253 Real
|
|
[attach-meaning] #253 arith 6
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #5 bv #b1
|
|
[attach-meaning] #6 bv #b0
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #109 <= #28 #72
|
|
[mk-app] #110 not #109
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #115 <= #96 #28
|
|
[mk-app] #116 not #115
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #118 <= #241 #96
|
|
[mk-app] #120 not #118
|
|
[attach-meaning] #72 arith (- 1)
|
|
[attach-meaning] #72 arith (- 1)
|
|
[mk-app] #155 <= #28 #28
|
|
[mk-app] #130 not #155
|
|
[eof]
|