Skip to content
Snippets Groups Projects
Commit 373f5edc authored by chsieh16's avatar chsieh16
Browse files

Add experiment result for a range of speed

parent 72b54d54
No related branches found
No related tags found
No related merge requests found
Showing
with 18713 additions and 0 deletions
[
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
-0.2617993877991494,
-0.20943951023931953
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "(>= (+ x_1 x_2) (- (/ 427775.0 524288.0)))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (F (>= (+ x_1 x_2) (- (/ 427775.0 524288.0)))))\n"
},
"teacher time": 0.005358219146728516,
"learner time": 0.13655424118041992
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
-0.20943951023931953,
-0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 34,
"formula": "(let ((a!1 (not (>= (+ x_2 (* (- 1.0) z_1)) (- (/ 1930943.0 8388608.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 2489531890663423.0 2251799813685248.0))))))\n (ite (>= (+ x_1 x_2) (- (/ 4872946950602751.0 4503599627370496.0)))\n a!1\n (and (>= (+ x_1 z_0 z_1) (- (/ 8057127792803839.0 18014398509481984.0)))\n a!2)))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_0 () Real)\n(assert (let ((a!1 (not (>= (+ x_2 (* (- 1.0) z_1)) (- (/ 1930943.0 8388608.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 2489531890663423.0 2251799813685248.0))))))\n(let ((a!3 (ite (>= (+ x_1 x_2) (- (/ 4872946950602751.0 4503599627370496.0)))\n a!1\n (and (>= (+ x_1 z_0 z_1)\n (- (/ 8057127792803839.0 18014398509481984.0)))\n a!2))))\n (F a!3))))\n"
},
"teacher time": 451.126576423645,
"learner time": 2.9727838039398193
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
-0.15707963267948966,
-0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 47,
"formula": "(let ((a!1 (not (>= (+ x_2 (* (- 1.0) z_0))\n (/ 6885245966090241.0 4503599627370496.0))))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) z_1) (/ 13367799.0 33554432.0)))))\n(let ((a!3 (ite (>= (+ x_2 z_1) (/ 5407353088245759.0 18014398509481984.0))\n a!1\n (and a!2\n (>= (+ x_2 z_1) (/ 3811214928904191.0 18014398509481984.0))))))\n(let ((a!4 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (- (/ 15772503.0 8388608.0)))\n a!3)))\n(let ((a!5 (or (>= x_1 (- (/ 7162443.0 8388608.0)))\n (and (>= (+ x_1 z_1) (- (/ 11478269.0 16777216.0))) a!4)\n (>= (+ x_1 (* (- 1.0) z_0) z_1)\n (/ 8057822503763969.0 4503599627370496.0)))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 7468330726195199.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 7060064019939327.0 144115188075855872.0)))\n a!5)))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_1 () Real)\n(declare-fun x_2 () Real)\n(assert (let ((a!1 (not (>= (+ x_2 (* (- 1.0) z_0))\n (/ 6885245966090241.0 4503599627370496.0))))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) z_1) (/ 13367799.0 33554432.0)))))\n(let ((a!3 (ite (>= (+ x_2 z_1) (/ 5407353088245759.0 18014398509481984.0))\n a!1\n (and a!2\n (>= (+ x_2 z_1) (/ 3811214928904191.0 18014398509481984.0))))))\n(let ((a!4 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (- (/ 15772503.0 8388608.0)))\n a!3)))\n(let ((a!5 (or (>= x_1 (- (/ 7162443.0 8388608.0)))\n (and (>= (+ x_1 z_1) (- (/ 11478269.0 16777216.0))) a!4)\n (>= (+ x_1 (* (- 1.0) z_0) z_1)\n (/ 8057822503763969.0 4503599627370496.0)))))\n (F (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 7468330726195199.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 7060064019939327.0 144115188075855872.0)))\n a!5)))))))\n"
},
"teacher time": 929.2359480857849,
"learner time": 6.740450620651245
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
-0.10471975511965975,
-0.052359877559829876
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 64,
"formula": "(let ((a!1 (and (>= (+ x_2 z_1) (/ 7909226298998785.0 36028797018963968.0))\n (not (<= (+ z_0 z_1) (- (/ 15047937.0 16777216.0))))))\n (a!3 (or (>= (+ x_2 z_0 z_1) (- (/ 5167987.0 8388608.0)))\n (and (>= (+ x_2 z_1) (/ 8096409563693055.0 36028797018963968.0))\n (not (<= z_0 (- (/ 5710786622128127.0 4503599627370496.0))))))))\n(let ((a!2 (and (not (<= (+ x_2 z_1) (/ 3415761452269569.0 18014398509481984.0)))\n (or (>= (+ x_1 z_0 z_1)\n (- (/ 3690169328730111.0 2251799813685248.0)))\n a!1)))\n (a!4 (or (>= (+ x_1 z_0 z_1)\n (- (/ 6270390796025857.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 5153400261967871.0 36028797018963968.0))\n a!3))))\n(let ((a!5 (ite (>= (+ x_1 (* (- 1.0) z_1))\n (- (/ 3081817276022783.0 2251799813685248.0)))\n a!2\n a!4)))\n(let ((a!6 (or (>= (+ x_1 (* (- 1.0) x_2)) (- (/ 1467563.0 2097152.0))) a!5)))\n (ite (>= (+ x_1 z_0 z_1) (- (/ 14128403.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 1789237.0 134217728.0)))\n a!6)))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_0 () Real)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (and (>= (+ x_2 z_1) (/ 7909226298998785.0 36028797018963968.0))\n (not (<= (+ z_0 z_1) (- (/ 15047937.0 16777216.0))))))\n (a!3 (or (>= (+ x_2 z_0 z_1) (- (/ 5167987.0 8388608.0)))\n (and (>= (+ x_2 z_1) (/ 8096409563693055.0 36028797018963968.0))\n (not (<= z_0 (- (/ 5710786622128127.0 4503599627370496.0))))))))\n(let ((a!2 (and (not (<= (+ x_2 z_1) (/ 3415761452269569.0 18014398509481984.0)))\n (or (>= (+ x_1 z_0 z_1)\n (- (/ 3690169328730111.0 2251799813685248.0)))\n a!1)))\n (a!4 (or (>= (+ x_1 z_0 z_1)\n (- (/ 6270390796025857.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 5153400261967871.0 36028797018963968.0))\n a!3))))\n(let ((a!5 (ite (>= (+ x_1 (* (- 1.0) z_1))\n (- (/ 3081817276022783.0 2251799813685248.0)))\n a!2\n a!4)))\n(let ((a!6 (or (>= (+ x_1 (* (- 1.0) x_2)) (- (/ 1467563.0 2097152.0))) a!5)))\n (F (ite (>= (+ x_1 z_0 z_1) (- (/ 14128403.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 1789237.0 134217728.0)))\n a!6)))))))\n"
},
"teacher time": 2127.52836227417,
"learner time": 12.304165840148926
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
-0.052359877559829876,
0.0
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 60,
"formula": "(let ((a!1 (ite (>= (+ x_2 z_1) (/ 3674374049628159.0 18014398509481984.0))\n (not (<= (+ z_0 z_1) (- (/ 1796573.0 2097152.0))))\n (and (>= (+ x_1 x_2 z_0)\n (- (/ 2465475778838529.0 2251799813685248.0)))\n (>= (+ x_1 z_1) (- (/ 1876987.0 2097152.0)))))))\n(let ((a!2 (ite (>= x_1 (- (/ 7885591.0 8388608.0)))\n (>= (+ x_2 z_1) (- (/ 1838425.0 268435456.0)))\n (ite (>= (+ x_2 z_0 z_1)\n (/ 8596497838899197.0 72057594037927936.0))\n (>= (+ x_2 z_1) (- (/ 4001969.0 536870912.0)))\n a!1))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 11202195.0 33554432.0)))\n (>= (+ x_2 z_1) (- (/ 8930489.0 134217728.0)))\n a!2)))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(assert (let ((a!1 (ite (>= (+ x_2 z_1) (/ 3674374049628159.0 18014398509481984.0))\n (not (<= (+ z_0 z_1) (- (/ 1796573.0 2097152.0))))\n (and (>= (+ x_1 x_2 z_0)\n (- (/ 2465475778838529.0 2251799813685248.0)))\n (>= (+ x_1 z_1) (- (/ 1876987.0 2097152.0)))))))\n(let ((a!2 (ite (>= x_1 (- (/ 7885591.0 8388608.0)))\n (>= (+ x_2 z_1) (- (/ 1838425.0 268435456.0)))\n (ite (>= (+ x_2 z_0 z_1)\n (/ 8596497838899197.0 72057594037927936.0))\n (>= (+ x_2 z_1) (- (/ 4001969.0 536870912.0)))\n a!1))))\n (F (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 11202195.0 33554432.0)))\n (>= (+ x_2 z_1) (- (/ 8930489.0 134217728.0)))\n a!2)))))\n"
},
"teacher time": 1301.1576087474823,
"learner time": 10.929332733154297
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
0.0,
0.052359877559829904
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 74,
"formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 8509589.0 8388608.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6049177968574463.0 4503599627370496.0)))))\n (a!3 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5398527.0 16777216.0))))))\n(let ((a!4 (or a!3\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 2817039.0 2097152.0))))))\n(let ((a!5 (and (>= x_2 (/ 4706359127834625.0 288230376151711744.0))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 4581261226016769.0 4503599627370496.0)))\n (or a!1 (and a!2 a!4)))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 15711327.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 3229690315669505.0 288230376151711744.0)))\n (or (>= (+ x_1 x_2) (- (/ 7196199.0 8388608.0))) a!5)))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_0 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 8509589.0 8388608.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6049177968574463.0 4503599627370496.0)))))\n (a!3 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5398527.0 16777216.0))))))\n(let ((a!4 (or a!3\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 2817039.0 2097152.0))))))\n(let ((a!5 (and (>= x_2 (/ 4706359127834625.0 288230376151711744.0))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 4581261226016769.0 4503599627370496.0)))\n (or a!1 (and a!2 a!4)))))\n(let ((a!6 (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 15711327.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 3229690315669505.0 288230376151711744.0)))\n (or (>= (+ x_1 x_2) (- (/ 7196199.0 8388608.0))) a!5))))\n (F a!6))))))\n"
},
"teacher time": 1413.452791929245,
"learner time": 11.662935018539429
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
0.052359877559829904,
0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 140,
"formula": "(let ((a!1 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 5262564908859391.0 36028797018963968.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) z_0)) (/ 254593.0 2097152.0)))))\n(let ((a!3 (or (>= (+ x_2 z_0 z_1) (- (/ 14961971.0 16777216.0)))\n (and a!2 (>= (+ x_2 z_1) (/ 4019899.0 16777216.0))))))\n(let ((a!4 (ite (>= x_1 (- (/ 3988291.0 4194304.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 4882331991015423.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 3222053.0 16777216.0)) a!3))))\n(let ((a!5 (ite (>= (+ x_1 z_1) (- (/ 848445.0 1048576.0)))\n a!1\n (ite (>= (+ x_2 z_0 z_1)\n (/ 6986936833015809.0 36028797018963968.0))\n (>= (+ x_2 z_1)\n (- (/ 6455808292290563.0 576460752303423488.0)))\n a!4))))\n (ite (>= (+ x_1 z_0 z_1) (- (/ 3240019.0 8388608.0)))\n (>= (+ x_2 z_1) (- (/ 4597519.0 67108864.0)))\n a!5)))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 5262564908859391.0 36028797018963968.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) z_0)) (/ 254593.0 2097152.0)))))\n(let ((a!3 (or (>= (+ x_2 z_0 z_1) (- (/ 14961971.0 16777216.0)))\n (and a!2 (>= (+ x_2 z_1) (/ 4019899.0 16777216.0))))))\n(let ((a!4 (ite (>= x_1 (- (/ 3988291.0 4194304.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 4882331991015423.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 3222053.0 16777216.0)) a!3))))\n(let ((a!5 (ite (>= (+ x_1 z_1) (- (/ 848445.0 1048576.0)))\n a!1\n (ite (>= (+ x_2 z_0 z_1)\n (/ 6986936833015809.0 36028797018963968.0))\n (>= (+ x_2 z_1)\n (- (/ 6455808292290563.0 576460752303423488.0)))\n a!4))))\n (F (ite (>= (+ x_1 z_0 z_1) (- (/ 3240019.0 8388608.0)))\n (>= (+ x_2 z_1) (- (/ 4597519.0 67108864.0)))\n a!5)))))))\n"
},
"teacher time": 3609.6403546333313,
"learner time": 36.37754821777344
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
0.10471975511965975,
0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 95,
"formula": "(let ((a!1 (and (>= (+ x_2 z_1) (/ 5699661046218751.0 144115188075855872.0))\n (not (>= (+ x_2 z_1) (/ 82941.0 2097152.0))))))\n(let ((a!2 (and (>= x_1 (- (/ 2398500595695617.0 2251799813685248.0)))\n (or (not (>= x_1 (- (/ 8933977.0 8388608.0)))) a!1))))\n(let ((a!3 (or (>= x_1 (- (/ 15073447.0 16777216.0)))\n (ite (>= (+ x_2 z_0 z_1)\n (/ 7946064233496575.0 72057594037927936.0))\n (>= (+ x_2 z_1)\n (- (/ 8040724238958595.0 576460752303423488.0)))\n a!2))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 5357516435226625.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 1131209.0 16777216.0)))\n a!3))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_0 () Real)\n(assert (let ((a!1 (and (>= (+ x_2 z_1) (/ 5699661046218751.0 144115188075855872.0))\n (not (>= (+ x_2 z_1) (/ 82941.0 2097152.0))))))\n(let ((a!2 (and (>= x_1 (- (/ 2398500595695617.0 2251799813685248.0)))\n (or (not (>= x_1 (- (/ 8933977.0 8388608.0)))) a!1))))\n(let ((a!3 (or (>= x_1 (- (/ 15073447.0 16777216.0)))\n (ite (>= (+ x_2 z_0 z_1)\n (/ 7946064233496575.0 72057594037927936.0))\n (>= (+ x_2 z_1)\n (- (/ 8040724238958595.0 576460752303423488.0)))\n a!2))))\n (F (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5357516435226625.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 1131209.0 16777216.0)))\n a!3))))))\n"
},
"teacher time": 2414.811444044113,
"learner time": 18.83181095123291
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
0.15707963267948966,
0.20943951023931956
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 14,
"formula": "(ite (>= (+ x_2 z_1) (- (/ 7618601968205823.0 1152921504606846976.0)))\n (or (>= (+ x_1 x_2 z_0 z_1) (- (/ 4672176019996671.0 4503599627370496.0)))\n (>= x_1 (- (/ 14970767.0 16777216.0))))\n (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 6374792324186111.0 288230376151711744.0)))\n (>= (+ x_2 z_1) (- (/ 156453.0 8388608.0)))\n (>= (+ x_1 x_2) (- (/ 5154723.0 8388608.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 (ite (>= (+ x_2 z_1)\n (- (/ 7618601968205823.0 1152921504606846976.0)))\n (or (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4672176019996671.0 4503599627370496.0)))\n (>= x_1 (- (/ 14970767.0 16777216.0))))\n (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 6374792324186111.0 288230376151711744.0)))\n (>= (+ x_2 z_1) (- (/ 156453.0 8388608.0)))\n (>= (+ x_1 x_2) (- (/ 5154723.0 8388608.0)))))))\n (F a!1)))\n"
},
"teacher time": 258.0099985599518,
"learner time": 1.5690507888793945
},
{
"part": [
[-Infinity, Infinity
],
[
-1.2,
-0.6
],
[
0.20943951023931956,
0.2617993877991494
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 51,
"formula": "(ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 16655363.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 5563872433930241.0 288230376151711744.0)))\n (and (>= (+ x_2 z_1) (/ 3791960322080769.0 18014398509481984.0))\n (>= (+ x_1 x_2 z_0 z_1) (- (/ 8205283.0 4194304.0)))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 16655363.0 16777216.0)))\n (>= (+ x_2 z_1) (- (/ 5563872433930241.0 288230376151711744.0)))\n (and (>= (+ x_2 z_1) (/ 3791960322080769.0 18014398509481984.0))\n (>= (+ x_1 x_2 z_0 z_1) (- (/ 8205283.0 4194304.0)))))))\n (F a!1)))\n"
},
"teacher time": 1422.0493354797363,
"learner time": 7.312782526016235
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
-0.2617993877991494,
-0.20943951023931953
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.013913393020629883,
"learner time": 0.07054328918457031
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
-0.20943951023931953,
-0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.012648344039916992,
"learner time": 0.06947946548461914
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
-0.15707963267948966,
-0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.014474868774414062,
"learner time": 0.07025718688964844
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
-0.10471975511965975,
-0.052359877559829876
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011543035507202148,
"learner time": 0.0719747543334961
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
-0.052359877559829876,
0.0
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.01175689697265625,
"learner time": 0.07247447967529297
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
0.0,
0.052359877559829904
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011318445205688477,
"learner time": 0.07349658012390137
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
0.052359877559829904,
0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.010420083999633789,
"learner time": 0.0706636905670166
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
0.10471975511965975,
0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.010987997055053711,
"learner time": 0.07183670997619629
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
0.15707963267948966,
0.20943951023931956
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.012183904647827148,
"learner time": 0.07227158546447754
},
{
"part": [
[-Infinity, Infinity
],
[
-0.6,
0.0
],
[
0.20943951023931956,
0.2617993877991494
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.010707855224609375,
"learner time": 0.06902384757995605
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
-0.2617993877991494,
-0.20943951023931953
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011021614074707031,
"learner time": 0.06873083114624023
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
-0.20943951023931953,
-0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.01100921630859375,
"learner time": 0.06693124771118164
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
-0.15707963267948966,
-0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011572837829589844,
"learner time": 0.06851840019226074
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
-0.10471975511965975,
-0.052359877559829876
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011268854141235352,
"learner time": 0.07213139533996582
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
-0.052359877559829876,
0.0
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.010118722915649414,
"learner time": 0.07128500938415527
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
0.0,
0.052359877559829904
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011667966842651367,
"learner time": 0.07077693939208984
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
0.052359877559829904,
0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.010200023651123047,
"learner time": 0.06936168670654297
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
0.10471975511965975,
0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.011373281478881836,
"learner time": 0.07111477851867676
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
0.15707963267948966,
0.20943951023931956
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.009887218475341797,
"learner time": 0.07155394554138184
},
{
"part": [
[-Infinity, Infinity
],
[
0.0,
0.5999999999999999
],
[
0.20943951023931956,
0.2617993877991494
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 0,
"formula": "true",
"smtlib": "(declare-fun F (Bool) Bool)\n(assert (F true))\n"
},
"teacher time": 0.009752988815307617,
"learner time": 0.07022809982299805
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
-0.2617993877991494,
-0.20943951023931953
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 6,
"formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 10790785.0 8388608.0)))))\n (and (not (>= (+ x_2 z_1) (/ 817089.0 16777216.0))) a!1))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 10790785.0 8388608.0)))))\n(let ((a!2 (and (not (>= (+ x_2 z_1) (/ 817089.0 16777216.0))) a!1)))\n (F a!2))))\n"
},
"teacher time": 135.31647491455078,
"learner time": 0.6360189914703369
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
-0.20943951023931953,
-0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 12,
"formula": "(and (not (>= (+ x_2 z_1) (/ 3869897.0 67108864.0)))\n (not (>= (+ x_1 x_2 z_0 z_1) (/ 6401825.0 8388608.0))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (and (not (>= (+ x_2 z_1) (/ 3869897.0 67108864.0)))\n (not (>= (+ x_1 x_2 z_0 z_1) (/ 6401825.0 8388608.0))))))\n (F a!1)))\n"
},
"teacher time": 203.54337358474731,
"learner time": 1.2637457847595215
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
-0.15707963267948966,
-0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 17,
"formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 7285475.0 8388608.0)))))\n (and (not (>= (+ x_2 z_1) (/ 7898579075072001.0 144115188075855872.0))) a!1))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 7285475.0 8388608.0)))))\n(let ((a!2 (and (not (>= (+ x_2 z_1)\n (/ 7898579075072001.0 144115188075855872.0)))\n a!1)))\n (F a!2))))\n"
},
"teacher time": 389.7571222782135,
"learner time": 1.683793067932129
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
-0.10471975511965975,
-0.052359877559829876
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 29,
"formula": "(let ((a!1 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (/ 1141329.0 1048576.0))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 8538102389800961.0 4503599627370496.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 3488115.0 4194304.0)))))\n (ite (>= (+ x_2 z_1) (/ 8893527.0 268435456.0)) a!1 a!2))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (/ 1141329.0 1048576.0))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 8538102389800961.0 4503599627370496.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 3488115.0 4194304.0)))))\n (F (ite (>= (+ x_2 z_1) (/ 8893527.0 268435456.0)) a!1 a!2))))\n"
},
"teacher time": 720.2763946056366,
"learner time": 3.5719165802001953
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
-0.052359877559829876,
0.0
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 28,
"formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_1) (/ 9178179.0 8388608.0)))))\n(let ((a!2 (and (>= x_1 (/ 4635998973591553.0 4503599627370496.0))\n a!1\n (>= (+ x_1 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 3163805517348865.0 2251799813685248.0)))))\n(let ((a!3 (ite (>= (+ x_2 z_1) (- (/ 5616965745901567.0 288230376151711744.0)))\n a!2\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) z_1)\n (/ 5413797686673407.0 4503599627370496.0)))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (/ 6799653710331905.0 36028797018963968.0))\n a!3\n (not (>= (+ x_2 z_1) (/ 369863.0 4194304.0)))))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_1) (/ 9178179.0 8388608.0)))))\n(let ((a!2 (and (>= x_1 (/ 4635998973591553.0 4503599627370496.0))\n a!1\n (>= (+ x_1 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 3163805517348865.0 2251799813685248.0)))))\n(let ((a!3 (ite (>= (+ x_2 z_1) (- (/ 5616965745901567.0 288230376151711744.0)))\n a!2\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) z_1)\n (/ 5413797686673407.0 4503599627370496.0)))))\n(let ((a!4 (ite (>= (+ x_1 x_2 z_0 z_1)\n (/ 6799653710331905.0 36028797018963968.0))\n a!3\n (not (>= (+ x_2 z_1) (/ 369863.0 4194304.0))))))\n (F a!4))))))\n"
},
"teacher time": 492.2216827869415,
"learner time": 3.308640956878662
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
0.0,
0.052359877559829904
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 9,
"formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 2291043.0 4194304.0)))))\n (ite (>= (+ x_2 z_1) (/ 5778770048843775.0 144115188075855872.0))\n (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1)) (/ 1969297.0 524288.0))\n a!1))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1) (/ 2291043.0 4194304.0)))))\n(let ((a!2 (ite (>= (+ x_2 z_1) (/ 5778770048843775.0 144115188075855872.0))\n (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 1969297.0 524288.0))\n a!1)))\n (F a!2))))\n"
},
"teacher time": 111.66231417655945,
"learner time": 0.9715366363525391
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
0.052359877559829904,
0.10471975511965975
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 29,
"formula": "(ite (>= (+ x_2 z_1) (/ 7720110299021313.0 288230376151711744.0))\n (not (>= (+ x_1 x_2) (/ 3616565.0 4194304.0)))\n (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 6727276532072449.0 18014398509481984.0)))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (ite (>= (+ x_2 z_1) (/ 7720110299021313.0 288230376151711744.0))\n (not (>= (+ x_1 x_2) (/ 3616565.0 4194304.0)))\n (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 6727276532072449.0 18014398509481984.0)))))\n (F a!1)))\n"
},
"teacher time": 382.561336517334,
"learner time": 3.201096296310425
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
0.10471975511965975,
0.15707963267948966
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 19,
"formula": "(let ((a!1 (or (not (>= (+ x_1 x_2 z_0 z_1)\n (/ 8759615328092159.0 18014398509481984.0)))\n (>= (+ x_1 x_2 z_1) (/ 4834355595706369.0 4503599627370496.0))))\n (a!3 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (- (/ 11902523.0 4194304.0))))))\n(let ((a!2 (and (not (>= (+ x_1 x_2 z_1)\n (/ 4835611336769535.0 4503599627370496.0)))\n a!1)))\n (ite (>= (+ x_1 z_0 z_1) (- (/ 8881287993491455.0 288230376151711744.0)))\n (or a!2 (not (>= x_1 (/ 13799907.0 16777216.0))) a!3)\n (not (>= (+ x_2 z_1) (/ 5903022915846143.0 36028797018963968.0))))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (or (not (>= (+ x_1 x_2 z_0 z_1)\n (/ 8759615328092159.0 18014398509481984.0)))\n (>= (+ x_1 x_2 z_1) (/ 4834355595706369.0 4503599627370496.0))))\n (a!3 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (- (/ 11902523.0 4194304.0))))))\n(let ((a!2 (and (not (>= (+ x_1 x_2 z_1)\n (/ 4835611336769535.0 4503599627370496.0)))\n a!1)))\n(let ((a!4 (ite (>= (+ x_1 z_0 z_1)\n (- (/ 8881287993491455.0 288230376151711744.0)))\n (or a!2 (not (>= x_1 (/ 13799907.0 16777216.0))) a!3)\n (not (>= (+ x_2 z_1) (/ 5903022915846143.0 36028797018963968.0))))))\n (F a!4)))))\n"
},
"teacher time": 443.42704153060913,
"learner time": 2.6742238998413086
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
0.15707963267948966,
0.20943951023931956
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 27,
"formula": "(let ((a!1 (and (not (>= (+ x_1 x_2 z_0 z_1) (/ 2023829.0 33554432.0)))\n (not (>= (+ x_2 z_1) (/ 9882057.0 67108864.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (/ 3635245823819777.0 288230376151711744.0))\n a!1\n (not (>= (+ x_1 x_2 z_1)\n (/ 4936071158693889.0 4503599627370496.0))))))\n (ite (>= x_1 (/ 7416223.0 8388608.0))\n a!2\n (not (>= (+ x_2 z_1) (/ 4143406758494209.0 18014398509481984.0))))))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_0 () Real)\n(assert (let ((a!1 (and (not (>= (+ x_1 x_2 z_0 z_1) (/ 2023829.0 33554432.0)))\n (not (>= (+ x_2 z_1) (/ 9882057.0 67108864.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (/ 3635245823819777.0 288230376151711744.0))\n a!1\n (not (>= (+ x_1 x_2 z_1)\n (/ 4936071158693889.0 4503599627370496.0))))))\n(let ((a!3 (ite (>= x_1 (/ 7416223.0 8388608.0))\n a!2\n (not (>= (+ x_2 z_1) (/ 4143406758494209.0 18014398509481984.0))))))\n (F a!3)))))\n"
},
"teacher time": 488.5836305618286,
"learner time": 3.8963794708251953
},
{
"part": [
[-Infinity, Infinity
],
[
0.5999999999999999,
1.2
],
[
0.20943951023931956,
0.2617993877991494
]
],
"feature_domain": "concat",
"ultimate_bound": 1.0,
"status": "found",
"result": {
"k": 11,
"formula": "(let ((a!1 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (/ 5246898478776321.0 4503599627370496.0))\n (not (>= (+ x_2 z_1) (/ 1219789.0 33554432.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5683256418631681.0 4503599627370496.0))))))\n (ite (>= (+ x_1 x_2 z_1) (/ 7640609.0 8388608.0))\n (or (not (>= x_1 (/ 14019355.0 16777216.0))) a!1)\n a!2))",
"smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(assert (let ((a!1 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (/ 5246898478776321.0 4503599627370496.0))\n (not (>= (+ x_2 z_1) (/ 1219789.0 33554432.0)))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5683256418631681.0 4503599627370496.0))))))\n(let ((a!3 (ite (>= (+ x_1 x_2 z_1) (/ 7640609.0 8388608.0))\n (or (not (>= x_1 (/ 14019355.0 16777216.0))) a!1)\n a!2)))\n (F a!3))))\n"
},
"teacher time": 163.59390830993652,
"learner time": 1.5178344249725342
}
]
\ No newline at end of file
0.6055230891767955,0.21039086439996335,0.41660669445991516,0.22222109138965607,true
0.6055231308302278,0.2103910681374018,0.4319450855255127,0.22146469354629517,true
0.6055247436131437,0.21039091470996776,0.4349457919597626,0.2213125377893448,true
0.6055203200924332,0.21039087102765186,0.46679142117500305,0.22158028185367584,true
0.605524139763951,0.21039094606112468,0.45684000849723816,0.22265802323818207,true
0.6055251112842444,0.2103909370347489,0.5138310790061951,0.21427631378173828,true
0.6055228794384323,0.21039093882307164,0.5476254224777222,0.21333089470863342,true
0.6055245435957852,0.21039093926453098,0.5404915809631348,0.213500514626503,true
0.6055230941911608,0.21039086431977685,0.629214882850647,0.20345115661621094,true
0.6055233205873297,0.21039101272290037,0.6191551685333252,0.20404589176177979,true
0.6055248965782742,0.21039091636522184,0.6303674578666687,0.20380684733390808,true
0.605523091765521,0.210390864379101,0.3413231670856476,0.23133814334869385,true
0.6055236907723393,0.21039085033813243,0.34430718421936035,0.23088113963603973,true
0.6055247295537862,0.21039091559982628,0.35675135254859924,0.22908948361873627,true
0.6055117615384152,0.21039159125324042,0.3991245627403259,0.22196000814437866,true
0.6055234055177661,0.21039096487954473,0.38797274231910706,0.22354239225387573,true
0.6055249645141116,0.21039092212475294,0.4026753604412079,0.223615363240242,true
0.6055230913494918,0.21039086430214535,0.4473547339439392,0.22048208117485046,true
0.6055237403619909,0.21039084787818607,0.4783157408237457,0.21772371232509613,true
0.6055247717431921,0.21039091357766102,0.4654044508934021,0.21957902610301971,true
0.6055197425796124,0.21039095045995423,0.6336061358451843,0.20569558441638947,true
0.6055241242678288,0.21039094232234734,0.6589073538780212,0.20441529154777527,true
0.6055250981006555,0.21039093578865645,0.34754717350006104,0.23068495094776154,true
0.6055227443589818,0.21039077382949142,0.34882164001464844,0.23074336349964142,true
0.605524426361987,0.2103909575928097,0.3615712523460388,0.22928206622600555,true
0.605523080091767,0.21039086451450312,0.6026841998100281,0.20679321885108948,true
0.6055230601091428,0.210391056720414,0.6256061792373657,0.20366592705249786,true
0.6055246869831761,0.21039091906619864,0.6534552574157715,0.20219114422798157,true
1.127661616009935,0.2244975299732123,-0.9664855599403381,0.24766840040683746,false
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment