Skip to content
Snippets Groups Projects
Commit 93b17818 authored by chsieh16's avatar chsieh16
Browse files

Add result

parent e324e757
No related branches found
No related tags found
No related merge requests found
Showing
with 18558 additions and 0 deletions
[{"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.2617993877991494, -0.20943951023931953]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.20943951023931953, -0.15707963267948966]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.15707963267948966, -0.10471975511965975]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.10471975511965975, -0.052359877559829876]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.052359877559829876, 0.0]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 63, "formula": "(let ((a!1 (ite (>= (+ x_2 z_1) (/ 7774625285684619.0 36028797018963968.0))\n (>= (+ x_2 z_0 z_1)\n (- (/ 8913446019858169.0 9007199254740992.0)))\n (not (<= (+ z_0 z_1)\n (- (/ 8302005809248959.0 18014398509481984.0))))))\n (a!3 (or (>= (+ x_2 z_1) (/ 622075371057253.0 9007199254740992.0))\n (and (<= z_0 (/ 4441347270441279.0 9007199254740992.0))\n (>= (+ x_2 z_0 z_1)\n (/ 7470480989889631.0 18014398509481984.0))))))\n(let ((a!2 (and (>= (+ x_2 z_1) (/ 7158903232693691.0 72057594037927936.0))\n (or (not (<= z_0 (- (/ 8349524189637271.0 18014398509481984.0))))\n a!1))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 8417199781237767.0 9007199254740992.0)))\n a!2\n a!3)))\n (ite (>= (+ x_1 z_0 z_1) (- (/ 2667807219184641.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (- (/ 5351456660706491.0 144115188075855872.0)))\n a!4))))", "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) (/ 7774625285684619.0 36028797018963968.0))\n (>= (+ x_2 z_0 z_1)\n (- (/ 8913446019858169.0 9007199254740992.0)))\n (not (<= (+ z_0 z_1)\n (- (/ 8302005809248959.0 18014398509481984.0))))))\n (a!3 (or (>= (+ x_2 z_1) (/ 622075371057253.0 9007199254740992.0))\n (and (<= z_0 (/ 4441347270441279.0 9007199254740992.0))\n (>= (+ x_2 z_0 z_1)\n (/ 7470480989889631.0 18014398509481984.0))))))\n(let ((a!2 (and (>= (+ x_2 z_1) (/ 7158903232693691.0 72057594037927936.0))\n (or (not (<= z_0 (- (/ 8349524189637271.0 18014398509481984.0))))\n a!1))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 8417199781237767.0 9007199254740992.0)))\n a!2\n a!3)))\n (F (ite (>= (+ x_1 z_0 z_1) (- (/ 2667807219184641.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (- (/ 5351456660706491.0 144115188075855872.0)))\n a!4))))))\n"}, "teacher time": 2234.6442456245422, "learner time": 7.990983963012695}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.0, 0.052359877559829904]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 86, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 2729824488213309.0 18014398509481984.0)))))\n(let ((a!2 (or (not (<= (+ z_0 z_1) (- (/ 332291343106091.0 281474976710656.0))))\n (and (not (>= x_1 (- (/ 1558125900500085.0 2251799813685248.0))))\n (or a!1\n (>= x_1 (- (/ 6237300836323415.0 9007199254740992.0))))))))\n(let ((a!3 (or (not (<= (+ z_0 z_1)\n (- (/ 8078738957002141.0 18014398509481984.0))))\n (and (>= (+ x_2 z_1) (/ 7943935411515837.0 36028797018963968.0))\n a!2))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5669212275727273.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 6209872293296863.0 72057594037927936.0))\n a!3)\n (>= (+ x_2 z_1) (- (/ 4811800765709819.0 36028797018963968.0))))))\n (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 1438918095343383.0 4503599627370496.0)))\n a!4\n (>= (+ x_2 z_1) (- (/ 2848382649123763.0 72057594037927936.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 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 2729824488213309.0 18014398509481984.0)))))\n(let ((a!2 (or (not (<= (+ z_0 z_1) (- (/ 332291343106091.0 281474976710656.0))))\n (and (not (>= x_1 (- (/ 1558125900500085.0 2251799813685248.0))))\n (or a!1\n (>= x_1 (- (/ 6237300836323415.0 9007199254740992.0))))))))\n(let ((a!3 (or (not (<= (+ z_0 z_1)\n (- (/ 8078738957002141.0 18014398509481984.0))))\n (and (>= (+ x_2 z_1) (/ 7943935411515837.0 36028797018963968.0))\n a!2))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5669212275727273.0 4503599627370496.0)))\n (and (>= (+ x_2 z_1) (/ 6209872293296863.0 72057594037927936.0))\n a!3)\n (>= (+ x_2 z_1) (- (/ 4811800765709819.0 36028797018963968.0))))))\n(let ((a!5 (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 1438918095343383.0 4503599627370496.0)))\n a!4\n (>= (+ x_2 z_1) (- (/ 2848382649123763.0 72057594037927936.0))))))\n (F a!5)))))))\n"}, "teacher time": 3624.2691645622253, "learner time": 11.493645429611206}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.052359877559829904, 0.10471975511965975]], "status": "exception", "result": "Traceback (most recent call last):\n File \"/home/chsieh16/cs598mp-fall2021-proj/dtree_synth.py\", line 220, in synth_dtree_per_part\n found, ret, time_info = synth_dtree(learner, teacher,\n File \"/home/chsieh16/cs598mp-fall2021-proj/dtree_synth.py\", line 63, in synth_dtree\n learner.add_negative_examples(*negative_examples)\n File \"/home/chsieh16/cs598mp-fall2021-proj/dtree_learner.py\", line 149, in add_negative_examples\n raise ValueError(f\"All negative examples {args} are repeated.\")\nValueError: All negative examples ((-0.13999966004024794, -0.7438512332452196, 0.052359877559829904, -1.2744555999999998, 0.14757072244016994), (-0.13999966280884354, -0.7522912037117263, 0.052359877559829904, -1.2742973446765287, 0.14757072244016994), (-0.13999966119292942, -0.7522892090762274, 0.05253612464662458, -1.2743897117263179, 0.14739447535337527), (-0.1399996679336559, -0.7776587431563334, 0.0526785113728342, -1.27400440596717, 0.14725208862716563), (-0.13999967786586873, -0.8018973851144436, 0.052359877559829904, -1.2734366720822436, 0.14757072244016994)) are repeated.\n"}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.10471975511965975, 0.15707963267948966]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.15707963267948966, 0.20943951023931956]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 43, "formula": "(let ((a!1 (or (>= (+ x_2 z_0) (- (/ 7729036247376673.0 18014398509481984.0)))\n (and (>= x_2 (/ 5668071964301623.0 36028797018963968.0))\n (not (>= x_2 (/ 1418814026606801.0 9007199254740992.0)))))))\n(let ((a!2 (ite (>= (+ x_2 z_0 z_1) (/ 4061771283767537.0 9007199254740992.0))\n (>= (+ x_2 z_1) (- (/ 2261581992363867.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1) (/ 8151954876864229.0 72057594037927936.0))\n a!1))))\n (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 2829465278888993.0 2251799813685248.0)))\n a!2\n (>= (+ x_2 z_1) (- (/ 1738073123327185.0 72057594037927936.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 (>= (+ x_2 z_0) (- (/ 7729036247376673.0 18014398509481984.0)))\n (and (>= x_2 (/ 5668071964301623.0 36028797018963968.0))\n (not (>= x_2 (/ 1418814026606801.0 9007199254740992.0)))))))\n(let ((a!2 (ite (>= (+ x_2 z_0 z_1) (/ 4061771283767537.0 9007199254740992.0))\n (>= (+ x_2 z_1) (- (/ 2261581992363867.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1) (/ 8151954876864229.0 72057594037927936.0))\n a!1))))\n(let ((a!3 (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 2829465278888993.0 2251799813685248.0)))\n a!2\n (>= (+ x_2 z_1) (- (/ 1738073123327185.0 72057594037927936.0))))))\n (F a!3)))))\n"}, "teacher time": 1496.6986649036407, "learner time": 4.5702433586120605}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.20943951023931956, 0.2617993877991494]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 57, "formula": "(let ((a!1 (or (>= (+ x_2 z_0 z_1)\n (- (/ 5149851762379355.0 9007199254740992.0)))\n (and (not (<= z_0 (- (/ 5246157637530971.0 4503599627370496.0))))\n (>= (+ x_2 z_1) (/ 6512821153606761.0 36028797018963968.0))))))\n (ite (>= (+ x_2 z_0 z_1) (/ 313773611043255.0 562949953421312.0))\n (>= (+ x_2 z_1) (- (/ 3108465887892379.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1) (/ 1575396259315129.0 18014398509481984.0)) a!1)))", "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(assert (let ((a!1 (or (>= (+ x_2 z_0 z_1)\n (- (/ 5149851762379355.0 9007199254740992.0)))\n (and (not (<= z_0 (- (/ 5246157637530971.0 4503599627370496.0))))\n (>= (+ x_2 z_1) (/ 6512821153606761.0 36028797018963968.0))))))\n(let ((a!2 (ite (>= (+ x_2 z_0 z_1) (/ 313773611043255.0 562949953421312.0))\n (>= (+ x_2 z_1) (- (/ 3108465887892379.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1) (/ 1575396259315129.0 18014398509481984.0))\n a!1))))\n (F a!2))))\n"}, "teacher time": 1641.5096249580383, "learner time": 6.412431478500366}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.2617993877991494, -0.20943951023931953]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.20943951023931953, -0.15707963267948966]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.15707963267948966, -0.10471975511965975]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.10471975511965975, -0.052359877559829876]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.052359877559829876, 0.0]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.0, 0.052359877559829904]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.052359877559829904, 0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 63, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 3320989010514217.0 4611686018427387904.0)))))\n (a!3 (and (>= (+ x_2 z_1) (/ 7857419461234199.0 576460752303423488.0))\n (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 3214945034314255.0 18014398509481984.0)))))\n (a!6 (not (>= (+ x_1 x_2 (* (- 1.0) z_1))\n (- (/ 1732478031294125.0 4503599627370496.0)))))\n (a!7 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (/ 4288955907402197.0 144115188075855872.0))))\n (a!8 (not (>= (+ x_2 (* (- 1.0) z_0) z_1)\n (- (/ 8550898143375515.0 36028797018963968.0))))))\n(let ((a!2 (and a!1\n (or (>= (+ x_1 z_0)\n (- (/ 8261860722170579.0 36028797018963968.0)))\n (>= (+ x_2 z_1)\n (/ 3232742323292901.0 1152921504606846976.0)))))\n (a!4 (or (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 8432699910147281.0 144115188075855872.0)))\n (ite (>= (+ x_1 x_2) (/ 6890591016685943.0 144115188075855872.0))\n (not (>= x_2 (/ 6744086398791789.0 72057594037927936.0)))\n a!3)))\n (a!9 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5591542475977701.0 144115188075855872.0)))\n (or a!6 a!7)\n (and a!8\n (>= (+ x_2 z_1)\n (- (/ 3958305225640357.0 144115188075855872.0)))))))\n(let ((a!5 (and (not (>= (+ x_2 z_1)\n (/ 7698607406278367.0 288230376151711744.0)))\n (ite (>= (+ x_2 z_0)\n (/ 4543392713102001.0 1152921504606846976.0))\n a!2\n a!4))))\n (ite (>= (+ x_2 z_1) (- (/ 3284270420559047.0 576460752303423488.0))) a!5 a!9))))", "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_0 z_1)\n (- (/ 3320989010514217.0 4611686018427387904.0)))))\n (a!3 (and (>= (+ x_2 z_1) (/ 7857419461234199.0 576460752303423488.0))\n (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 3214945034314255.0 18014398509481984.0)))))\n (a!6 (not (>= (+ x_1 x_2 (* (- 1.0) z_1))\n (- (/ 1732478031294125.0 4503599627370496.0)))))\n (a!7 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (/ 4288955907402197.0 144115188075855872.0))))\n (a!8 (not (>= (+ x_2 (* (- 1.0) z_0) z_1)\n (- (/ 8550898143375515.0 36028797018963968.0))))))\n(let ((a!2 (and a!1\n (or (>= (+ x_1 z_0)\n (- (/ 8261860722170579.0 36028797018963968.0)))\n (>= (+ x_2 z_1)\n (/ 3232742323292901.0 1152921504606846976.0)))))\n (a!4 (or (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 8432699910147281.0 144115188075855872.0)))\n (ite (>= (+ x_1 x_2) (/ 6890591016685943.0 144115188075855872.0))\n (not (>= x_2 (/ 6744086398791789.0 72057594037927936.0)))\n a!3)))\n (a!9 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5591542475977701.0 144115188075855872.0)))\n (or a!6 a!7)\n (and a!8\n (>= (+ x_2 z_1)\n (- (/ 3958305225640357.0 144115188075855872.0)))))))\n(let ((a!5 (and (not (>= (+ x_2 z_1)\n (/ 7698607406278367.0 288230376151711744.0)))\n (ite (>= (+ x_2 z_0)\n (/ 4543392713102001.0 1152921504606846976.0))\n a!2\n a!4))))\n (F (ite (>= (+ x_2 z_1) (- (/ 3284270420559047.0 576460752303423488.0)))\n a!5\n a!9))))))\n"}, "teacher time": 3605.0249140262604, "learner time": 9.754810810089111}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.10471975511965975, 0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 41, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (/ 6117877804140521.0 72057594037927936.0))))\n (a!3 (or (not (>= x_2 (/ 2074545338111349.0 18014398509481984.0)))\n (and (>= x_2 (/ 8586793633845509.0 72057594037927936.0))\n (not (>= x_2 (/ 2159187790948001.0 18014398509481984.0)))))))\n(let ((a!2 (and (not (>= (+ x_2 z_1)\n (/ 3387603316252445.0 144115188075855872.0)))\n (>= (+ x_2 z_1) (- (/ 7125743769069317.0 288230376151711744.0)))\n a!1)))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 2603504823705045.0 9007199254740992.0)))\n a!2\n (and (>= x_2 (/ 4149061853185083.0 36028797018963968.0)) a!3))))", "smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun x_2 () Real)\n(declare-fun z_1 () 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_0 z_1)\n (/ 6117877804140521.0 72057594037927936.0))))\n (a!3 (or (not (>= x_2 (/ 2074545338111349.0 18014398509481984.0)))\n (and (>= x_2 (/ 8586793633845509.0 72057594037927936.0))\n (not (>= x_2 (/ 2159187790948001.0 18014398509481984.0)))))))\n(let ((a!2 (and (not (>= (+ x_2 z_1)\n (/ 3387603316252445.0 144115188075855872.0)))\n (>= (+ x_2 z_1) (- (/ 7125743769069317.0 288230376151711744.0)))\n a!1)))\n (F (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 2603504823705045.0 9007199254740992.0)))\n a!2\n (and (>= x_2 (/ 4149061853185083.0 36028797018963968.0)) a!3))))))\n"}, "teacher time": 1309.0546045303345, "learner time": 4.959433555603027}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.15707963267948966, 0.20943951023931956]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 13, "formula": "(let ((a!1 (not (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (/ 3165084782119711.0 2251799813685248.0)))))\n (and (not (>= (+ x_1 x_2 z_1) (- (/ 2579101258476205.0 72057594037927936.0))))\n (>= (+ x_2 z_1) (- (/ 4773282378816845.0 288230376151711744.0)))\n (>= (+ x_1 x_2 z_0 z_1) (- (/ 8673358223003123.0 18014398509481984.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 x_2 z_0 (* (- 1.0) z_1))\n (/ 3165084782119711.0 2251799813685248.0)))))\n(let ((a!2 (and (not (>= (+ x_1 x_2 z_1)\n (- (/ 2579101258476205.0 72057594037927936.0))))\n (>= (+ x_2 z_1) (- (/ 4773282378816845.0 288230376151711744.0)))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 8673358223003123.0 18014398509481984.0)))\n a!1)))\n (F a!2))))\n"}, "teacher time": 582.9290719032288, "learner time": 1.3278286457061768}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.20943951023931956, 0.2617993877991494]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 26, "formula": "(let ((a!1 (and (not (>= (+ x_1 z_1)\n (- (/ 733217319353327.0 2251799813685248.0))))\n (or (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5346978821668989.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (/ 2537140680316039.0 9007199254740992.0)))))\n (a!2 (and (not (>= (+ x_1 x_2 z_0 z_1)\n (/ 940202758227275.0 1125899906842624.0)))\n (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (/ 3396798946115595.0 36028797018963968.0))))\n (a!3 (and (>= (+ x_2 z_1) (- (/ 2063381455067053.0 36028797018963968.0)))\n (not (>= (+ x_1 z_1)\n (- (/ 1685677975046379.0 4503599627370496.0))))\n (>= (+ x_1 z_0 z_1)\n (- (/ 6692561616174969.0 9007199254740992.0))))))\n (ite (>= (+ x_2 z_1) (- (/ 3094395201504593.0 288230376151711744.0)))\n a!1\n (ite (>= (+ x_2 z_1) (- (/ 1028967310766863.0 72057594037927936.0)))\n a!2\n a!3)))", "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 (and (not (>= (+ x_1 z_1)\n (- (/ 733217319353327.0 2251799813685248.0))))\n (or (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5346978821668989.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (/ 2537140680316039.0 9007199254740992.0)))))\n (a!2 (and (not (>= (+ x_1 x_2 z_0 z_1)\n (/ 940202758227275.0 1125899906842624.0)))\n (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (/ 3396798946115595.0 36028797018963968.0))))\n (a!3 (and (>= (+ x_2 z_1) (- (/ 2063381455067053.0 36028797018963968.0)))\n (not (>= (+ x_1 z_1)\n (- (/ 1685677975046379.0 4503599627370496.0))))\n (>= (+ x_1 z_0 z_1)\n (- (/ 6692561616174969.0 9007199254740992.0))))))\n(let ((a!4 (ite (>= (+ x_2 z_1) (- (/ 3094395201504593.0 288230376151711744.0)))\n a!1\n (ite (>= (+ x_2 z_1)\n (- (/ 1028967310766863.0 72057594037927936.0)))\n a!2\n a!3))))\n (F a!4))))\n"}, "teacher time": 1473.9741106033325, "learner time": 2.5462939739227295}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.2617993877991494, -0.20943951023931953]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 23, "formula": "(let ((a!1 (and (not (>= (+ x_1 x_2)\n (- (/ 6386385296228111.0 72057594037927936.0))))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (/ 6984270212390891.0 144115188075855872.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (/ 7901962763708669.0 9007199254740992.0)))))\n(let ((a!3 (and (not (<= z_1 (/ 7115514473019693.0 36028797018963968.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 417206601490171.0 1125899906842624.0)))\n a!2)))\n (ite (>= (+ x_2 z_1) (/ 3612310599804081.0 144115188075855872.0)) a!1 a!3)))", "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_1 x_2)\n (- (/ 6386385296228111.0 72057594037927936.0))))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (/ 6984270212390891.0 144115188075855872.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (/ 7901962763708669.0 9007199254740992.0)))))\n(let ((a!3 (and (not (<= z_1 (/ 7115514473019693.0 36028797018963968.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 417206601490171.0 1125899906842624.0)))\n a!2)))\n (F (ite (>= (+ x_2 z_1) (/ 3612310599804081.0 144115188075855872.0)) a!1 a!3)))))\n"}, "teacher time": 922.247231721878, "learner time": 2.3628642559051514}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.20943951023931953, -0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 24, "formula": "(let ((a!1 (and (>= (+ x_1 x_2 z_1) (/ 4965793752891583.0 576460752303423488.0))\n (not (>= (+ x_2 z_1) (/ 6032917577314161.0 72057594037927936.0)))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 1574570569359447.0 2251799813685248.0))))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (/ 5867708969735583.0 144115188075855872.0))\n (and (not (>= x_2 (- (/ 904788027017503.0 4503599627370496.0))))\n (>= x_2 (- (/ 3637157499380239.0 18014398509481984.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 (and (>= (+ x_1 x_2 z_1) (/ 4965793752891583.0 576460752303423488.0))\n (not (>= (+ x_2 z_1) (/ 6032917577314161.0 72057594037927936.0)))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 1574570569359447.0 2251799813685248.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (/ 5867708969735583.0 144115188075855872.0))\n (and (not (>= x_2 (- (/ 904788027017503.0 4503599627370496.0))))\n (>= x_2 (- (/ 3637157499380239.0 18014398509481984.0))))\n a!1)))\n (F a!2))))\n"}, "teacher time": 846.3275980949402, "learner time": 2.293952465057373}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.15707963267948966, -0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 33, "formula": "(let ((a!1 (and (not (>= (+ x_2 z_1)\n (- (/ 5889181844528509.0 1152921504606846976.0))))\n (not (>= (+ x_2 z_0)\n (- (/ 1816643643002231.0 36028797018963968.0))))))\n (a!2 (and (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (- (/ 7141098521782859.0 9007199254740992.0)))\n (not (>= (+ x_2 z_1) (/ 2935582065684851.0 36028797018963968.0)))))\n (a!3 (and (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (/ 4890336337451757.0 36028797018963968.0))\n (>= (+ x_1 z_1) (/ 5485192672937123.0 72057594037927936.0)))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 2567557343680953.0 288230376151711744.0)))\n a!1\n (ite (>= (+ x_1 z_1) (/ 5309455730293663.0 36028797018963968.0)) a!2 a!3)))", "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 (and (not (>= (+ x_2 z_1)\n (- (/ 5889181844528509.0 1152921504606846976.0))))\n (not (>= (+ x_2 z_0)\n (- (/ 1816643643002231.0 36028797018963968.0))))))\n (a!2 (and (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (- (/ 7141098521782859.0 9007199254740992.0)))\n (not (>= (+ x_2 z_1) (/ 2935582065684851.0 36028797018963968.0)))))\n (a!3 (and (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (/ 4890336337451757.0 36028797018963968.0))\n (>= (+ x_1 z_1) (/ 5485192672937123.0 72057594037927936.0)))))\n(let ((a!4 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 2567557343680953.0 288230376151711744.0)))\n a!1\n (ite (>= (+ x_1 z_1) (/ 5309455730293663.0 36028797018963968.0))\n a!2\n a!3))))\n (F a!4))))\n"}, "teacher time": 1576.851619720459, "learner time": 3.6407623291015625}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.10471975511965975, -0.052359877559829876]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 50, "formula": "(let ((a!1 (and (not (>= (+ x_2 z_1)\n (/ 2763386825845949.0 2305843009213693952.0)))\n (not (>= (+ x_2 z_0)\n (- (/ 588601916466859.0 9007199254740992.0))))))\n (a!2 (and (>= (+ x_1 z_1) (/ 7025822223992863.0 72057594037927936.0))\n (not (>= (+ x_2 z_1) (/ 1340801953285549.0 36028797018963968.0)))\n (>= (+ x_1 x_2 z_0)\n (- (/ 4930670575714487.0 9007199254740992.0))))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (/ 4428192796361685.0 1152921504606846976.0))\n a!1\n a!2))", "smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun z_0 () Real)\n(declare-fun x_2 () Real)\n(declare-fun x_1 () Real)\n(declare-fun z_1 () Real)\n(assert (let ((a!1 (and (not (>= (+ x_2 z_1)\n (/ 2763386825845949.0 2305843009213693952.0)))\n (not (>= (+ x_2 z_0)\n (- (/ 588601916466859.0 9007199254740992.0))))))\n (a!2 (and (>= (+ x_1 z_1) (/ 7025822223992863.0 72057594037927936.0))\n (not (>= (+ x_2 z_1) (/ 1340801953285549.0 36028797018963968.0)))\n (>= (+ x_1 x_2 z_0)\n (- (/ 4930670575714487.0 9007199254740992.0))))))\n (F (ite (>= (+ x_1 x_2 z_0 z_1) (/ 4428192796361685.0 1152921504606846976.0))\n a!1\n a!2))))\n"}, "teacher time": 2071.5069143772125, "learner time": 8.13667893409729}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.052359877559829876, 0.0]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.0, 0.052359877559829904]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 62, "formula": "(let ((a!1 (and (not (>= (+ x_2 z_1)\n (/ 3056539023900827.0 144115188075855872.0)))\n (>= (+ x_1 x_2) (/ 4524629636190465.0 72057594037927936.0))\n (>= (+ x_2 z_1) (- (/ 4638224830311557.0 36028797018963968.0)))))\n (a!2 (and (not (>= (+ x_2 z_1)\n (- (/ 5038559817194091.0 1152921504606846976.0))))\n (>= (+ x_2 (* (- 1.0) z_0))\n (/ 8451361385851223.0 288230376151711744.0))))\n (a!3 (and (>= (+ x_1 x_2) (/ 2438409166405121.0 36028797018963968.0))\n (not (>= (+ x_2 z_1)\n (/ 4188779999018789.0 288230376151711744.0)))\n (>= (+ x_2 z_1) (- (/ 5709879780362429.0 18014398509481984.0))))))\n (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 7102911599822459.0 36028797018963968.0))\n a!1\n (ite (>= (+ x_1 z_0 z_1) (- (/ 8409308573970689.0 288230376151711744.0)))\n a!2\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 (not (>= (+ x_2 z_1)\n (/ 3056539023900827.0 144115188075855872.0)))\n (>= (+ x_1 x_2) (/ 4524629636190465.0 72057594037927936.0))\n (>= (+ x_2 z_1) (- (/ 4638224830311557.0 36028797018963968.0)))))\n (a!2 (and (not (>= (+ x_2 z_1)\n (- (/ 5038559817194091.0 1152921504606846976.0))))\n (>= (+ x_2 (* (- 1.0) z_0))\n (/ 8451361385851223.0 288230376151711744.0))))\n (a!3 (and (>= (+ x_1 x_2) (/ 2438409166405121.0 36028797018963968.0))\n (not (>= (+ x_2 z_1)\n (/ 4188779999018789.0 288230376151711744.0)))\n (>= (+ x_2 z_1) (- (/ 5709879780362429.0 18014398509481984.0))))))\n(let ((a!4 (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 7102911599822459.0 36028797018963968.0))\n a!1\n (ite (>= (+ x_1 z_0 z_1)\n (- (/ 8409308573970689.0 288230376151711744.0)))\n a!2\n a!3))))\n (F a!4))))\n"}, "teacher time": 2056.3842403888702, "learner time": 9.65384840965271}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.052359877559829904, 0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 26, "formula": "(let ((a!1 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 1871321305646181.0 18014398509481984.0)))\n (and (>= x_2 (/ 6517899772834555.0 72057594037927936.0))\n (not (>= x_2 (/ 6559829366229285.0 72057594037927936.0))))\n (not (>= (+ x_2 z_1)\n (/ 5418415459390295.0 144115188075855872.0)))))\n (a!2 (and (>= (+ x_2 (* (- 1.0) z_0))\n (/ 1019867157215813.0 9007199254740992.0))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 3604705461185333.0 9007199254740992.0))))))\n (ite (>= (+ x_2 z_1) (/ 6426217293060397.0 576460752303423488.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 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 1871321305646181.0 18014398509481984.0)))\n (and (>= x_2 (/ 6517899772834555.0 72057594037927936.0))\n (not (>= x_2 (/ 6559829366229285.0 72057594037927936.0))))\n (not (>= (+ x_2 z_1)\n (/ 5418415459390295.0 144115188075855872.0)))))\n (a!2 (and (>= (+ x_2 (* (- 1.0) z_0))\n (/ 1019867157215813.0 9007199254740992.0))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 3604705461185333.0 9007199254740992.0))))))\n (F (ite (>= (+ x_2 z_1) (/ 6426217293060397.0 576460752303423488.0)) a!1 a!2))))\n"}, "teacher time": 1020.6676380634308, "learner time": 3.170403242111206}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.10471975511965975, 0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 10, "formula": "(and (<= z_1 (- (/ 3464292772435131.0 36028797018963968.0)))\n (not (>= (+ x_1 x_2 z_0 z_1) (/ 4792550579462587.0 36028797018963968.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 (<= z_1 (- (/ 3464292772435131.0 36028797018963968.0)))\n (not (>= (+ x_1 x_2 z_0 z_1)\n (/ 4792550579462587.0 36028797018963968.0))))))\n (F a!1)))\n"}, "teacher time": 367.6673550605774, "learner time": 0.8539254665374756}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.15707963267948966, 0.20943951023931956]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.20943951023931956, 0.2617993877991494]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.2617993877991494, -0.20943951023931953]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 18, "formula": "(let ((a!1 (not (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (/ 786120248492119.0 36028797018963968.0)))))\n(let ((a!2 (and (not (>= (+ x_2 z_1)\n (/ 5894688428218813.0 9223372036854775808.0)))\n a!1)))\n (ite (>= (+ x_2 z_0 z_1) (- (/ 5946508812703655.0 9007199254740992.0)))\n a!2\n (not (>= (+ x_2 z_1) (/ 3659135065561807.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 (not (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (/ 786120248492119.0 36028797018963968.0)))))\n(let ((a!2 (and (not (>= (+ x_2 z_1)\n (/ 5894688428218813.0 9223372036854775808.0)))\n a!1)))\n(let ((a!3 (ite (>= (+ x_2 z_0 z_1)\n (- (/ 5946508812703655.0 9007199254740992.0)))\n a!2\n (not (>= (+ x_2 z_1) (/ 3659135065561807.0 36028797018963968.0))))))\n (F a!3)))))\n"}, "teacher time": 414.1424825191498, "learner time": 1.5012648105621338}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.20943951023931953, -0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 3, "formula": "(and (not (>= (+ x_2 z_0 z_1) (- (/ 5784148641817395.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 7478144315015565.0 72057594037927936.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(assert (let ((a!1 (and (not (>= (+ x_2 z_0 z_1)\n (- (/ 5784148641817395.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 7478144315015565.0 72057594037927936.0))))))\n (F a!1)))\n"}, "teacher time": 76.16948533058167, "learner time": 0.2432873249053955}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.15707963267948966, -0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 7, "formula": "(and (not (>= (+ x_2 z_0 z_1) (- (/ 5882329815853849.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 3122121882826477.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(assert (let ((a!1 (and (not (>= (+ x_2 z_0 z_1)\n (- (/ 5882329815853849.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 3122121882826477.0 36028797018963968.0))))))\n (F a!1)))\n"}, "teacher time": 147.84312558174133, "learner time": 0.5697779655456543}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.10471975511965975, -0.052359877559829876]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 19, "formula": "(let ((a!1 (and (not (>= (+ x_2 z_0 z_1)\n (- (/ 8881353368913527.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 4740114268281187.0 36028797018963968.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4935320091969785.0 18014398509481984.0)))\n a!1\n (not (>= (+ x_2 z_1) (/ 7872565967500971.0 72057594037927936.0))))))\n (ite (>= (+ x_2 z_1) (/ 7993043382428625.0 288230376151711744.0))\n a!2\n (not (>= (+ x_2 z_0 z_1) (- (/ 3781865361167057.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 (and (not (>= (+ x_2 z_0 z_1)\n (- (/ 8881353368913527.0 9007199254740992.0))))\n (not (>= (+ x_2 z_1) (/ 4740114268281187.0 36028797018963968.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4935320091969785.0 18014398509481984.0)))\n a!1\n (not (>= (+ x_2 z_1) (/ 7872565967500971.0 72057594037927936.0))))))\n(let ((a!3 (ite (>= (+ x_2 z_1) (/ 7993043382428625.0 288230376151711744.0))\n a!2\n (not (>= (+ x_2 z_0 z_1)\n (- (/ 3781865361167057.0 18014398509481984.0)))))))\n (F a!3)))))\n"}, "teacher time": 420.12671184539795, "learner time": 1.8325061798095703}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.052359877559829876, 0.0]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 25, "formula": "(ite (<= (+ z_0 z_1) (- (/ 2673068324269335.0 4503599627370496.0)))\n (not (>= (+ x_2 z_1) (/ 5591545358281463.0 72057594037927936.0)))\n (and (not (>= x_2 (- (/ 7186025711089567.0 144115188075855872.0))))\n (>= x_2 (- (/ 7293120589652497.0 144115188075855872.0)))))", "smtlib": "(declare-fun F (Bool) Bool)\n(declare-fun x_2 () Real)\n(declare-fun z_1 () Real)\n(declare-fun z_0 () Real)\n(assert (let ((a!1 (ite (<= (+ z_0 z_1) (- (/ 2673068324269335.0 4503599627370496.0)))\n (not (>= (+ x_2 z_1) (/ 5591545358281463.0 72057594037927936.0)))\n (and (not (>= x_2\n (- (/ 7186025711089567.0 144115188075855872.0))))\n (>= x_2 (- (/ 7293120589652497.0 144115188075855872.0)))))))\n (F a!1)))\n"}, "teacher time": 375.92742395401, "learner time": 2.2922589778900146}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.0, 0.052359877559829904]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.052359877559829904, 0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 26, "formula": "(let ((a!1 (and (not (>= (+ x_2 z_1) (/ 86294283107979.0 2251799813685248.0)))\n (>= (+ x_2 (* (- 1.0) z_0) z_1)\n (/ 2892551702469199.0 4503599627370496.0)))))\n (ite (>= (+ x_2 z_1) (/ 855183849497771.0 36028797018963968.0))\n a!1\n (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 5900679282175607.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(assert (let ((a!1 (and (not (>= (+ x_2 z_1) (/ 86294283107979.0 2251799813685248.0)))\n (>= (+ x_2 (* (- 1.0) z_0) z_1)\n (/ 2892551702469199.0 4503599627370496.0)))))\n(let ((a!2 (ite (>= (+ x_2 z_1) (/ 855183849497771.0 36028797018963968.0))\n a!1\n (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 5900679282175607.0 18014398509481984.0)))))\n (F a!2))))\n"}, "teacher time": 567.6602101325989, "learner time": 2.503000259399414}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.10471975511965975, 0.15707963267948966]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.15707963267948966, 0.20943951023931956]], "status": "skip", "result": "The region contains unsafe datapoints."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.20943951023931956, 0.2617993877991494]], "status": "skip", "result": "The region contains unsafe datapoints."}]
\ No newline at end of file
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.
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