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

Add result for OOPSLA

parent 1613f85f
No related branches found
No related tags found
No related merge requests found
Showing
with 16800 additions and 0 deletions
[{"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.2617993877991494, -0.20943951023931953]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 15, "formula": "(let ((a!1 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5028750869119287.0 4503599627370496.0))))))\n (ite (>= (+ x_1 x_2 z_1) (- (/ 344960756987819.0 562949953421312.0)))\n a!1\n (and (>= x_2 (- (/ 3801900975189303.0 18014398509481984.0)))\n (not (>= x_2 (- (/ 7579979709789667.0 36028797018963968.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(declare-fun x_1 () Real)\n(assert (let ((a!1 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5028750869119287.0 4503599627370496.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_1) (- (/ 344960756987819.0 562949953421312.0)))\n a!1\n (and (>= x_2 (- (/ 3801900975189303.0 18014398509481984.0)))\n (not (>= x_2\n (- (/ 7579979709789667.0 36028797018963968.0))))))))\n (F a!2))))\n"}, "teacher time": 176.1372504234314, "learner time": 0.5803453922271729}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.20943951023931953, -0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 33, "formula": "(let ((a!1 (or (>= x_1 (- (/ 3052260604254825.0 4503599627370496.0)))\n (and (not (>= x_2 (- (/ 6165766560562187.0 36028797018963968.0))))\n (>= x_2 (- (/ 3094832230812433.0 18014398509481984.0)))))))\n (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 2906418285721873.0 4503599627370496.0)))\n (and (not (>= x_1 (- (/ 6103684439698885.0 9007199254740992.0)))) a!1)\n (>= (+ x_2 z_1) (- (/ 276642208986521.0 4503599627370496.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 (or (>= x_1 (- (/ 3052260604254825.0 4503599627370496.0)))\n (and (not (>= x_2 (- (/ 6165766560562187.0 36028797018963968.0))))\n (>= x_2 (- (/ 3094832230812433.0 18014398509481984.0)))))))\n(let ((a!2 (ite (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 2906418285721873.0 4503599627370496.0)))\n (and (not (>= x_1 (- (/ 6103684439698885.0 9007199254740992.0))))\n a!1)\n (>= (+ x_2 z_1) (- (/ 276642208986521.0 4503599627370496.0))))))\n (F a!2))))\n"}, "teacher time": 742.9465644359589, "learner time": 2.1642656326293945}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.15707963267948966, -0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 55, "formula": "(let ((a!1 (or (>= (+ x_2 z_0 z_1)\n (- (/ 5594448018313295.0 9007199254740992.0)))\n (and (>= x_2 (- (/ 1094599889432399.0 9007199254740992.0)))\n (not (>= x_2 (- (/ 8713672645427493.0 72057594037927936.0))))))))\n(let ((a!2 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 2499595521302539.0 4503599627370496.0)))\n (>= (+ x_2 z_1) (/ 6817165769513175.0 144115188075855872.0))\n (and (>= (+ x_2 z_1) (/ 4468785000811071.0 36028797018963968.0))\n a!1))))\n(let ((a!3 (or (not (<= (+ z_0 z_1) (/ 2324360730017531.0 36028797018963968.0)))\n a!2)))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 1521414582957593.0 4503599627370496.0)))\n (>= (+ x_2 z_1) (- (/ 3759455089133291.0 72057594037927936.0)))\n (and (>= (+ x_2 z_1) (/ 8562464396024919.0 1152921504606846976.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 (or (>= (+ x_2 z_0 z_1)\n (- (/ 5594448018313295.0 9007199254740992.0)))\n (and (>= x_2 (- (/ 1094599889432399.0 9007199254740992.0)))\n (not (>= x_2 (- (/ 8713672645427493.0 72057594037927936.0))))))))\n(let ((a!2 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 2499595521302539.0 4503599627370496.0)))\n (>= (+ x_2 z_1) (/ 6817165769513175.0 144115188075855872.0))\n (and (>= (+ x_2 z_1) (/ 4468785000811071.0 36028797018963968.0))\n a!1))))\n(let ((a!3 (or (not (<= (+ z_0 z_1) (/ 2324360730017531.0 36028797018963968.0)))\n a!2)))\n(let ((a!4 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 1521414582957593.0 4503599627370496.0)))\n (>= (+ x_2 z_1) (- (/ 3759455089133291.0 72057594037927936.0)))\n (and (>= (+ x_2 z_1)\n (/ 8562464396024919.0 1152921504606846976.0))\n a!3))))\n (F a!4))))))\n"}, "teacher time": 1979.7605946063995, "learner time": 6.804669380187988}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.10471975511965975, -0.052359877559829876]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 70, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 3840589147788229.0 4503599627370496.0)))))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) z_1)\n (- (/ 191039498637321.0 2251799813685248.0)))))\n (a!5 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6361937956010893.0 4503599627370496.0))))))\n(let ((a!3 (or a!1\n (and a!2\n (>= (+ x_2 z_1) (/ 3002605716203289.0 18014398509481984.0))))))\n(let ((a!4 (ite (>= (+ x_2 z_1) (/ 3479837757196933.0 18014398509481984.0))\n (not (<= (+ z_0 z_1)\n (- (/ 4232133900831671.0 4503599627370496.0))))\n a!3)))\n(let ((a!6 (and (>= (+ x_2 z_1) (/ 2593802448811823.0 36028797018963968.0))\n (or a!4\n (>= (+ x_2 z_0 z_1)\n (- (/ 1780072522516139.0 4503599627370496.0)))\n a!5))))\n (ite (>= (+ x_2 z_0 z_1) (/ 2404137673960757.0 9007199254740992.0))\n (>= (+ x_2 z_1) (- (/ 2517401943581229.0 72057594037927936.0)))\n a!6)))))", "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) z_0) (* (- 1.0) z_1))\n (- (/ 3840589147788229.0 4503599627370496.0)))))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0) z_1)\n (- (/ 191039498637321.0 2251799813685248.0)))))\n (a!5 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6361937956010893.0 4503599627370496.0))))))\n(let ((a!3 (or a!1\n (and a!2\n (>= (+ x_2 z_1) (/ 3002605716203289.0 18014398509481984.0))))))\n(let ((a!4 (ite (>= (+ x_2 z_1) (/ 3479837757196933.0 18014398509481984.0))\n (not (<= (+ z_0 z_1)\n (- (/ 4232133900831671.0 4503599627370496.0))))\n a!3)))\n(let ((a!6 (and (>= (+ x_2 z_1) (/ 2593802448811823.0 36028797018963968.0))\n (or a!4\n (>= (+ x_2 z_0 z_1)\n (- (/ 1780072522516139.0 4503599627370496.0)))\n a!5))))\n (F (ite (>= (+ x_2 z_0 z_1) (/ 2404137673960757.0 9007199254740992.0))\n (>= (+ x_2 z_1) (- (/ 2517401943581229.0 72057594037927936.0)))\n a!6)))))))\n"}, "teacher time": 3634.8293833732605, "learner time": 11.054906129837036}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [-0.052359877559829876, 0.0]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.0, 0.052359877559829904]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.052359877559829904, 0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.10471975511965975, 0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 54, "formula": "(let ((a!1 (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 6789059344670711.0 9007199254740992.0)))\n (and (>= (+ x_2 z_1) (/ 4145968780961005.0 18014398509481984.0))\n (>= (+ x_2 z_0 z_1)\n (- (/ 5585319221868615.0 4503599627370496.0))))\n (>= (+ x_2 z_1) (/ 3434229983914537.0 36028797018963968.0)))))\n (ite (>= (+ x_2 z_0 z_1) (/ 3237686410992625.0 18014398509481984.0))\n (>= (+ x_2 z_1) (- (/ 5159887223501017.0 144115188075855872.0)))\n 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(declare-fun x_1 () Real)\n(assert (let ((a!1 (ite (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 6789059344670711.0 9007199254740992.0)))\n (and (>= (+ x_2 z_1) (/ 4145968780961005.0 18014398509481984.0))\n (>= (+ x_2 z_0 z_1)\n (- (/ 5585319221868615.0 4503599627370496.0))))\n (>= (+ x_2 z_1) (/ 3434229983914537.0 36028797018963968.0)))))\n (F (ite (>= (+ x_2 z_0 z_1) (/ 3237686410992625.0 18014398509481984.0))\n (>= (+ x_2 z_1) (- (/ 5159887223501017.0 144115188075855872.0)))\n a!1))))\n"}, "teacher time": 1748.1200394630432, "learner time": 5.28392219543457}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.15707963267948966, 0.20943951023931956]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-1.2, -0.6], [0.20943951023931956, 0.2617993877991494]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.2617993877991494, -0.20943951023931953]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 60, "formula": "(let ((a!1 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 8059371677164597.0 36028797018963968.0)))\n (and (not (<= z_1 (/ 3051195953302915.0 9007199254740992.0)))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5393546942535925.0 4503599627370496.0)))))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 5600620651962569.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 2005344827677025.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1) (/ 2944857247131819.0 576460752303423488.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 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 8059371677164597.0 36028797018963968.0)))\n (and (not (<= z_1 (/ 3051195953302915.0 9007199254740992.0)))\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5393546942535925.0 4503599627370496.0)))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 5600620651962569.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 2005344827677025.0 36028797018963968.0)))\n (and (>= (+ x_2 z_1)\n (/ 2944857247131819.0 576460752303423488.0))\n a!1))))\n (F a!2))))\n"}, "teacher time": 2895.2021520137787, "learner time": 5.7989561557769775}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.20943951023931953, -0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 30, "formula": "(let ((a!1 (and (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 3909932422330741.0 4503599627370496.0)))\n (not (<= z_1 (/ 7054852787478863.0 36028797018963968.0))))))\n (ite (>= (+ x_1 x_2 z_0 z_1) (- (/ 2950652190901943.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (- (/ 1867620427616393.0 72057594037927936.0)))\n (ite (<= z_1 (/ 596208361129499.0 2251799813685248.0))\n a!1\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 2056551656160153.0 2251799813685248.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 (>= (+ x_1 x_2 z_0 (* (- 1.0) z_1))\n (- (/ 3909932422330741.0 4503599627370496.0)))\n (not (<= z_1 (/ 7054852787478863.0 36028797018963968.0))))))\n(let ((a!2 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 2950652190901943.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (- (/ 1867620427616393.0 72057594037927936.0)))\n (ite (<= z_1 (/ 596208361129499.0 2251799813685248.0))\n a!1\n (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 2056551656160153.0 2251799813685248.0)))))))\n (F a!2))))\n"}, "teacher time": 1689.9155962467194, "learner time": 3.086308002471924}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.15707963267948966, -0.10471975511965975]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 67, "formula": "(let ((a!1 (not (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 279762257772367.0 1125899906842624.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (/ 6067278241031147.0 36028797018963968.0))))\n (a!3 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 2038417461900583.0 9007199254740992.0)))\n (and (>= (+ x_2 z_0 z_1)\n (- (/ 3411846012902595.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (/ 3563184614492783.0 72057594037927936.0)))))\n (a!4 (and (>= (+ x_2 z_0) (- (/ 536705316664803.0 18014398509481984.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 2079402920669431.0 9007199254740992.0))))))\n(let ((a!5 (and a!2\n (ite (>= (+ x_2 z_1)\n (/ 5044403399840191.0 288230376151711744.0))\n a!3\n a!4))))\n (ite (>= (+ x_1 z_0 z_1) (- (/ 2961846338135735.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 8725050539526081.0 576460752303423488.0)))\n (ite (>= (+ x_2 z_1) (/ 5498191862901565.0 72057594037927936.0)) a!1 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_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 279762257772367.0 1125899906842624.0))))\n (a!2 (not (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0))\n (/ 6067278241031147.0 36028797018963968.0))))\n (a!3 (or (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 2038417461900583.0 9007199254740992.0)))\n (and (>= (+ x_2 z_0 z_1)\n (- (/ 3411846012902595.0 9007199254740992.0)))\n (>= (+ x_2 z_1) (/ 3563184614492783.0 72057594037927936.0)))))\n (a!4 (and (>= (+ x_2 z_0) (- (/ 536705316664803.0 18014398509481984.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 2079402920669431.0 9007199254740992.0))))))\n(let ((a!5 (and a!2\n (ite (>= (+ x_2 z_1)\n (/ 5044403399840191.0 288230376151711744.0))\n a!3\n a!4))))\n(let ((a!6 (ite (>= (+ x_1 z_0 z_1)\n (- (/ 2961846338135735.0 18014398509481984.0)))\n (>= (+ x_2 z_1) (- (/ 8725050539526081.0 576460752303423488.0)))\n (ite (>= (+ x_2 z_1) (/ 5498191862901565.0 72057594037927936.0))\n a!1\n a!5))))\n (F a!6)))))\n"}, "teacher time": 3598.6450974941254, "learner time": 7.8077614307403564}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.10471975511965975, -0.052359877559829876]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 33, "formula": "(let ((a!1 (and (>= (+ x_2 z_1) (/ 4654082400916295.0 1152921504606846976.0))\n (not (>= (+ x_2 z_1) (/ 2641253095061739.0 9007199254740992.0)))))\n (a!2 (and (not (>= (+ x_1 z_1) (/ 8956445488380377.0 36028797018963968.0)))\n (>= (+ x_2 z_1) (/ 6708060484076587.0 576460752303423488.0))))\n (a!3 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 1308476015880209.0 18014398509481984.0)))\n (not (>= x_1 (- (/ 1426379353404843.0 36028797018963968.0))))))\n (a!7 (and (>= (+ x_2 z_1) (/ 5679581003221361.0 144115188075855872.0))\n (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 5627400856786765.0 4503599627370496.0)))))\n (a!9 (not (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 6440071806666069.0 72057594037927936.0)))))\n (a!13 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4530158615380995.0 144115188075855872.0)))\n (>= (+ x_2 z_1)\n (- (/ 6307362615150477.0 288230376151711744.0)))\n (and (>= (+ x_2 z_0 z_1)\n (/ 5134137802559533.0 18014398509481984.0))\n (>= (+ x_2 z_1)\n (- (/ 5363787156198261.0 144115188075855872.0)))))))\n(let ((a!4 (ite (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 1382124101162539.0 9007199254740992.0)))\n a!3\n (and (>= (+ x_2 z_1)\n (/ 4815315014571049.0 288230376151711744.0))\n (>= (+ x_1 x_2)\n (- (/ 2400312766797231.0 4503599627370496.0))))))\n (a!10 (ite (>= (+ x_1 x_2 z_0)\n (- (/ 269131848621931.0 562949953421312.0)))\n (or a!9\n (>= (+ x_2 z_1)\n (- (/ 2616954265545833.0 2305843009213693952.0))))\n (>= (+ x_2 (* (- 1.0) z_0))\n (- (/ 5508431247014355.0 288230376151711744.0))))))\n(let ((a!5 (and (>= (+ x_2 z_1) (/ 7889874201588881.0 576460752303423488.0))\n (or (not (<= z_0 (- (/ 986952148979213.0 9007199254740992.0))))\n a!4)))\n (a!11 (and (not (>= (+ x_2 z_1)\n (/ 5197489037797829.0 36028797018963968.0)))\n a!10)))\n(let ((a!6 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 7584335591349259.0 72057594037927936.0)))\n (or (not (>= x_2 (- (/ 2848098381915283.0 36028797018963968.0))))\n a!2\n (not (>= x_1 (- (/ 294112302445039.0 2251799813685248.0)))))\n a!5)))\n(let ((a!8 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 2903942657006707.0 18014398509481984.0)))\n a!1\n (ite (>= x_1 (- (/ 8395439288558239.0 18014398509481984.0)))\n a!6\n a!7))))\n(let ((a!12 (ite (>= (+ x_2 (* (- 1.0) z_0))\n (- (/ 7009503340671093.0 576460752303423488.0)))\n a!8\n a!11)))\n (ite (>= (+ x_2 z_1) (- (/ 5739176380485617.0 1152921504606846976.0)))\n a!12\n a!13)))))))", "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 (and (>= (+ x_2 z_1) (/ 4654082400916295.0 1152921504606846976.0))\n (not (>= (+ x_2 z_1) (/ 2641253095061739.0 9007199254740992.0)))))\n (a!2 (and (not (>= (+ x_1 z_1) (/ 8956445488380377.0 36028797018963968.0)))\n (>= (+ x_2 z_1) (/ 6708060484076587.0 576460752303423488.0))))\n (a!3 (and (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 1308476015880209.0 18014398509481984.0)))\n (not (>= x_1 (- (/ 1426379353404843.0 36028797018963968.0))))))\n (a!7 (and (>= (+ x_2 z_1) (/ 5679581003221361.0 144115188075855872.0))\n (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 5627400856786765.0 4503599627370496.0)))))\n (a!9 (not (>= (+ x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 6440071806666069.0 72057594037927936.0)))))\n (a!13 (ite (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4530158615380995.0 144115188075855872.0)))\n (>= (+ x_2 z_1)\n (- (/ 6307362615150477.0 288230376151711744.0)))\n (and (>= (+ x_2 z_0 z_1)\n (/ 5134137802559533.0 18014398509481984.0))\n (>= (+ x_2 z_1)\n (- (/ 5363787156198261.0 144115188075855872.0)))))))\n(let ((a!4 (ite (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 1382124101162539.0 9007199254740992.0)))\n a!3\n (and (>= (+ x_2 z_1)\n (/ 4815315014571049.0 288230376151711744.0))\n (>= (+ x_1 x_2)\n (- (/ 2400312766797231.0 4503599627370496.0))))))\n (a!10 (ite (>= (+ x_1 x_2 z_0)\n (- (/ 269131848621931.0 562949953421312.0)))\n (or a!9\n (>= (+ x_2 z_1)\n (- (/ 2616954265545833.0 2305843009213693952.0))))\n (>= (+ x_2 (* (- 1.0) z_0))\n (- (/ 5508431247014355.0 288230376151711744.0))))))\n(let ((a!5 (and (>= (+ x_2 z_1) (/ 7889874201588881.0 576460752303423488.0))\n (or (not (<= z_0 (- (/ 986952148979213.0 9007199254740992.0))))\n a!4)))\n (a!11 (and (not (>= (+ x_2 z_1)\n (/ 5197489037797829.0 36028797018963968.0)))\n a!10)))\n(let ((a!6 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 7584335591349259.0 72057594037927936.0)))\n (or (not (>= x_2 (- (/ 2848098381915283.0 36028797018963968.0))))\n a!2\n (not (>= x_1 (- (/ 294112302445039.0 2251799813685248.0)))))\n a!5)))\n(let ((a!8 (ite (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 2903942657006707.0 18014398509481984.0)))\n a!1\n (ite (>= x_1 (- (/ 8395439288558239.0 18014398509481984.0)))\n a!6\n a!7))))\n(let ((a!12 (ite (>= (+ x_2 (* (- 1.0) z_0))\n (- (/ 7009503340671093.0 576460752303423488.0)))\n a!8\n a!11)))\n (F (ite (>= (+ x_2 z_1) (- (/ 5739176380485617.0 1152921504606846976.0)))\n a!12\n a!13)))))))))\n"}, "teacher time": 3617.7398726940155, "learner time": 6.494742393493652}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [-0.052359877559829876, 0.0]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "not found", "result": {"reason": "Reached max time usage 3600.0.", "k": 67, "formula": "(let ((a!1 (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1)))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0))\n (/ 2835053075090657.0 36028797018963968.0))))\n (a!3 (not (>= (+ x_1 x_2 (* (- 1.0) z_1))\n (- (/ 5332496145987291.0 36028797018963968.0)))))\n (a!5 (not (>= (+ x_1 (* (- 1.0) x_2))\n (- (/ 3522630600568237.0 72057594037927936.0)))))\n (a!6 (and (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 7657596547207621.0 36028797018963968.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 8433669805363031.0 144115188075855872.0)))))\n (a!8 (and (not (>= x_2 (- (/ 7953420352619049.0 288230376151711744.0))))\n (not (>= (+ x_1 x_2)\n (- (/ 2145647268308349.0 9007199254740992.0))))))\n (a!9 (and (not (<= z_1 (/ 2329285145994083.0 9007199254740992.0)))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6896487309462081.0 9007199254740992.0)))))\n (a!14 (ite (>= (+ x_2 z_1)\n (- (/ 8568293567152211.0 576460752303423488.0)))\n (not (>= (+ x_1 x_2)\n (- (/ 5675983888126987.0 36028797018963968.0))))\n (and (not (<= z_1 (/ 2447384300030515.0 144115188075855872.0)))\n (<= z_1 (/ 5665879972290989.0 288230376151711744.0))))))\n(let ((a!4 (or (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 3563507432514073.0 18014398509481984.0)))\n a!3))\n (a!7 (and (not (>= (+ x_1 x_2)\n (- (/ 3313437317012967.0 36028797018963968.0))))\n (or (not (>= a!1\n (- (/ 3170974553683589.0 4611686018427387904.0))))\n a!6)))\n (a!10 (and (not (>= (+ x_1 z_1)\n (- (/ 6772477090842733.0 36028797018963968.0))))\n (ite (>= (+ x_1 z_1)\n (- (/ 429854623273669.0 2251799813685248.0)))\n a!8\n a!9))))\n(let ((a!11 (ite (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5502047664758535.0 18014398509481984.0)))\n (ite (>= (+ x_1 x_2)\n (- (/ 6629630116421945.0 72057594037927936.0)))\n a!7\n a!10)\n (and (>= (+ x_2 z_1)\n (/ 4040401307218897.0 576460752303423488.0))\n (>= x_2 (- (/ 1698047291566937.0 36028797018963968.0)))))))\n(let ((a!12 (ite (>= (+ x_1 (* (- 1.0) x_2))\n (- (/ 7055780168714131.0 144115188075855872.0)))\n a!5\n a!11)))\n(let ((a!13 (ite (>= x_1 (- (/ 666203261502095.0 9007199254740992.0)))\n (and (not (>= x_2\n (- (/ 2269729184233765.0 288230376151711744.0))))\n (>= x_2 (- (/ 4539612283488395.0 576460752303423488.0))))\n (ite (>= x_1 (- (/ 2667045390271675.0 36028797018963968.0)))\n (and a!2 a!4)\n a!12))))\n (ite (>= a!1 (- (/ 6351107699626993.0 18014398509481984.0))) a!13 a!14))))))", "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 (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1)))\n (a!2 (not (>= (+ x_1 x_2 (* (- 1.0) z_0))\n (/ 2835053075090657.0 36028797018963968.0))))\n (a!3 (not (>= (+ x_1 x_2 (* (- 1.0) z_1))\n (- (/ 5332496145987291.0 36028797018963968.0)))))\n (a!5 (not (>= (+ x_1 (* (- 1.0) x_2))\n (- (/ 3522630600568237.0 72057594037927936.0)))))\n (a!6 (and (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 7657596547207621.0 36028797018963968.0)))\n (>= (+ x_1 (* (- 1.0) x_2) z_1)\n (- (/ 8433669805363031.0 144115188075855872.0)))))\n (a!8 (and (not (>= x_2 (- (/ 7953420352619049.0 288230376151711744.0))))\n (not (>= (+ x_1 x_2)\n (- (/ 2145647268308349.0 9007199254740992.0))))))\n (a!9 (and (not (<= z_1 (/ 2329285145994083.0 9007199254740992.0)))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_1))\n (- (/ 6896487309462081.0 9007199254740992.0)))))\n (a!14 (ite (>= (+ x_2 z_1)\n (- (/ 8568293567152211.0 576460752303423488.0)))\n (not (>= (+ x_1 x_2)\n (- (/ 5675983888126987.0 36028797018963968.0))))\n (and (not (<= z_1 (/ 2447384300030515.0 144115188075855872.0)))\n (<= z_1 (/ 5665879972290989.0 288230376151711744.0))))))\n(let ((a!4 (or (>= (+ x_1 (* (- 1.0) x_2) z_0)\n (- (/ 3563507432514073.0 18014398509481984.0)))\n a!3))\n (a!7 (and (not (>= (+ x_1 x_2)\n (- (/ 3313437317012967.0 36028797018963968.0))))\n (or (not (>= a!1\n (- (/ 3170974553683589.0 4611686018427387904.0))))\n a!6)))\n (a!10 (and (not (>= (+ x_1 z_1)\n (- (/ 6772477090842733.0 36028797018963968.0))))\n (ite (>= (+ x_1 z_1)\n (- (/ 429854623273669.0 2251799813685248.0)))\n a!8\n a!9))))\n(let ((a!11 (ite (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (- (/ 5502047664758535.0 18014398509481984.0)))\n (ite (>= (+ x_1 x_2)\n (- (/ 6629630116421945.0 72057594037927936.0)))\n a!7\n a!10)\n (and (>= (+ x_2 z_1)\n (/ 4040401307218897.0 576460752303423488.0))\n (>= x_2 (- (/ 1698047291566937.0 36028797018963968.0)))))))\n(let ((a!12 (ite (>= (+ x_1 (* (- 1.0) x_2))\n (- (/ 7055780168714131.0 144115188075855872.0)))\n a!5\n a!11)))\n(let ((a!13 (ite (>= x_1 (- (/ 666203261502095.0 9007199254740992.0)))\n (and (not (>= x_2\n (- (/ 2269729184233765.0 288230376151711744.0))))\n (>= x_2 (- (/ 4539612283488395.0 576460752303423488.0))))\n (ite (>= x_1 (- (/ 2667045390271675.0 36028797018963968.0)))\n (and a!2 a!4)\n a!12))))\n (F (ite (>= a!1 (- (/ 6351107699626993.0 18014398509481984.0))) a!13 a!14))))))))\n"}, "teacher time": 3618.873932123184, "learner time": 14.520384788513184}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.0, 0.052359877559829904]], "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 43, in synth_dtree\n result = teacher.check(candidate)\n File \"/home/chsieh16/cs598mp-fall2021-proj/dtree_teacher_base.py\", line 133, in check\n self._set_candidate(conjunct)\n File \"/home/chsieh16/cs598mp-fall2021-proj/dtree_teacher_base.py\", line 50, in _set_candidate\n raise RuntimeError(f\"{conjunct} should be a conjunction.\")\nRuntimeError: False should be a conjunction.\n"}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.052359877559829904, 0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.10471975511965975, 0.15707963267948966]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.15707963267948966, 0.20943951023931956]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [-0.6, 0.0], [0.20943951023931956, 0.2617993877991494]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.2617993877991494, -0.20943951023931953]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.20943951023931953, -0.15707963267948966]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.15707963267948966, -0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.10471975511965975, -0.052359877559829876]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [-0.052359877559829876, 0.0]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 44, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 z_1)\n (- (/ 5112528810971469.0 72057594037927936.0)))))\n (a!2 (and (>= (+ x_1 x_2 z_1) (/ 4269794351995631.0 9007199254740992.0))\n (not (>= (+ x_2 z_1) (/ 1297659990871131.0 18014398509481984.0)))))\n (a!5 (and (>= (+ x_1 x_2) (/ 3847053344477379.0 72057594037927936.0))\n (not (>= (+ x_2 z_0 z_1)\n (- (/ 7176994012252853.0 72057594037927936.0)))))))\n(let ((a!3 (and a!1\n (ite (>= (+ x_2 z_1) (/ 365047734563815.0 18014398509481984.0))\n a!2\n (>= (+ x_1 x_2)\n (/ 6473984272148139.0 144115188075855872.0))))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) z_1))\n (/ 4519262246154565.0 9007199254740992.0))\n (not (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4535279028013331.0 288230376151711744.0))))\n a!3)))\n (ite (>= (+ x_2 z_1) (/ 5364065298511247.0 288230376151711744.0)) a!4 a!5))))", "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)\n (- (/ 5112528810971469.0 72057594037927936.0)))))\n (a!2 (and (>= (+ x_1 x_2 z_1) (/ 4269794351995631.0 9007199254740992.0))\n (not (>= (+ x_2 z_1) (/ 1297659990871131.0 18014398509481984.0)))))\n (a!5 (and (>= (+ x_1 x_2) (/ 3847053344477379.0 72057594037927936.0))\n (not (>= (+ x_2 z_0 z_1)\n (- (/ 7176994012252853.0 72057594037927936.0)))))))\n(let ((a!3 (and a!1\n (ite (>= (+ x_2 z_1) (/ 365047734563815.0 18014398509481984.0))\n a!2\n (>= (+ x_1 x_2)\n (/ 6473984272148139.0 144115188075855872.0))))))\n(let ((a!4 (ite (>= (+ x_1 (* (- 1.0) z_1))\n (/ 4519262246154565.0 9007199254740992.0))\n (not (>= (+ x_1 x_2 z_0 z_1)\n (- (/ 4535279028013331.0 288230376151711744.0))))\n a!3)))\n (F (ite (>= (+ x_2 z_1) (/ 5364065298511247.0 288230376151711744.0)) a!4 a!5))))))\n"}, "teacher time": 1667.269275188446, "learner time": 6.1674463748931885}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.0, 0.052359877559829904]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.052359877559829904, 0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.10471975511965975, 0.15707963267948966]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.15707963267948966, 0.20943951023931956]], "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.1396976667634376, 0.249280076923651, 0.20943951023931956, 0.16630087257983334, -0.17044139999999974), (-0.1396818761294844, 0.2399739495902638, 0.20943951023931956, 0.1768496293261711, -0.17044139999999985)) are repeated.\n"}, {"part": [[-Infinity, Infinity], [0.0, 0.5999999999999999], [0.20943951023931956, 0.2617993877991494]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 5, "formula": "(and (not (>= (+ x_1 z_0 z_1) (- (/ 5390131412578527.0 36028797018963968.0))))\n (not (>= (+ x_2 z_1) (/ 5423875983866489.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 (and (not (>= (+ x_1 z_0 z_1)\n (- (/ 5390131412578527.0 36028797018963968.0))))\n (not (>= (+ x_2 z_1) (/ 5423875983866489.0 72057594037927936.0))))))\n (F a!1)))\n"}, "teacher time": 118.57961368560791, "learner time": 0.3993110656738281}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.2617993877991494, -0.20943951023931953]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.20943951023931953, -0.15707963267948966]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.15707963267948966, -0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.10471975511965975, -0.052359877559829876]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [-0.052359877559829876, 0.0]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.0, 0.052359877559829904]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 5, "formula": "(ite (>= (+ x_2 z_1) (/ 1149627391695403.0 36028797018963968.0))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 6878631437659483.0 2251799813685248.0))\n (not (>= (+ x_2 z_0 z_1) (- (/ 2839596126250763.0 9007199254740992.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) (/ 1149627391695403.0 36028797018963968.0))\n (>= (+ x_1 (* (- 1.0) x_2) (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 6878631437659483.0 2251799813685248.0))\n (not (>= (+ x_2 z_0 z_1)\n (- (/ 2839596126250763.0 9007199254740992.0)))))))\n (F a!1)))\n"}, "teacher time": 108.39767742156982, "learner time": 0.44097065925598145}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.052359877559829904, 0.10471975511965975]], "status": "skip", "result": "No unsafe datapoints for unsafe run."}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.10471975511965975, 0.15707963267948966]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 16, "formula": "(let ((a!1 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (/ 1505895629001637.0 562949953421312.0)))))\n (ite (>= (+ x_1 z_0 z_1) (/ 1141925155468689.0 36028797018963968.0))\n (and (not (<= x_2 (/ 2762969180030905.0 18014398509481984.0)))\n a!1\n (not (>= x_2 (/ 5535849882121727.0 36028797018963968.0))))\n (not (>= (+ x_2 z_1) (/ 5675854184457719.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 (not (>= (+ x_1 (* (- 1.0) x_2) z_0 (* (- 1.0) z_1))\n (/ 1505895629001637.0 562949953421312.0)))))\n(let ((a!2 (ite (>= (+ x_1 z_0 z_1) (/ 1141925155468689.0 36028797018963968.0))\n (and (not (<= x_2 (/ 2762969180030905.0 18014398509481984.0)))\n a!1\n (not (>= x_2 (/ 5535849882121727.0 36028797018963968.0))))\n (not (>= (+ x_2 z_1) (/ 5675854184457719.0 72057594037927936.0))))))\n (F a!2))))\n"}, "teacher time": 202.2067265510559, "learner time": 1.527289867401123}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.15707963267948966, 0.20943951023931956]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 3, "formula": "(and (<= (+ z_0 z_1) (- (/ 7112814114683121.0 9007199254740992.0)))\n (not (>= (+ x_2 z_1) (/ 3607531019591545.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 (<= (+ z_0 z_1) (- (/ 7112814114683121.0 9007199254740992.0)))\n (not (>= (+ x_2 z_1) (/ 3607531019591545.0 36028797018963968.0))))))\n (F a!1)))\n"}, "teacher time": 48.199371099472046, "learner time": 0.27370500564575195}, {"part": [[-Infinity, Infinity], [0.5999999999999999, 1.2], [0.20943951023931956, 0.2617993877991494]], "feature_domain": "concat", "ultimate_bound": 0.0, "status": "found", "result": {"k": 16, "formula": "(and (not (>= x_2 (/ 8403237721672993.0 36028797018963968.0)))\n (not (<= x_2 (/ 8403237721672993.0 36028797018963968.0)))\n (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 8324792221923603.0 72057594037927936.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 (/ 8403237721672993.0 36028797018963968.0)))\n (not (<= x_2 (/ 8403237721672993.0 36028797018963968.0)))\n (>= (+ x_1 x_2 (* (- 1.0) z_0) (* (- 1.0) z_1))\n (/ 8324792221923603.0 72057594037927936.0)))))\n (F a!1)))\n"}, "teacher time": 133.48461890220642, "learner time": 1.2041714191436768}]
\ 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
0.6,0.21034383304166743,0.5619743717990529,0.08640264268317144,false
0.6,0.21170486155602336,0.5619743717990529,0.08734998738805802,false
0.6001276750322182,0.2148125489293497,0.5619743717990529,0.08954970457143605,false
0.6001431804041583,0.21479885583846425,0.5619743717990529,0.08953601148055057,false
0.6,0.20943951023931953,0.5619743717990529,0.08326927388579242,false
0.6,0.20943951023931953,0.5619743717990529,0.08104329708402683,false
0.5999999999999986,0.2336330772603737,0.561974371799586,0.10210349530771601,false
0.6022159626800725,0.23363307726038784,0.5619743717990529,0.10210349530771601,false
0.6,0.20943951023931953,0.5619743717990529,0.07700253629103415,false
0.6000000000013207,0.23673243741619246,0.578112976074909,0.09949750511769588,false
0.6,0.2307028179700558,0.1508735025675574,0.16187001797005576,false
0.6,0.23070281796234438,0.1315499801847447,0.16497398075463365,false
0.6,0.23359906862273883,0.09254417436692586,0.17413696900978637,false
0.6,0.2555326502043924,-0.004945234512408551,0.1898038129966818,false
0.6,0.2617993877991508,-0.005128206380782116,0.19296658779915077,false
0.6,0.20997545516089627,-0.04393899773422881,0.17413696900978637,false
0.6,0.23673243742011785,-0.06343698215558682,0.20233728818619834,false
0.5999999999999998,0.2555326502043926,-0.19997921652298922,0.221137500970473,false
0.60011052513366,0.26100808859896807,-0.20156422359146658,0.22452531373262807,false
0.6,0.2617993877991508,-0.21949790188998258,0.22740423856523118,false
0.6,0.2617993877991507,-1.4805385860867106,0.22520608779915063,false
0.6,0.2617993877991508,-1.4949947038655405,0.22740423856523118,false
0.6,0.209439510553062,-0.0634369821555868,0.18603233321520263,false
0.6,0.20945076488787634,-0.0634369821555868,0.18604027465691025,false
0.6,0.21034383333600676,-0.0634369821555868,0.1866704441993028,false
0.6,0.23360354950513507,-0.10825825675926326,0.209543749505135,false
0.6,0.23673243742642763,-0.12776184281424696,0.21267263742642756,false
0.6,0.23673243742011796,-0.14144520886564751,0.21487076337571476,false
0.6,0.25553265020745997,-0.2643787184730172,0.2314728502074599,false
0.6,0.25553265020439253,-0.2780813907506467,0.23367097615998939,false
0.6,0.2617993877991508,-0.28391313840081056,0.23773958779915072,false
0.6,0.20943951023936055,-0.10243707140619795,0.19229907008593128,false
0.6,0.2100180731452389,-0.1219399424619203,0.19584078291879908,false
0.6,0.21034383709399496,-0.1219399424619203,0.19607055059144005,false
0.6,0.2103824576499368,-0.1219399424619203,0.19607055059144007,false
0.6,0.20943951023931953,-0.1219399424619203,0.19293718179406114,false
0.6,0.23080502528776858,-0.1472677045501356,0.21301192528776858,false
0.6,0.2307982774389712,-0.14776051918563615,0.21300517743897118,false
0.6,0.23673243741868272,-0.16677669377118132,0.2189393374186827,false
0.6,0.23673243742011796,-0.21949790188998258,0.22740423856523118,false
0.6,0.2617993877991508,-0.32299888973920404,0.2440062877991508,false
0.6048638,0.23359906862273883,0.5816355544783299,0.09580274907527767,false
0.6068732150816128,0.23673243742011796,0.5816355544781345,0.09893611787268823,false
0.6032799102393193,0.20943951023931953,0.57742662707617,0.047247009818492225,false
0.6032799102393193,0.20943951023931953,0.5816355544781351,0.04657624031285659,false
0.6032799102393193,0.20943951023931953,0.6013082580256999,0.043442871515489256,false
0.6197255253303311,0.20947192834161005,0.6209928792122914,0.040341920820083865,false
0.6556397877991508,0.2617993877991508,0.620992879210504,0.0926693802779297,false
0.6525064190017714,0.2586660190017716,0.6406898157500011,-0.4494034216686473,false
0.6551148963408033,0.2612744963408033,0.6603994663439168,-0.45253679046603457,false
0.6,0.23047118634866093,-0.29761964894933185,0.23367646268329037,false
0.6,0.2429991750148761,-0.33671412433346043,0.23993771375474754,false
0.6559790594052042,0.2604987594052041,0.6013082580257738,0.11773633065696248,false
0.6541209580826756,0.2585182892950069,0.6013082580257737,0.11460296185958335,false
0.6541407168014738,0.2585139225205903,0.6013082580257738,0.11460296185958335,false
0.6541463190017717,0.25866601900177166,0.6013082580257737,0.11460296185958335,false
0.6544555418270253,0.2589752418270252,0.6013082580257737,0.11460296185958335,false
0.6432343909117815,0.24775409091178147,0.561974371799052,0.11460296185958349,false
0.6474746812353178,0.25199438123531787,0.5619743717990529,0.11773633065696254,false
0.6478795814070135,0.25239928140701345,0.5619743717990529,0.11773633065696248,false
0.6366396664214847,0.24047328515055064,0.5275298806774179,0.11473928127093413,false
0.7216492381180984,0.2174446,0.5111329465827467,0.09395889690107811,false
1.2,0.20943951023931953,1.987268815622282,-0.39110186383872514,false
1.2,0.20955542833056093,1.987268815622282,-0.39110186383872514,false
0.8668122139912378,0.20943951023931953,-0.2322364178754625,0.21255331412354425,false
1.0321585839827847,0.25242319229269494,-0.388206592360554,0.24616080067046409,false
0.6037559,0.209633690803743,-0.1804644620298426,0.20030549194885638,false
0.6037559,0.25866601900177166,-0.37583512473658187,0.24933782014688488,false
0.6041610627398329,0.25866601900177166,-0.37583512473658187,0.24933782014688488,false
0.6037558999999993,0.2617993877991494,-0.46859872106308986,0.267310881874774,false
0.619462294075619,0.2617993877991508,-0.46859872106309347,0.2673108818747698,false
0.6190036829816521,0.20943951023931953,0.7048357691138436,0.06391183410712803,false
0.6180957399786786,0.20943951023931953,0.7048357691138436,0.06387125413310546,false
0.6088990686068764,0.2273360060727352,0.7048357691138436,0.0727327036541062,false
0.6846344663675386,0.20945929482414272,0.8155740994237333,0.04901097518465314,false
0.6,0.20943951023931953,0.7315348378739819,0.018209082365337692,false
0.8876453635897653,0.21503925003226565,1.0760733515421645,-0.03308432792013358,false
0.8876211542582819,0.21503925003226565,1.0760733515421645,-0.03308432792013358,false
0.6425188873838784,0.2579427084322893,0.768955793067749,0.08859929431612948,false
0.6371648308777184,0.2617993877991508,0.7689557930677491,0.08324523780996934,false
0.6773058114753189,0.21651115734054532,0.842724947220446,0.04961706425487292,false
0.6756794882283829,0.21506735489268713,0.8425082072603244,0.04820748096805849,false
0.6756794882288211,0.21506735489268713,0.8427249472204459,0.04817326180701467,false
0.6000256318632565,0.21467695297398157,0.7797951037585047,0.054848561078733454,false
0.6,0.21222383417944538,0.7803688263192552,0.05179608786019016,false
0.6000031221593173,0.21227213898156982,0.7803725355192304,0.05184380562165675,false
0.6022696439223441,0.21222383417944538,0.7830652176063723,0.05136934049541719,false
0.6348215264485689,0.20943951023931953,0.8183651576948126,0.045836958993075966,false
0.6,0.20943951023931953,0.797768471450284,0.031612118789035554,false
0.6108814519945196,0.20943951023931953,0.8383716457538786,0.0018903964799606432,false
0.5999999999999996,0.250145917492677,0.8737816707104646,-0.003694673217787936,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