Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
C
cs598mp-fall2021-proj
Manage
Activity
Members
Labels
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Model registry
Analyze
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
chsieh16
cs598mp-fall2021-proj
Commits
4560f5da
Commit
4560f5da
authored
1 year ago
by
chsieh16
Browse files
Options
Downloads
Patches
Plain Diff
Add generated AAP from EMSOFT approach
parent
373f5edc
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
exp_oopsla/gem-emsoft-aap-ult_bound=1.0-vel=2.8.out.json
+1
-0
1 addition, 0 deletions
exp_oopsla/gem-emsoft-aap-ult_bound=1.0-vel=2.8.out.json
with
1 addition
and
0 deletions
exp_oopsla/gem-emsoft-aap-ult_bound=1.0-vel=2.8.out.json
0 → 100644
+
1
−
0
View file @
4560f5da
[{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
-0.2617993877991494
,
-0.20943951023931953
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (- (/ 15394516512607743.0 5000000000000000.0)) (- x_1))
\n
(* (/ 11160342572361413.0 1000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1605092016371253.0 50000000000000000.0) (- x_1))
\n
(* (/ 9419637376065083.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (- (/ 15394516512607743.0 5000000000000000.0)) (- x_1))
\n
(* (/ 11160342572361413.0 1000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1605092016371253.0 50000000000000000.0) (- x_1))
\n
(* (/ 9419637376065083.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
-0.20943951023931953
,
-0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 4714272282732249.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 7779849680047.0 9765625000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 5636117481373213.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 11012272503114409.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 10329359584179607.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 4714272282732249.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 7779849680047.0 9765625000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 5636117481373213.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 11012272503114409.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 10329359584179607.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
-0.15707963267948966
,
-0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 10527595794271727.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 802781930667.0 390625000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4559784287644937.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 11599721514004477.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 3948299015705331.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 10527595794271727.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 802781930667.0 390625000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4559784287644937.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 11599721514004477.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 3948299015705331.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
-0.10471975511965975
,
-0.052359877559829876
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8802835183129537.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 20137502811831287.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1898421512271399.0 200000000000000000.0) (- x_1))
\n
(* (/ 2954729060402157.0 2500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 13954490491586759.0 2000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8802835183129537.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 20137502811831287.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1898421512271399.0 200000000000000000.0) (- x_1))
\n
(* (/ 2954729060402157.0 2500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 13954490491586759.0 2000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
-0.052359877559829876
,
0.0
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 804005534199071.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 5716184322630299.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2025462900811141.0 125000000000000000.0) (- x_1))
\n
(* (/ 10530144821672651.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 3662534193257649.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 804005534199071.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 5716184322630299.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2025462900811141.0 125000000000000000.0) (- x_1))
\n
(* (/ 10530144821672651.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 3662534193257649.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
0.0
,
0.052359877559829904
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 3915289859892767.0 5000000000000000.0) (- x_1))
\n
(* (/ 148006381927741.0 390625000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2283080304802329.0 125000000000000000.0) (- x_1))
\n
(* (/ 963349452695649.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 904884256347089.0 125000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 3915289859892767.0 5000000000000000.0) (- x_1))
\n
(* (/ 148006381927741.0 390625000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2283080304802329.0 125000000000000000.0) (- x_1))
\n
(* (/ 963349452695649.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 904884256347089.0 125000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
0.052359877559829904
,
0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 755099929351027.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 5759861544525549.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 228339194430877.0 10000000000000000.0) (- x_1))
\n
(* (/ 5437904836830719.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 1552959434920751.0 200000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 755099929351027.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 5759861544525549.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 228339194430877.0 10000000000000000.0) (- x_1))
\n
(* (/ 5437904836830719.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 1552959434920751.0 200000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
0.10471975511965975
,
0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8397160189683781.0 10000000000000000.0) (- x_1))
\n
(* (/ 9091844298777943.0 50000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 604619557148917.0 31250000000000000.0) (- x_1))
\n
(* (/ 1310731749719749.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 1769680012466759.0 200000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8397160189683781.0 10000000000000000.0) (- x_1))
\n
(* (/ 9091844298777943.0 50000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 604619557148917.0 31250000000000000.0) (- x_1))
\n
(* (/ 1310731749719749.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 1769680012466759.0 200000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
0.15707963267948966
,
0.20943951023931956
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8196471058153899.0 10000000000000000.0) (- x_1))
\n
(* (/ 5028196357751839.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 9291717199585093.0 500000000000000000.0) (- x_1))
\n
(* (/ 10304618010835673.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 11764936805828139.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8196471058153899.0 10000000000000000.0) (- x_1))
\n
(* (/ 5028196357751839.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 9291717199585093.0 500000000000000000.0) (- x_1))
\n
(* (/ 10304618010835673.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 11764936805828139.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-1.2
,
-0.6
],
[
0.20943951023931956
,
0.2617993877991494
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 7449029241943507.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 34319015358513677.0 100000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 15613216950181759.0 500000000000000000.0) (- x_1))
\n
(* (/ 2165380121931539.0 2000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 858211531305779.0 50000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 7449029241943507.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 34319015358513677.0 100000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 15613216950181759.0 500000000000000000.0) (- x_1))
\n
(* (/ 2165380121931539.0 2000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 858211531305779.0 50000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
-0.2617993877991494
,
-0.20943951023931953
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 9880361849440813.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 11040409032409.0 16000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 5267959107819491.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 5279957089382127.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 8275850353234599.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 9880361849440813.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 11040409032409.0 16000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 5267959107819491.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 5279957089382127.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 8275850353234599.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
-0.20943951023931953
,
-0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 1004536409768367.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 433567899649319.0 400000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4377267900988293.0 10000000000000000000.0)) (- x_1))
\n
(* (/ 10842835632334589.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 2069816206121939.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 1004536409768367.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 433567899649319.0 400000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4377267900988293.0 10000000000000000000.0)) (- x_1))
\n
(* (/ 10842835632334589.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 2069816206121939.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
-0.15707963267948966
,
-0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 4689739905164137.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 11967370246900557.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 9428278428006391.0 2500000000000000000.0) (- x_1))
\n
(* (/ 1364120470989437.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 1670231819390749.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 4689739905164137.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 11967370246900557.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 9428278428006391.0 2500000000000000000.0) (- x_1))
\n
(* (/ 1364120470989437.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 1670231819390749.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
-0.10471975511965975
,
-0.052359877559829876
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 6894006984270191.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 5601121606506557.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 13635010621300469.0 500000000000000000.0) (- x_1))
\n
(* (/ 266548037158479.0 250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 859990119756303.0 2500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 6894006984270191.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 5601121606506557.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 13635010621300469.0 500000000000000000.0) (- x_1))
\n
(* (/ 266548037158479.0 250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 859990119756303.0 2500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
-0.052359877559829876
,
0.0
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 4012407979788999.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 9323701999082753.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2788991572033073.0 250000000000000000.0) (- x_1))
\n
(* (/ 11450138353215833.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 4012407979788999.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 9323701999082753.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2788991572033073.0 250000000000000000.0) (- x_1))
\n
(* (/ 11450138353215833.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
0.0
,
0.052359877559829904
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 4001585557821269.0 5000000000000000.0) (- x_1))
\n
(* (/ 304606001168943.0 156250000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 12515126696607577.0 1000000000000000000.0) (- x_1))
\n
(* (/ 9370324313532873.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 4001585557821269.0 5000000000000000.0) (- x_1))
\n
(* (/ 304606001168943.0 156250000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 12515126696607577.0 1000000000000000000.0) (- x_1))
\n
(* (/ 9370324313532873.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
0.052359877559829904
,
0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 9428772038301123.0 10000000000000000.0) (- x_1))
\n
(* (/ 6426945322514297.0 5000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 31275925282361053.0 10000000000000000000.0) (- x_1))
\n
(* (/ 469057719055757.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 7036118239147783.0 10000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 9428772038301123.0 10000000000000000.0) (- x_1))
\n
(* (/ 6426945322514297.0 5000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 31275925282361053.0 10000000000000000000.0) (- x_1))
\n
(* (/ 469057719055757.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 7036118239147783.0 10000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
0.10471975511965975
,
0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8502246634852169.0 10000000000000000.0) (- x_1))
\n
(* (/ 84647014687647.0 156250000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 8226906527708513.0 1000000000000000000.0) (- x_1))
\n
(* (/ 492403611813093.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 16937438512380871.0 5000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8502246634852169.0 10000000000000000.0) (- x_1))
\n
(* (/ 84647014687647.0 156250000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 8226906527708513.0 1000000000000000000.0) (- x_1))
\n
(* (/ 492403611813093.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 16937438512380871.0 5000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
0.15707963267948966
,
0.20943951023931956
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8804135980309051.0 10000000000000000.0) (- x_1))
\n
(* (/ 26019278994628803.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 38334450852194313.0 10000000000000000000.0) (- x_1))
\n
(* (/ 1991404871889733.0 2000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 171565046396301.0 20000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8804135980309051.0 10000000000000000.0) (- x_1))
\n
(* (/ 26019278994628803.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 38334450852194313.0 10000000000000000000.0) (- x_1))
\n
(* (/ 1991404871889733.0 2000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 171565046396301.0 20000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
-0.6
,
0.0
],
[
0.20943951023931956
,
0.2617993877991494
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8030535254050801.0 10000000000000000.0) (- x_1))
\n
(* (/ 207154092992597.0 6250000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1701725261979779.0 100000000000000000.0) (- x_1))
\n
(* (/ 10145183346534679.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 16170765055133353.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8030535254050801.0 10000000000000000.0) (- x_1))
\n
(* (/ 207154092992597.0 6250000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1701725261979779.0 100000000000000000.0) (- x_1))
\n
(* (/ 10145183346534679.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 16170765055133353.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
-0.2617993877991494
,
-0.20943951023931953
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 2121610998146079.0 2500000000000000.0) (- x_1))
\n
(* (- (/ 3885374828653829.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3078474216288387.0 200000000000000000.0) (- x_1))
\n
(* (/ 5306095596592677.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 10815843399322957.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 2121610998146079.0 2500000000000000.0) (- x_1))
\n
(* (- (/ 3885374828653829.0 5000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3078474216288387.0 200000000000000000.0) (- x_1))
\n
(* (/ 5306095596592677.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 10815843399322957.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
-0.20943951023931953
,
-0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 10043723727041867.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 8120172194047247.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 8881645681677341.0 20000000000000000000.0)) (- x_1))
\n
(* (/ 1323767317881219.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 13260782961369687.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 10043723727041867.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 8120172194047247.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 8881645681677341.0 20000000000000000000.0)) (- x_1))
\n
(* (/ 1323767317881219.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 13260782961369687.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
-0.15707963267948966
,
-0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 10162616758049299.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2612262668749873.0 2500000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1364581874550667.0 3125000000000000000.0) (- x_1))
\n
(* (/ 10762721173859557.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 396827405569201.0 62500000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 10162616758049299.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2612262668749873.0 2500000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1364581874550667.0 3125000000000000000.0) (- x_1))
\n
(* (/ 10762721173859557.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 396827405569201.0 62500000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
-0.10471975511965975
,
-0.052359877559829876
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 8948448273905373.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2282508523149617.0 1250000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 14687506572532791.0 1000000000000000000.0) (- x_1))
\n
(* (/ 1129811251877317.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 7244789770054329.0 5000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 8948448273905373.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2282508523149617.0 1250000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 14687506572532791.0 1000000000000000000.0) (- x_1))
\n
(* (/ 1129811251877317.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 7244789770054329.0 5000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
-0.052359877559829876
,
0.0
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 11639385580730441.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 12709682455885947.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4245230341807707.0 500000000000000000.0)) (- x_1))
\n
(* (/ 5281088493477293.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 11639385580730441.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 12709682455885947.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 4245230341807707.0 500000000000000000.0)) (- x_1))
\n
(* (/ 5281088493477293.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
0.0
,
0.052359877559829904
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 2691461674106983.0 2500000000000000.0) (- x_1))
\n
(* (/ 16126622211804373.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 805287654083333.0 500000000000000000.0) (- x_1))
\n
(* (/ 2385129015713521.0 2500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 2691461674106983.0 2500000000000000.0) (- x_1))
\n
(* (/ 16126622211804373.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 805287654083333.0 500000000000000000.0) (- x_1))
\n
(* (/ 2385129015713521.0 2500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
0.052359877559829904
,
0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 1144982723503549.0 1250000000000000.0) (- x_1))
\n
(* (/ 1121421431458757.0 1000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 624030174830711.0 50000000000000000.0) (- x_1))
\n
(* (/ 4747216531815359.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 1068063698926183.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 1144982723503549.0 1250000000000000.0) (- x_1))
\n
(* (/ 1121421431458757.0 1000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 624030174830711.0 50000000000000000.0) (- x_1))
\n
(* (/ 4747216531815359.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 1068063698926183.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
0.10471975511965975
,
0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 2190096868059607.0 2500000000000000.0) (- x_1))
\n
(* (/ 312726615744361.0 625000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 311133400865907.0 20000000000000000.0) (- x_1))
\n
(* (/ 495197240300101.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 3467404948350343.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 2190096868059607.0 2500000000000000.0) (- x_1))
\n
(* (/ 312726615744361.0 625000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 311133400865907.0 20000000000000000.0) (- x_1))
\n
(* (/ 495197240300101.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 3467404948350343.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
0.15707963267948966
,
0.20943951023931956
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 11482401883882497.0 50000000000000000.0) (- x_1))
\n
(* (/ 8833553339121069.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3082107943952683.0 250000000000000000.0) (- x_1))
\n
(* (/ 982424909266799.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 4361818347632187.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 11482401883882497.0 50000000000000000.0) (- x_1))
\n
(* (/ 8833553339121069.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3082107943952683.0 250000000000000000.0) (- x_1))
\n
(* (/ 982424909266799.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 4361818347632187.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.0
,
0.5999999999999999
],
[
0.20943951023931956
,
0.2617993877991494
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (- (/ 1455496082504191.0 200000000000000.0)) (- x_1))
\n
(* (/ 16590473473426939.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3162653881007017.0 125000000000000000.0) (- x_1))
\n
(* (/ 9850491358198713.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (- (/ 1455496082504191.0 200000000000000.0)) (- x_1))
\n
(* (/ 16590473473426939.0 10000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 3162653881007017.0 125000000000000000.0) (- x_1))
\n
(* (/ 9850491358198713.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
-0.2617993877991494
,
-0.20943951023931953
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 4334822526305619.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 536294921446787.0 625000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 162104552362039.0 10000000000000000.0) (- x_1))
\n
(* (/ 1073409515848489.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 11631989974900267.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 4334822526305619.0 5000000000000000.0) (- x_1))
\n
(* (- (/ 536294921446787.0 625000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 162104552362039.0 10000000000000000.0) (- x_1))
\n
(* (/ 1073409515848489.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 11631989974900267.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
-0.20943951023931953
,
-0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 1822492790387731.0 2500000000000000.0) (- x_1))
\n
(* (- (/ 18538498536519843.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1824076879934283.0 50000000000000000.0) (- x_1))
\n
(* (/ 187016002729463.0 156250000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 8679682042791287.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 1822492790387731.0 2500000000000000.0) (- x_1))
\n
(* (- (/ 18538498536519843.0 10000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 1824076879934283.0 50000000000000000.0) (- x_1))
\n
(* (/ 187016002729463.0 156250000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 8679682042791287.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
-0.15707963267948966
,
-0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 6111725136367281.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2964060937509089.0 1000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 8060289093833349.0 200000000000000000.0) (- x_1))
\n
(* (/ 1568189627641107.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 6664203159518163.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 6111725136367281.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 2964060937509089.0 1000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 8060289093833349.0 200000000000000000.0) (- x_1))
\n
(* (/ 1568189627641107.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 6664203159518163.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
-0.10471975511965975
,
-0.052359877559829876
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 1803915515714033.0 2000000000000000.0) (- x_1))
\n
(* (- (/ 3099877004863941.0 2000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 52878250399397.0 4000000000000000.0) (- x_1))
\n
(* (/ 11111702371860037.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 5317086715191631.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 1803915515714033.0 2000000000000000.0) (- x_1))
\n
(* (- (/ 3099877004863941.0 2000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 52878250399397.0 4000000000000000.0) (- x_1))
\n
(* (/ 11111702371860037.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 5317086715191631.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
-0.052359877559829876
,
0.0
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 993715228771501.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 20315263033885217.0 50000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 5965844834964831.0 1000000000000000000.0) (- x_1))
\n
(* (/ 494566948372731.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 95789281727303.0 10000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 993715228771501.0 1000000000000000.0) (- x_1))
\n
(* (- (/ 20315263033885217.0 50000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 5965844834964831.0 1000000000000000000.0) (- x_1))
\n
(* (/ 494566948372731.0 500000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 95789281727303.0 10000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
0.0
,
0.052359877559829904
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 2516176143500391.0 2500000000000000.0) (- x_1))
\n
(* (/ 2065256737533531.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 29146591937641393.0 5000000000000000000.0) (- x_1))
\n
(* (/ 624583140840339.0 625000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 4900063528805807.0 500000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 2516176143500391.0 2500000000000000.0) (- x_1))
\n
(* (/ 2065256737533531.0 100000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 29146591937641393.0 5000000000000000000.0) (- x_1))
\n
(* (/ 624583140840339.0 625000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 4900063528805807.0 500000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
0.052359877559829904
,
0.10471975511965975
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 5041959510636277.0 5000000000000000.0) (- x_1))
\n
(* (/ 7709614854297493.0 250000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 2487493795855533.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 5402574190307129.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) (/ 10207060531037617.0 1000000000000000000.0)))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 5041959510636277.0 5000000000000000.0) (- x_1))
\n
(* (/ 7709614854297493.0 250000000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (- (/ 2487493795855533.0 1000000000000000000.0)) (- x_1))
\n
(* (/ 5402574190307129.0 5000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0))
\n
(/ 10207060531037617.0 1000000000000000000.0)))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
0.10471975511965975
,
0.15707963267948966
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (- (/ 386054894395631.0 312500000000000.0)) (- x_1))
\n
(* (/ 4420290115923221.0 500000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 902519105044549.0 200000000000000000.0) (- x_1))
\n
(* (/ 10172180088315181.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (- (/ 386054894395631.0 312500000000000.0)) (- x_1))
\n
(* (/ 4420290115923221.0 500000000000000.0) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 902519105044549.0 200000000000000000.0) (- x_1))
\n
(* (/ 10172180088315181.0 10000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
0.15707963267948966
,
0.20943951023931956
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (- (/ 4829472251529503.0 2000000000000000.0)) (- x_1))
\n
(* (- (/ 2791763618243791.0 1000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 10463173705548941.0 1000000000000000000.0) (- x_1))
\n
(* (/ 1018262268127513.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (- (/ 4829472251529503.0 2000000000000000.0)) (- x_1))
\n
(* (- (/ 2791763618243791.0 1000000000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 10463173705548941.0 1000000000000000000.0) (- x_1))
\n
(* (/ 1018262268127513.0 1000000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}},
{
"part"
:
[[
-Infinity
,
Infinity
],
[
0.5999999999999999
,
1.2
],
[
0.20943951023931956
,
0.2617993877991494
]],
"ultimate_bound"
:
1.0
,
"status"
:
"found"
,
"result"
:
{
"formula"
:
"(let ((a!1 (- z_0
\n
(+ (* (/ 7002921745469697.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 559300984630813.0 31250000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2032088228319903.0 250000000000000000.0) (- x_1))
\n
(* (/ 1286038630009711.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))"
,
"smtlib"
:
"(declare-fun F (Bool) Bool)
\n
(declare-fun x_2 () Real)
\n
(declare-fun x_1 () Real)
\n
(declare-fun z_1 () Real)
\n
(declare-fun z_0 () Real)
\n
(assert (let ((a!1 (- z_0
\n
(+ (* (/ 7002921745469697.0 10000000000000000.0) (- x_1))
\n
(* (- (/ 559300984630813.0 31250000000000.0)) (- x_2))
\n
0.0)))
\n
(a!2 (- z_1
\n
(+ (* (/ 2032088228319903.0 250000000000000000.0) (- x_1))
\n
(* (/ 1286038630009711.0 1250000000000000.0) (- x_2))
\n
0.0))))
\n
(F (<= (+ (^ a!1 2.0) (^ a!2 2.0)) 0.0))))
\n
"
}}]
\ No newline at end of file
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment