Analysing Machine Learning Models With Imandra

In this notebook we show how Imandra can be used to analyse and reason about models that have been learnt from data, an important and exciting topic bridging the gap between formal methods and machine learning (ML). Brief notes and some links are included, but for a fuller explanation (with code snippets included for reference) see our corresponding Medium post. You can also find all of our code for both learning and analysing our models on GitHub.

To illustrate this approach we'll be looking at (relatively simple) examples from two of the most common tasks within supervised learning (and ML more generally): classification and regression. In particular, we'll show how two of the most common kinds of model used to perform these tasks, random forests and neural networks, can be analysed using Imandra. For each task we'll use a real-world benchmark dataset from the UCI Machine Learning Repository and create our models using Python with some standard ML libraries.

We'll mostly be working with reals in this notebook so we'll start by installing a pretty printer so that we're not overrun with digits.

In [1]:
let pp_approx fmt r = CCFormat.fprintf fmt "%s" (Real.to_string_approx r) [@@program]
#install_printer pp_approx
Out[1]:
val pp_approx : CCFormat.t -> Q.t -> unit = <fun>

Classification

In a classification task we want to learn to predict the label of a datapoint based on previous data. In the classic Wisconsin Breast Cancer (Diagnostic) dataset) the task is to predict whether the cancer is benign or malignant based on the features of cell nuclei. In the dataset we have the following variables:

1. ID number
2. Diagnosis (malignant or benign)
3-32. Real values for the mean, standard error, and the 'worst' value for each cell nucleus'
      a) Radius
      b) Texture
      c) Perimeter
      d) Area
      e) Smoothness
      f) Compactness
      g) Concavity
      h) Concave points
      i) Symmetry
      j) Fractal dimension

As is standard practice we pre-process the data before learning. First we standardise each variable to have zero mean and unit variance, then remove all but one from sets of highly correlated variables, along with those that have low mutual information with respect to the target variable. The data is split into training (80%) and test (20%) sets and we use Scikit-Learn to learn a random forest of 3 decision trees of maximum depth 3. As this is a relatively straightforward problem even this simple model achieves a fairly high accuracy. Using a short Python script each tree is then converted to Imandra Modelling Language (IML) and can be reasoned about using Imandra.

In [2]:
let tree_0 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
  if f_2 <=. (-0.10815) then
    if f_0 <=. (0.26348) then
      if f_6 <=. (-0.06176) then
        (236.0, 1.0)
      else
        (17.0, 5.0)
    else
      if f_3 <=. (-0.54236) then
        (8.0, 2.0)
      else
        (3.0, 7.0)
  else
    if f_6 <=. (0.09812) then
      if f_6 <=. (-0.17063) then
        (24.0, 0.0)
      else
        (4.0, 2.0)
    else
      if f_2 <=. (2.65413) then
        (6.0, 128.0)
      else
        (7.0, 5.0);;

let tree_1 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
  if f_5 <=. (-0.05799) then
    if f_0 <=. (0.68524) then
      if f_1 <=. (-0.83180) then
        (110.0, 3.0)
      else
        (137.0, 0.0)
    else
      if f_3 <=. (0.45504) then
        (1.0, 8.0)
      else
        (0.0, 7.0)
  else
    if f_0 <=. (-0.18668) then
      if f_6 <=. (0.45214) then
        (39.0, 0.0)
      else
        (2.0, 11.0)
    else
      if f_6 <=. (-0.00009) then
        (8.0, 4.0)
      else
        (5.0, 120.0);;

let tree_2 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
  if f_2 <=. (0.10459) then
    if f_5 <=. (-0.38015) then
      if f_5 <=. (-0.60659) then
        (139.0, 1.0)
      else
        (44.0, 3.0)
    else
      if f_6 <=. (-0.07927) then
        (38.0, 2.0)
      else
        (25.0, 17.0)
  else
    if f_6 <=. (0.46888) then
      if f_3 <=. (0.41642) then
        (28.0, 3.0)
      else
        (1.0, 4.0)
    else
      if f_2 <=. (1.74327) then
        (3.0, 122.0)
      else
        (4.0, 21.0);;

let rf (f_0, f_1, f_2, f_3, f_4, f_5, f_6) = let open Real in
let (a_0, b_0) = tree_0 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_1, b_1) = tree_1 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_2, b_2) = tree_2 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let a = a_0 + a_1 + a_2 in
let b = b_0 + b_1 + b_2 in
(a, b);;
Out[2]:
val tree_0 : real -> 'a -> real -> real -> 'b -> 'c -> real -> Q.t * Q.t =
  <fun>
val tree_1 : real -> real -> 'a -> real -> 'b -> real -> real -> Q.t * Q.t =
  <fun>
val tree_2 : 'a -> 'b -> real -> real -> 'c -> real -> real -> Q.t * Q.t =
  <fun>
val rf : real * real * real * real * 'a * real * real -> real * real = <fun>

We can create a custom input type in Imandra for our model, so that we can keep track of the different features of our data.

In [3]:
type rf_input = {
  radius_mean : real;
  compactness_mean : real;
  concavity_mean : real;
  radius_se : real;
  compactness_worst : real;
  concavity_worst : real;
  concave_points_worst : real;
}
Out[3]:
type rf_input = {
  radius_mean : real;
  compactness_mean : real;
  concavity_mean : real;
  radius_se : real;
  compactness_worst : real;
  concavity_worst : real;
  concave_points_worst : real;
}

However, remember that we also processed our data before learning. To make things easier we'll add in a function applying this transformation to each input variable. Here we simply use some multiplicative and additive scaling values extracted during our data pre-processing stage. After that we can define a full model which combines these pre-processing steps and the random forest.

In [4]:
let process_rf_input input = let open Real in
let f_0 = (input.radius_mean          - 14.12729) / 3.52405 in
let f_1 = (input.compactness_mean     - 0.10434)  / 0.05281 in
let f_2 = (input.concavity_mean       - 0.08880)  / 0.07972 in
let f_3 = (input.radius_se            - 0.40517)  / 0.27731 in
let f_4 = (input.compactness_worst    - 0.25427)  / 0.15734 in
let f_5 = (input.concavity_worst      - 0.27219)  / 0.20862 in
let f_6 = (input.concave_points_worst - 0.11461)  / 0.06573 in
(f_0, f_1, f_2, f_3, f_4, f_5, f_6)

let process_rf_output c =
let (a, b) = c in
if a >. b then "benign" else "malignant"

let rf_model input = input |> process_rf_input |> rf |> process_rf_output
Out[4]:
val process_rf_input :
  rf_input -> real * real * real * real * real * real * real = <fun>
val process_rf_output : real * real -> string = <fun>
val rf_model : rf_input -> string = <fun>

As our model is fully executable we can both query it as well as find counterexamples, prove properties, apply logical side-conditions, decompose its regions, and more. As a quick sanity check to make sure everything is working, let's run a datum from our dataset through the model. In particular, we'll input (17.99, 0.2776, 0.3001, 1.095, 0.6656, 0.7119, 0.2654) which is classified as malignant in the data.

In [5]:
let x = {
  radius_mean = 17.99;
  compactness_mean = 0.2776;
  concavity_mean = 0.3001;
  radius_se = 1.095;
  compactness_worst = 0.6656;
  concavity_worst = 0.7119;
  concave_points_worst = 0.7119;
}

let y = rf_model x
Out[5]:
val x : rf_input =
  {radius_mean = 17.99; compactness_mean = 0.2776; concavity_mean = 0.3001;
   radius_se = 1.095; compactness_worst = 0.6656; concavity_worst = 0.7119;
   concave_points_worst = 0.7119}
val y : string = "malignant"

Great, just what we'd expect. Now we'll use Imandra to generate an example datapoint for us given that diagnosis is benign.

In [6]:
instance (fun x -> rf_model x = "benign")
Out[6]:
- : rf_input -> bool = <fun>
module CX : sig val x : rf_input end
Instance (after 0 steps, 0.178s):
 let (x : rf_input) =
   {radius_mean = (Real.mk_of_string "-216972096653/500000000");
    compactness_mean = (Real.mk_of_string "-140469793679/500000000");
    concavity_mean = (Real.mk_of_string "-4048959910859/500000000");
    radius_se = 5853.0; compactness_worst = 9.0;
    concavity_worst = (Real.mk_of_string "-5709271784029/5000000000");
    concave_points_worst = (Real.mk_of_string "-47569488241/78125000")}
Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.178s
details
Expand
smt_stats
num checks1
arith assert lower7
arith pivots3
rlimit count2633
mk clause65
datatype occurs check25
seq add axiom2
mk bool var158
arith assert upper15
decisions22
seq num reductions2
propagations43
datatype accessor ax28
datatype constructor ax4
num allocs1016846696
final checks1
added eqs93
del clause1
arith eq adapter6
memory23.170000
max memory26.980000
Expand
  • start[0.178s]
      (if (((if ….2 <=. -2163/20000 then … else …).0
            +. (if ….5 <=. -5799/100000 then … else …).0)
           +. (if ….2 <=. 10459/100000 then … else …).0)
          >.
          (((if ….2 <=. -2163/20000 then … else …).1
            +. (if ….5 <=. -5799/100000 then … else …).1)
           +. (if ….2 <=. 10459/100000 then … else …).1)
       then "benign" else "malignant")
      = "benign"
  • simplify

    into
    (if (((if :var_0:.concavity_mean <=. 40089141/500000000
           then
             if :var_0:.radius_mean <=. 7527903347/500000000
             then
               if :var_0:.concave_points_worst <=. 8636759/78125000 then …
               else …
             else if :var_0:.radius_se <=. 636920371/2500000000 then … else …
           else
           if :var_0:.concave_points_worst <=. 302648569/2500000000
           then
             if :var_0:.concave_points_worst <=. 1033944901/10000000000 then …
             else …
           else
           if :var_0:.concavity_mean <=. 750968109/2500000000 then … else …).0
          +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
              then
                if :var_0:.radius_mean <=. 8271055011/500000000
                then
                  if :var_0:.compactness_mean <=. 30206321/500000000 then …
                  else …
                else
                if :var_0:.radius_se <=. 166049107/312500000 then … else …
              else
              if :var_0:.radius_mean <=. 6734710173/500000000
              then
                if :var_0:.concave_points_worst <=. 721645811/5000000000 
                then … else …
              else
              if :var_0:.concave_points_worst <=. 1146040843/10000000000 
              then … else …).0)
         +. (if :var_0:.concavity_mean <=. 242844787/2500000000
             then
               if :var_0:.concavity_worst <=. 192883107/1000000000
               then
                 if :var_0:.concavity_worst <=. 728215971/5000000000 then …
                 else …
               else
               if :var_0:.concave_points_worst <=. 1093995829/10000000000
               then … else …
             else
             if :var_0:.concave_points_worst <=. 181786853/1250000000
             then
               if :var_0:.radius_se <=. 2603237151/5000000000 then … else …
             else
             if :var_0:.concavity_mean <=. 569433711/2500000000 then … else …).0)
        <=.
        (((if :var_0:.concavity_mean <=. 40089141/500000000
           then
             if :var_0:.radius_mean <=. 7527903347/500000000
             then
               if :var_0:.concave_points_worst <=. 8636759/78125000 then …
               else …
             else if :var_0:.radius_se <=. 636920371/2500000000 then … else …
           else
           if :var_0:.concave_points_worst <=. 302648569/2500000000
           then
             if :var_0:.concave_points_worst <=. 1033944901/10000000000 then …
             else …
           else
           if :var_0:.concavity_mean <=. 750968109/2500000000 then … else …).1
          +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
              then
                if :var_0:.radius_mean <=. 8271055011/500000000
                then
                  if :var_0:.compactness_mean <=. 30206321/500000000 then …
                  else …
                else
                if :var_0:.radius_se <=. 166049107/312500000 then … else …
              else
              if :var_0:.radius_mean <=. 6734710173/500000000
              then
                if :var_0:.concave_points_worst <=. 721645811/5000000000 
                then … else …
              else
              if :var_0:.concave_points_worst <=. 1146040843/10000000000 
              then … else …).1)
         +. (if :var_0:.concavity_mean <=. 242844787/2500000000
             then
               if :var_0:.concavity_worst <=. 192883107/1000000000
               then
                 if :var_0:.concavity_worst <=. 728215971/5000000000 then …
                 else …
               else
               if :var_0:.concave_points_worst <=. 1093995829/10000000000
               then … else …
             else
             if :var_0:.concave_points_worst <=. 181786853/1250000000
             then
               if :var_0:.radius_se <=. 2603237151/5000000000 then … else …
             else
             if :var_0:.concavity_mean <=. 569433711/2500000000 then … else …).1)
     then "malignant" else "benign")
    = "benign"
    expansions
    []
    rewrite_steps
      forward_chaining
      • Sat (Some let (x : rf_input) = {radius_mean = (Real.mk_of_string "-216972096653/500000000"); compactness_mean = (Real.mk_of_string "-140469793679/500000000"); concavity_mean = (Real.mk_of_string "-4048959910859/500000000"); radius_se = 5853.0; compactness_worst = 9.0; concavity_worst = (Real.mk_of_string "-5709271784029/5000000000"); concave_points_worst = (Real.mk_of_string "-47569488241/78125000")} )
      In [7]:
      CX.x
      
      Out[7]:
      - : rf_input =
      {radius_mean = -433.944193306; compactness_mean = -280.939587358;
       concavity_mean = -8097.91982172; radius_se = 5853.; compactness_worst = 9.;
       concavity_worst = -1141.85435681; concave_points_worst = -608.889449485}
      

      This looks a bit funny however; notice how the unspecified input variables are unbounded in a way that doesn't make sense with respect to the data. In general we might only care about the performance of our model when some reasonable bounds are placed on the input (for example, the mean radius can't be negative, and if the values for this variable in our dataset range between 6.98 and 28.11 we wouldn't really expect any value greater than, say, 35). Using the description of each variable in the dataset we can form a condition describing valid and reasonable inputs to our model. In machine learning more generally, we are typically only interested in the performance and quality of a model over some particular distribution of data, which we often have particular prior beliefs about.

      In [8]:
      let is_valid_rf input =
        5.0 <=. input.radius_mean && input.radius_mean <=. 35.0 &&
        0.0 <=. input.compactness_mean && input.compactness_mean <=. 0.4 &&
        0.0 <=. input.concavity_mean && input.concavity_mean <=. 0.5 &&
        0.0 <=. input.radius_se && input.radius_se <=. 3.5 &&
        0.0 <=. input.compactness_worst && input.compactness_worst <=. 1.2 &&
        0.0 <=. input.concavity_worst && input.concavity_worst <=. 1.5 &&
        0.0 <=. input.concave_points_worst && input.concave_points_worst <=. 0.35
      
      instance (fun x -> rf_model x = "benign" && is_valid_rf x)
      
      Out[8]:
      val is_valid_rf : rf_input -> bool = <fun>
      - : rf_input -> bool = <fun>
      module CX : sig val x : rf_input end
      
      Instance (after 0 steps, 0.038s):
       let (x : rf_input) =
         {radius_mean = (Real.mk_of_string "15370932811137/2500000000000");
          compactness_mean = (Real.mk_of_string "13562638129/5000000000000");
          concavity_mean = (Real.mk_of_string "11265048621/5000000000000");
          radius_se = (Real.mk_of_string "40971/20000");
          compactness_worst = (Real.mk_of_string "321/5000");
          concavity_worst = (Real.mk_of_string "443483526339/50000000000000");
          concave_points_worst = (Real.mk_of_string "34970237191/390625000000")}
      
      Instance
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.038s
      details
      Expand
      smt_stats
      num checks1
      arith assert lower14
      arith pivots3
      rlimit count3211
      mk clause65
      datatype occurs check25
      seq add axiom2
      mk bool var172
      arith assert upper22
      decisions22
      seq num reductions2
      propagations43
      datatype accessor ax28
      datatype constructor ax4
      num allocs1085644787
      final checks1
      added eqs93
      del clause1
      arith eq adapter6
      memory26.460000
      max memory27.150000
      Expand
      • start[0.038s]
          (if (((if ….2 <=. -2163/20000 then … else …).0
                +. (if ….5 <=. -5799/100000 then … else …).0)
               +. (if ….2 <=. 10459/100000 then … else …).0)
              >.
              (((if ….2 <=. -2163/20000 then … else …).1
                +. (if ….5 <=. -5799/100000 then … else …).1)
               +. (if ….2 <=. 10459/100000 then … else …).1)
           then "benign" else "malignant")
          = "benign"
          && 5 <=. :var_0:.radius_mean
             && :var_0:.radius_mean <=. 35
                && 0 <=. :var_0:.compactness_mean
                   && :var_0:.compactness_mean <=. 2/5
                      && 0 <=. :var_0:.concavity_mean
                         && :var_0:.concavity_mean <=. 1/2
                            && 0 <=. :var_0:.radius_se
                               && :var_0:.radius_se <=. 7/2
                                  && 0 <=. :var_0:.compactness_worst
                                     && :var_0:.compactness_worst <=. 6/5
                                        && 0 <=. :var_0:.concavity_worst
                                           && :var_0:.concavity_worst <=. 3/2
                                              && 0 <=. :var_0:.concave_points_worst
                                                 && :var_0:.concave_points_worst <=.
                                                    7/20
      • simplify

        into
        ((((((((((((((if (((if :var_0:.concavity_mean <=. 40089141/500000000
                            then
                              if :var_0:.radius_mean <=. 7527903347/500000000
                              then
                                if :var_0:.concave_points_worst <=. 8636759/78125000
                                then … else …
                              else
                              if :var_0:.radius_se <=. 636920371/2500000000 then …
                              else …
                            else
                            if :var_0:.concave_points_worst <=. 302648569/2500000000
                            then
                              if :var_0:.concave_points_worst <=.
                                 1033944901/10000000000
                              then … else …
                            else
                            if :var_0:.concavity_mean <=. 750968109/2500000000
                            then … else …).0
                           +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
                               then
                                 if :var_0:.radius_mean <=. 8271055011/500000000
                                 then
                                   if :var_0:.compactness_mean <=. 30206321/500000000
                                   then … else …
                                 else
                                 if :var_0:.radius_se <=. 166049107/312500000
                                 then … else …
                               else
                               if :var_0:.radius_mean <=. 6734710173/500000000
                               then
                                 if :var_0:.concave_points_worst <=.
                                    721645811/5000000000
                                 then … else …
                               else
                               if :var_0:.concave_points_worst <=.
                                  1146040843/10000000000
                               then … else …).0)
                          +. (if :var_0:.concavity_mean <=. 242844787/2500000000
                              then
                                if :var_0:.concavity_worst <=. 192883107/1000000000
                                then
                                  if :var_0:.concavity_worst <=. 728215971/5000000000
                                  then … else …
                                else
                                if :var_0:.concave_points_worst <=.
                                   1093995829/10000000000
                                then … else …
                              else
                              if :var_0:.concave_points_worst <=.
                                 181786853/1250000000
                              then
                                if :var_0:.radius_se <=. 2603237151/5000000000
                                then … else …
                              else
                              if :var_0:.concavity_mean <=. 569433711/2500000000
                              then … else …).0)
                         <=.
                         (((if :var_0:.concavity_mean <=. 40089141/500000000
                            then
                              if :var_0:.radius_mean <=. 7527903347/500000000
                              then
                                if :var_0:.concave_points_worst <=. 8636759/78125000
                                then … else …
                              else
                              if :var_0:.radius_se <=. 636920371/2500000000 then …
                              else …
                            else
                            if :var_0:.concave_points_worst <=. 302648569/2500000000
                            then
                              if :var_0:.concave_points_worst <=.
                                 1033944901/10000000000
                              then … else …
                            else
                            if :var_0:.concavity_mean <=. 750968109/2500000000
                            then … else …).1
                           +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
                               then
                                 if :var_0:.radius_mean <=. 8271055011/500000000
                                 then
                                   if :var_0:.compactness_mean <=. 30206321/500000000
                                   then … else …
                                 else
                                 if :var_0:.radius_se <=. 166049107/312500000
                                 then … else …
                               else
                               if :var_0:.radius_mean <=. 6734710173/500000000
                               then
                                 if :var_0:.concave_points_worst <=.
                                    721645811/5000000000
                                 then … else …
                               else
                               if :var_0:.concave_points_worst <=.
                                  1146040843/10000000000
                               then … else …).1)
                          +. (if :var_0:.concavity_mean <=. 242844787/2500000000
                              then
                                if :var_0:.concavity_worst <=. 192883107/1000000000
                                then
                                  if :var_0:.concavity_worst <=. 728215971/5000000000
                                  then … else …
                                else
                                if :var_0:.concave_points_worst <=.
                                   1093995829/10000000000
                                then … else …
                              else
                              if :var_0:.concave_points_worst <=.
                                 181786853/1250000000
                              then
                                if :var_0:.radius_se <=. 2603237151/5000000000
                                then … else …
                              else
                              if :var_0:.concavity_mean <=. 569433711/2500000000
                              then … else …).1)
                      then "malignant" else "benign")
                     = "benign" && 5 <=. :var_0:.radius_mean)
                    && :var_0:.radius_mean <=. 35)
                   && 0 <=. :var_0:.compactness_mean)
                  && :var_0:.compactness_mean <=. 2/5)
                 && 0 <=. :var_0:.concavity_mean)
                && :var_0:.concavity_mean <=. 1/2)
               && 0 <=. :var_0:.radius_se)
              && :var_0:.radius_se <=. 7/2)
             && 0 <=. :var_0:.compactness_worst)
            && :var_0:.compactness_worst <=. 6/5)
           && 0 <=. :var_0:.concavity_worst)
          && :var_0:.concavity_worst <=. 3/2)
         && 0 <=. :var_0:.concave_points_worst)
        && :var_0:.concave_points_worst <=. 7/20
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let (x : rf_input) = {radius_mean = (Real.mk_of_string "15370932811137/2500000000000"); compactness_mean = (Real.mk_of_string "13562638129/5000000000000"); concavity_mean = (Real.mk_of_string "11265048621/5000000000000"); radius_se = (Real.mk_of_string "40971/20000"); compactness_worst = (Real.mk_of_string "321/5000"); concavity_worst = (Real.mk_of_string "443483526339/50000000000000"); concave_points_worst = (Real.mk_of_string "34970237191/390625000000")} )
          In [9]:
          CX.x
          
          Out[9]:
          - : rf_input =
          {radius_mean = 6.14837312445; compactness_mean = 0.0027125276258;
           concavity_mean = 0.0022530097242; radius_se = 2.04855;
           compactness_worst = 0.0642; concavity_worst = 0.00886967052678;
           concave_points_worst = 0.089523807209}
          

          This looks much better. Now let's move on to reasoning about our model in more interesting ways. One thing we can do is check the validity of certain constraints we might want our model to satisfy. For example, if the surface of a cell nucleus has many, large concave sections then is a particularly negative sign indicating that the cancer is likely to be malignant. We can use Imandra to easily verify that our model always classifies a sample of highly concave cells as malignant.

          In [10]:
          verify (fun x -> is_valid_rf x
                  && x.concavity_mean >=. 0.4
                  && x.concavity_worst >=. 1.0
                  && x.concave_points_worst >=. 0.25
                  ==> rf_model x = "malignant")
          
          Out[10]:
          - : rf_input -> bool = <fun>
          
          Proved
          proof
          ground_instances0
          definitions0
          inductions0
          search_time
          0.035s
          details
          Expand
          smt_stats
          num checks1
          arith assert lower30
          arith pivots2
          rlimit count3216
          mk clause56
          seq add axiom2
          mk bool var181
          arith assert upper16
          decisions9
          seq num reductions2
          propagations28
          conflicts2
          datatype accessor ax28
          arith conflicts2
          datatype constructor ax4
          num allocs1264100801
          added eqs99
          del clause36
          arith eq adapter8
          memory16.700000
          max memory27.150000
          Expand
          • start[0.035s]
              (5 <=. :var_0:.radius_mean
               && :var_0:.radius_mean <=. 35
                  && 0 <=. :var_0:.compactness_mean
                     && :var_0:.compactness_mean <=. 2/5
                        && 0 <=. :var_0:.concavity_mean
                           && :var_0:.concavity_mean <=. 1/2
                              && 0 <=. :var_0:.radius_se
                                 && :var_0:.radius_se <=. 7/2
                                    && 0 <=. :var_0:.compactness_worst
                                       && :var_0:.compactness_worst <=. 6/5
                                          && 0 <=. :var_0:.concavity_worst
                                             && :var_0:.concavity_worst <=. 3/2
                                                && 0 <=. :var_0:.concave_points_worst
                                                   && :var_0:.concave_points_worst <=.
                                                      7/20)
              && :var_0:.concavity_mean >=. 2/5
                 && :var_0:.concavity_worst >=. 1 && :var_0:.concave_points_worst >=. 1/4
              ==> (if (((if ….2 <=. -2163/20000 then … else …).0
                        +. (if ….5 <=. -5799/100000 then … else …).0)
                       +. (if ….2 <=. 10459/100000 then … else …).0)
                      >.
                      (((if ….2 <=. -2163/20000 then … else …).1
                        +. (if ….5 <=. -5799/100000 then … else …).1)
                       +. (if ….2 <=. 10459/100000 then … else …).1)
                   then "benign" else "malignant")
                  = "malignant"
          • simplify

            into
            not
            ((((((((((((((((5 <=. :var_0:.radius_mean && :var_0:.radius_mean <=. 35)
                           && 0 <=. :var_0:.compactness_mean)
                          && :var_0:.compactness_mean <=. 2/5)
                         && 0 <=. :var_0:.concavity_mean)
                        && :var_0:.concavity_mean <=. 1/2)
                       && 0 <=. :var_0:.radius_se)
                      && :var_0:.radius_se <=. 7/2)
                     && 0 <=. :var_0:.compactness_worst)
                    && :var_0:.compactness_worst <=. 6/5)
                   && 0 <=. :var_0:.concavity_worst)
                  && :var_0:.concavity_worst <=. 3/2)
                 && 0 <=. :var_0:.concave_points_worst)
                && :var_0:.concave_points_worst <=. 7/20)
               && :var_0:.concavity_mean >=. 2/5)
              && :var_0:.concavity_worst >=. 1)
             && :var_0:.concave_points_worst >=. 1/4)
            || (if (((if :var_0:.concavity_mean <=. 40089141/500000000
                      then
                        if :var_0:.radius_mean <=. 7527903347/500000000
                        then
                          if :var_0:.concave_points_worst <=. 8636759/78125000 then …
                          else …
                        else
                        if :var_0:.radius_se <=. 636920371/2500000000 then … else …
                      else
                      if :var_0:.concave_points_worst <=. 302648569/2500000000
                      then
                        if :var_0:.concave_points_worst <=. 1033944901/10000000000
                        then … else …
                      else
                      if :var_0:.concavity_mean <=. 750968109/2500000000 then …
                      else …).0
                     +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
                         then
                           if :var_0:.radius_mean <=. 8271055011/500000000
                           then
                             if :var_0:.compactness_mean <=. 30206321/500000000 then …
                             else …
                           else
                           if :var_0:.radius_se <=. 166049107/312500000 then … else …
                         else
                         if :var_0:.radius_mean <=. 6734710173/500000000
                         then
                           if :var_0:.concave_points_worst <=. 721645811/5000000000
                           then … else …
                         else
                         if :var_0:.concave_points_worst <=. 1146040843/10000000000
                         then … else …).0)
                    +. (if :var_0:.concavity_mean <=. 242844787/2500000000
                        then
                          if :var_0:.concavity_worst <=. 192883107/1000000000
                          then
                            if :var_0:.concavity_worst <=. 728215971/5000000000 then …
                            else …
                          else
                          if :var_0:.concave_points_worst <=. 1093995829/10000000000
                          then … else …
                        else
                        if :var_0:.concave_points_worst <=. 181786853/1250000000
                        then
                          if :var_0:.radius_se <=. 2603237151/5000000000 then …
                          else …
                        else
                        if :var_0:.concavity_mean <=. 569433711/2500000000 then …
                        else …).0)
                   <=.
                   (((if :var_0:.concavity_mean <=. 40089141/500000000
                      then
                        if :var_0:.radius_mean <=. 7527903347/500000000
                        then
                          if :var_0:.concave_points_worst <=. 8636759/78125000 then …
                          else …
                        else
                        if :var_0:.radius_se <=. 636920371/2500000000 then … else …
                      else
                      if :var_0:.concave_points_worst <=. 302648569/2500000000
                      then
                        if :var_0:.concave_points_worst <=. 1033944901/10000000000
                        then … else …
                      else
                      if :var_0:.concavity_mean <=. 750968109/2500000000 then …
                      else …).1
                     +. (if :var_0:.concavity_worst <=. 1300460631/5000000000
                         then
                           if :var_0:.radius_mean <=. 8271055011/500000000
                           then
                             if :var_0:.compactness_mean <=. 30206321/500000000 then …
                             else …
                           else
                           if :var_0:.radius_se <=. 166049107/312500000 then … else …
                         else
                         if :var_0:.radius_mean <=. 6734710173/500000000
                         then
                           if :var_0:.concave_points_worst <=. 721645811/5000000000
                           then … else …
                         else
                         if :var_0:.concave_points_worst <=. 1146040843/10000000000
                         then … else …).1)
                    +. (if :var_0:.concavity_mean <=. 242844787/2500000000
                        then
                          if :var_0:.concavity_worst <=. 192883107/1000000000
                          then
                            if :var_0:.concavity_worst <=. 728215971/5000000000 then …
                            else …
                          else
                          if :var_0:.concave_points_worst <=. 1093995829/10000000000
                          then … else …
                        else
                        if :var_0:.concave_points_worst <=. 181786853/1250000000
                        then
                          if :var_0:.radius_se <=. 2603237151/5000000000 then …
                          else …
                        else
                        if :var_0:.concavity_mean <=. 569433711/2500000000 then …
                        else …).1)
                then "malignant" else "benign")
               = "malignant"
            expansions
            []
            rewrite_steps
              forward_chaining
              • unsat

                (let ((a!1 (ite (<= (radius_mean_65 x_95) (/ 7527903347.0 500000000.0))
                                (ite (<= (co…

              The nested if ... then ... else statements in how the trees are defined mean that they are a prime candidate for Imandra's region decomposition functionality. As well as the total model we can of course also decompose the individual trees making up the ensemble.

              In [11]:
              Decompose.top ~assuming:"is_valid_rf" "rf_model"
              
              Out[11]:
              - : Imandra_interactive.Decompose.t list =
              [<region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>; <region>; <region>; <region>; <region>; <region>]
              
              Regions details

              No group selected.

              • Concrete regions are numbered
              • Unnumbered regions are groups whose children share a particular constraint
              • Click on a region to view its details
              • Double click on a region to zoom in on it
              • Shift+double click to zoom out
              • Hit escape to reset back to the top
              ConstraintsInvariant
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_mean <=. 6734710173/500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_se <=. 166049107/312500000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              • not (input.concavity_mean <=. 569433711/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.concavity_mean <=. 569433711/2500000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • not (input.concave_points_worst <=. 181786853/1250000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • input.concavity_mean <=. 569433711/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • not (input.concavity_mean <=. 750968109/2500000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 302648569/2500000000)
              • input.concavity_mean <=. 750968109/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • not (input.concave_points_worst <=. 1033944901/10000000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_mean <=. 6734710173/500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • not (input.radius_se <=. 2603237151/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • not (input.concavity_mean <=. 242844787/2500000000)
              • input.concave_points_worst <=. 181786853/1250000000
              • input.radius_se <=. 2603237151/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • not (input.concavity_mean <=. 40089141/500000000)
              • input.concave_points_worst <=. 1033944901/10000000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 302648569/2500000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_se <=. 166049107/312500000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_se <=. 166049107/312500000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • input.radius_se <=. 166049107/312500000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • input.radius_se <=. 166049107/312500000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_se <=. 166049107/312500000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.radius_se <=. 636920371/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_se <=. 166049107/312500000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_se <=. 166049107/312500000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.radius_se <=. 636920371/2500000000
              • input.radius_se <=. 166049107/312500000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.radius_se <=. 636920371/2500000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.radius_se <=. 636920371/2500000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.radius_se <=. 636920371/2500000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.radius_se <=. 636920371/2500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.radius_se <=. 636920371/2500000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.radius_se <=. 636920371/2500000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.radius_se <=. 636920371/2500000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.radius_se <=. 636920371/2500000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • not (input.concave_points_worst <=. 721645811/5000000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • not (input.concave_points_worst <=. 1146040843/10000000000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "malignant"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • not (input.radius_mean <=. 6734710173/500000000)
              • input.concave_points_worst <=. 1146040843/10000000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • input.radius_mean <=. 6734710173/500000000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • not (input.concavity_worst <=. 1300460631/5000000000)
              • input.concave_points_worst <=. 721645811/5000000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • input.radius_mean <=. 6734710173/500000000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 8636759/78125000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 8636759/78125000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 8636759/78125000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • not (input.concave_points_worst <=. 1093995829/10000000000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • not (input.concavity_worst <=. 192883107/1000000000)
              • input.concave_points_worst <=. 8636759/78125000
              • input.concave_points_worst <=. 1093995829/10000000000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • not (input.concave_points_worst <=. 8636759/78125000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • not (input.concavity_worst <=. 728215971/5000000000)
              • input.concave_points_worst <=. 8636759/78125000
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • not (input.concave_points_worst <=. 8636759/78125000)
              "benign"
              • input.concavity_mean <=. 40089141/500000000
              • input.radius_mean <=. 7527903347/500000000
              • input.concavity_worst <=. 1300460631/5000000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              • input.concavity_mean <=. 242844787/2500000000
              • input.concavity_worst <=. 192883107/1000000000
              • input.concavity_worst <=. 728215971/5000000000
              • input.concave_points_worst <=. 8636759/78125000
              "benign"
              In [12]:
              Decompose.top "tree_0"
              
              Out[12]:
              - : Imandra_interactive.Decompose.t list =
              [<region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>]
              
              Regions details

              No group selected.

              • Concrete regions are numbered
              • Unnumbered regions are groups whose children share a particular constraint
              • Click on a region to view its details
              • Double click on a region to zoom in on it
              • Shift+double click to zoom out
              • Hit escape to reset back to the top
              ConstraintsInvariant
              • not (f_2 <=. -2163/20000)
              • not (f_6 <=. 2453/25000)
              • not (f_2 <=. 265413/100000)
              (7, 5)
              • not (f_2 <=. -2163/20000)
              • not (f_6 <=. 2453/25000)
              • f_2 <=. 265413/100000
              (6, 128)
              • not (f_2 <=. -2163/20000)
              • f_6 <=. 2453/25000
              • not (f_6 <=. -17063/100000)
              (4, 2)
              • not (f_2 <=. -2163/20000)
              • f_6 <=. 2453/25000
              • f_6 <=. -17063/100000
              (24, 0)
              • f_2 <=. -2163/20000
              • not (f_0 <=. 6587/25000)
              • not (f_3 <=. -13559/25000)
              (3, 7)
              • f_2 <=. -2163/20000
              • not (f_0 <=. 6587/25000)
              • f_3 <=. -13559/25000
              (8, 2)
              • f_2 <=. -2163/20000
              • f_0 <=. 6587/25000
              • not (f_6 <=. -193/3125)
              (17, 5)
              • f_2 <=. -2163/20000
              • f_0 <=. 6587/25000
              • f_6 <=. -193/3125
              (236, 1)

              We can also use side conditions on the region decomposition of our model by using the ~assuming: flag. One application here is in simulating partial observability. Perhaps we know most of the measurements for a particular set of cells and we'd like to see how the classification of the input depends on the remaining features. Let's imagine that we only have the concavity measurements for a particular patient's cell sample and we'd like to see how the output of our model depends on the values of the other features.

              In [13]:
              let partial_observation x =
                is_valid_rf x &&
                x.concavity_mean = 0.04295 &&
                x.concavity_worst = 0.26000 &&
                x.concave_points_worst = 0.11460;;
              
              Decompose.top ~ctx_asm_simp:true ~assuming:"partial_observation" "rf_model"
              
              Out[13]:
              val partial_observation : rf_input -> bool = <fun>
              - : Imandra_interactive.Decompose.t list =
              [<region>; <region>; <region>; <region>; <region>; <region>; <region>;
               <region>; <region>]
              
              Regions details

              No group selected.

              • Concrete regions are numbered
              • Unnumbered regions are groups whose children share a particular constraint
              • Click on a region to view its details
              • Double click on a region to zoom in on it
              • Shift+double click to zoom out
              • Hit escape to reset back to the top
              ConstraintsInvariant
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 8271055011/500000000)
              • not (input.radius_se <=. 166049107/312500000)
              "malignant"
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.radius_se <=. 166049107/312500000
              "malignant"
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              "benign"
              • not (input.radius_mean <=. 7527903347/500000000)
              • not (input.radius_se <=. 636920371/2500000000)
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              "benign"
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.radius_se <=. 636920371/2500000000
              • not (input.radius_mean <=. 8271055011/500000000)
              • input.radius_se <=. 166049107/312500000
              "benign"
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.radius_se <=. 636920371/2500000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              "benign"
              • not (input.radius_mean <=. 7527903347/500000000)
              • input.radius_se <=. 636920371/2500000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              "benign"
              • input.radius_mean <=. 7527903347/500000000
              • input.radius_mean <=. 8271055011/500000000
              • not (input.compactness_mean <=. 30206321/500000000)
              "benign"
              • input.radius_mean <=. 7527903347/500000000
              • input.radius_mean <=. 8271055011/500000000
              • input.compactness_mean <=. 30206321/500000000
              "benign"

              Regression

              In a regression task we want to learn to predict the value(s) of some variable(s) based on previous data. In the commonly used Forest Fires dataset the aim is to predict the area burned by forest fires, in the northeast region of Portugal, by using meteorological and other data. This is a fairly difficult task and while the neural network below doesn't achieve state-of-the-art performance, it's enough to demonstrate how we can analyse relatively simple models in Imandra. In the dataset we have the following variables:

              1. X-axis spatial coordinate (within the Montesinho park map)
              2. Y-axis spatial coordinate (within the Montesinho park map)
              3. Month
              4. Day
              5. FFMC index (from the FWI system)
              6. DMC index (from the FWI system)
              7. DC index (from the FWI system)
              8. ISI index (from the FWI system)
              9. Temperature
              10. Relative percentage humidity
              11. Wind speed
              12. Rainfall
              13. Area of forest burned

              We again pre-process the data before learning by first transforming the month and day variables into a numerical value and applying a sine transformation (so that similar times are close in value), as well as removing outliers and applying an approximate logarithmic transformation to the area variable (as recommended in the dataset description). Each variable is scaled to lie between 0 and 1, and those with high correlations and/or low mutual information respect to the target variable are removed. We then split the data into training (80%) and test (20%) sets and use Keras to learn a simple feed-forward neural network with one (6 neuron) hidden layer, ReLU activation functions, and stochastic gradient descent to optimise the mean squared error. After saving our model as a .h5 file we use a short Python script to extract the network into an IML file and reason about it using Imandra.

              In [14]:
              let relu x = Real.(if x > 0.0 then x else 0.0);;
              
              let linear x = Real.(x)
              
              let layer_0 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
                let y_0 = relu @@ (0.20124)*x_0 + (-0.15722)*x_1 + (-0.19063)*x_2 + (-0.54562)*x_3 + (0.03425)*x_4 + (0.50104)*x_5 + -0.02768 in
                let y_1 = relu @@ (0.29103)*x_0 + (0.03180)*x_1 + (-0.16336)*x_2 + (0.17919)*x_3 + (0.32971)*x_4 + (-0.43206)*x_5 + -0.02620 in
                let y_2 = relu @@ (0.66419)*x_0 + (0.25399)*x_1 + (0.00449)*x_2 + (0.03841)*x_3 + (-0.51482)*x_4 + (0.58299)*x_5 + 0.11858 in
                let y_3 = relu @@ (0.47598)*x_0 + (-0.36142)*x_1 + (0.38981)*x_2 + (0.27632)*x_3 + (-0.61231)*x_4 + (-0.03662)*x_5 + -0.02890 in
                let y_4 = relu @@ (0.10277)*x_0 + (-0.28841)*x_1 + (0.04637)*x_2 + (0.28808)*x_3 + (0.05957)*x_4 + (-0.22041)*x_5 + 0.18270 in
                let y_5 = relu @@ (0.55604)*x_0 + (-0.04015)*x_1 + (0.10557)*x_2 + (0.60757)*x_3 + (-0.32314)*x_4 + (0.47933)*x_5 + -0.24876 in
                (y_0, y_1, y_2, y_3, y_4, y_5)
              
              let layer_1 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
                let y_0 = linear @@ (0.28248)*x_0 + (-0.25208)*x_1 + (-0.50075)*x_2 + (-0.07092)*x_3 + (-0.43189)*x_4 + (0.60065)*x_5 + 0.47136 in
                (y_0)
              
              let nn (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
                (x_0, x_1, x_2, x_3, x_4, x_5) |> layer_0 |> layer_1
              
              Out[14]:
              val relu : real -> real = <fun>
              val linear : 'a -> 'a = <fun>
              val layer_0 :
                real * real * real * real * real * real ->
                real * real * real * real * real * real = <fun>
              val layer_1 : real * real * real * real * real * real -> real = <fun>
              val nn : real * real * real * real * real * real -> real = <fun>
              

              Given the description of the dataset above we can again create some custom input types in Imandra for our model.

              In [15]:
              type month = Jan | Feb | Mar | Apr | May | Jun| Jul | Aug | Sep | Oct | Nov | Dec
              
              type day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
              
              type nn_input = {
                month : month;
                day : day;
                dmc : real;
                temp : real;
                rh : real;
                rain : real
              }
              
              Out[15]:
              type month =
                  Jan
                | Feb
                | Mar
                | Apr
                | May
                | Jun
                | Jul
                | Aug
                | Sep
                | Oct
                | Nov
                | Dec
              type day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
              type nn_input = {
                month : month;
                day : day;
                dmc : real;
                temp : real;
                rh : real;
                rain : real;
              }
              

              As before, because we pre-processed our data, we'll add in a function applying this transform to each input variable. Equally, we'll need to convert back to hectares for our output variable, again using some minimum and maximum values extracted during our data pre-processing stage. After that we define a full model which combines these pre/post-processing steps and the network above.

              In [16]:
              let month_2_num = let open Real in function
                | Jan -> 0.134
                | Feb -> 0.500
                | Mar -> 1.000
                | Apr -> 1.500
                | May -> 1.866
                | Jun -> 2.000
                | Jul -> 1.866
                | Aug -> 1.500
                | Sep -> 1.000
                | Oct -> 0.500
                | Nov -> 0.133
                | Dec -> 0.000
              
              let day_2_num = let open Real in function
                | Mon -> 0.377
                | Tue -> 1.223
                | Wed -> 1.901
                | Thu -> 1.901
                | Fri -> 1.223
                | Sat -> 0.377
                | Sun -> 0.000
              
              let process_nn_input input = let open Real in
                let real_month = month_2_num input.month in
                let real_day = day_2_num input.day in
                let x_0 = (real_month - 0.0)  / (2.0   - 0.0)  in
                let x_1 = (real_day   - 0.0)  / (1.901 - 0.0)  in
                let x_2 = (input.dmc  - 1.1)  / (291.3 - 1.1)  in
                let x_3 = (input.temp - 2.2)  / (33.3  - 2.2)  in
                let x_4 = (input.rh   - 15.0) / (100.0 - 15.0) in
                let x_5 = (input.rain - 0.0)  / (6.40  - 0.0)  in
                (x_0, x_1, x_2, x_3, x_4, x_5)
              
              let process_nn_output y_0 = let open Real in
                let y = 4.44323 * y_0 in
                if y <= 1.0 then (y - 0.00000) * 1.71828 else
                if y <= 2.0 then (y - 0.63212) * 4.67077 else
                if y <= 3.0 then (y - 1.49679) * 12.69648 else
                if y <= 4.0 then (y - 2.44700) * 34.51261 else
                (y - 3.42868) * 93.81501
              
              let nn_model input = input |> process_nn_input |> nn |> process_nn_output
              
              Out[16]:
              val month_2_num : month -> Q.t = <fun>
              val day_2_num : day -> Q.t = <fun>
              val process_nn_input : nn_input -> real * real * real * real * real * real =
                <fun>
              val process_nn_output : real -> real = <fun>
              val nn_model : nn_input -> real = <fun>
              

              Let's start as in the previous section by running a datum from our dataset through the model. In particular, we'll input x = (Aug, Sat, 231.1, 26.9, 31.0, 0.0) which has an area of y = 4.96 hectares in the data.

              In [17]:
              let x = {
                month = Aug;
                day = Sat;
                dmc = 231.1;
                temp = 26.9;
                rh = 31.0;
                rain = 0.0
              }
              
              let y = nn_model x
              
              Out[17]:
              val x : nn_input =
                {month = Aug; day = Sat; dmc = 231.1; temp = 26.9; rh = 31.; rain = 0.}
              val y : real = 2.1368837387
              

              Our answer is both roughly similar to the recorded datapoint value and also to the value we get from our original Keras model, 2.13683266556. The small disparity here is due to our rounding the weight values in our network to 5 decimal places when we extracted them to IML, though it wasn't necessary to do so. Now we'll use Imandra to generate an example for us with some particular side conditions.

              In [18]:
              instance (fun x -> nn_model x >. 20.0 && x.temp = 20.0 && x.month = May)
              
              Out[18]:
              - : nn_input -> bool = <fun>
              module CX : sig val x : nn_input end
              
              Instance (after 0 steps, 0.075s):
               let (x : nn_input) =
                 {month = May; day = Wed;
                  dmc =
                   (Real.mk_of_string "7597491365091646983788244502461274105063710103/1285912235995896196222304684839556138615000");
                  temp = 20.0;
                  rh =
                   (Real.mk_of_string "116321417146729453300761696944820485610293761/51436489439835847848892187393582245544600");
                  rain =
                   (Real.mk_of_string "2495451056678694134139316951586229474021508/32147805899897404905557617120988903465375")}
              
              Instance
              proof attempt
              ground_instances0
              definitions0
              inductions0
              search_time
              0.075s
              details
              Expand
              smt_stats
              num checks1
              arith assert lower58
              arith pivots25
              rlimit count15745
              mk clause69
              datatype occurs check7
              mk bool var145
              arith assert upper36
              datatype splits4
              decisions70
              arith add rows132
              arith bound prop1
              propagations92
              conflicts7
              arith fixed eqs13
              datatype accessor ax10
              arith conflicts2
              arith assert diseq1
              datatype constructor ax11
              final checks1
              added eqs102
              del clause24
              arith eq adapter31
              memory570.920000
              max memory909.420000
              num allocs8267399245171.000000
              Expand
              • start[0.075s]
                  (if (444323/100000
                       *. ((((((3531/12500
                                *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                            +. -19063/100000 *. …)
                                           +. -27281/50000 *. …)
                                          +. 137/4000 *. …)
                                         +. 6263/12500 *. …)
                                        +. -173/6250)
                                       >. 0
                                    then
                                      (((((5031/25000 *. … +. -7861/50000 *. …)
                                          +. -19063/100000 *. …)
                                         +. -27281/50000 *. …)
                                        +. 137/4000 *. …)
                                       +. 6263/12500 *. …)
                                      +. -173/6250
                                    else 0)
                                +. -3151/12500
                                   *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                               +. -1021/6250 *. …)
                                              +. 17919/100000 *. …)
                                             +. 32971/100000 *. …)
                                            +. -21603/50000 *. …)
                                           +. -131/5000)
                                          >. 0
                                       then
                                         (((((29103/100000 *. … +. 159/5000 *. …)
                                             +. -1021/6250 *. …)
                                            +. 17919/100000 *. …)
                                           +. 32971/100000 *. …)
                                          +. -21603/50000 *. …)
                                         +. -131/5000
                                       else 0))
                               +. -2003/4000
                                  *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                              +. 449/100000 *. …)
                                             +. 3841/100000 *. …)
                                            +. -25741/50000 *. …)
                                           +. 58299/100000 *. …)
                                          +. 5929/50000)
                                         >. 0
                                      then
                                        (((((66419/100000 *. … +. 25399/100000 *. …)
                                            +. 449/100000 *. …)
                                           +. 3841/100000 *. …)
                                          +. -25741/50000 *. …)
                                         +. 58299/100000 *. …)
                                        +. 5929/50000
                                      else 0))
                              +. -1773/25000
                                 *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                             +. 38981/100000 *. …)
                                            +. 1727/6250 *. …)
                                           +. -61231/100000 *. …)
                                          +. -1831/50000 *. …)
                                         +. -289/10000)
                                        >. 0
                                     then
                                       (((((23799/50000 *. … +. -18071/50000 *. …)
                                           +. 38981/100000 *. …)
                                          +. 1727/6250 *. …)
                                         +. -61231/100000 *. …)
                                        +. -1831/50000 *. …)
                                       +. -289/10000
                                     else 0))
                             +. -43189/100000
                                *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                            +. 4637/100000 *. …)
                                           +. 3601/12500 *. …)
                                          +. 5957/100000 *. …)
                                         +. -22041/100000 *. …)
                                        +. 1827/10000)
                                       >. 0
                                    then
                                      (((((10277/100000 *. … +. -28841/100000 *. …)
                                          +. 4637/100000 *. …)
                                         +. 3601/12500 *. …)
                                        +. 5957/100000 *. …)
                                       +. -22041/100000 *. …)
                                      +. 1827/10000
                                    else 0))
                            +. 12013/20000
                               *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                           +. 10557/100000 *. …)
                                          +. 60757/100000 *. …)
                                         +. -16157/50000 *. …)
                                        +. 47933/100000 *. …)
                                       +. -6219/25000)
                                      >. 0
                                   then
                                     (((((13901/25000 *. … +. -803/20000 *. …)
                                         +. 10557/100000 *. …)
                                        +. 60757/100000 *. …)
                                       +. -16157/50000 *. …)
                                      +. 47933/100000 *. …)
                                     +. -6219/25000
                                   else 0))
                           +. 1473/3125))
                      <=. 1
                   then
                     (444323/100000
                      *. ((((((3531/12500
                               *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                           +. -19063/100000 *. …)
                                          +. -27281/50000 *. …)
                                         +. 137/4000 *. …)
                                        +. 6263/12500 *. …)
                                       +. -173/6250)
                                      >. 0
                                   then
                                     (((((5031/25000 *. … +. -7861/50000 *. …)
                                         +. -19063/100000 *. …)
                                        +. -27281/50000 *. …)
                                       +. 137/4000 *. …)
                                      +. 6263/12500 *. …)
                                     +. -173/6250
                                   else 0)
                               +. -3151/12500
                                  *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                              +. -1021/6250 *. …)
                                             +. 17919/100000 *. …)
                                            +. 32971/100000 *. …)
                                           +. -21603/50000 *. …)
                                          +. -131/5000)
                                         >. 0
                                      then
                                        (((((29103/100000 *. … +. 159/5000 *. …)
                                            +. -1021/6250 *. …)
                                           +. 17919/100000 *. …)
                                          +. 32971/100000 *. …)
                                         +. -21603/50000 *. …)
                                        +. -131/5000
                                      else 0))
                              +. -2003/4000
                                 *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                             +. 449/100000 *. …)
                                            +. 3841/100000 *. …)
                                           +. -25741/50000 *. …)
                                          +. 58299/100000 *. …)
                                         +. 5929/50000)
                                        >. 0
                                     then
                                       (((((66419/100000 *. … +. 25399/100000 *. …)
                                           +. 449/100000 *. …)
                                          +. 3841/100000 *. …)
                                         +. -25741/50000 *. …)
                                        +. 58299/100000 *. …)
                                       +. 5929/50000
                                     else 0))
                             +. -1773/25000
                                *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                            +. 38981/100000 *. …)
                                           +. 1727/6250 *. …)
                                          +. -61231/100000 *. …)
                                         +. -1831/50000 *. …)
                                        +. -289/10000)
                                       >. 0
                                    then
                                      (((((23799/50000 *. … +. -18071/50000 *. …)
                                          +. 38981/100000 *. …)
                                         +. 1727/6250 *. …)
                                        +. -61231/100000 *. …)
                                       +. -1831/50000 *. …)
                                      +. -289/10000
                                    else 0))
                            +. -43189/100000
                               *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                           +. 4637/100000 *. …)
                                          +. 3601/12500 *. …)
                                         +. 5957/100000 *. …)
                                        +. -22041/100000 *. …)
                                       +. 1827/10000)
                                      >. 0
                                   then
                                     (((((10277/100000 *. … +. -28841/100000 *. …)
                                         +. 4637/100000 *. …)
                                        +. 3601/12500 *. …)
                                       +. 5957/100000 *. …)
                                      +. -22041/100000 *. …)
                                     +. 1827/10000
                                   else 0))
                           +. 12013/20000
                              *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                          +. 10557/100000 *. …)
                                         +. 60757/100000 *. …)
                                        +. -16157/50000 *. …)
                                       +. 47933/100000 *. …)
                                      +. -6219/25000)
                                     >. 0
                                  then
                                    (((((13901/25000 *. … +. -803/20000 *. …)
                                        +. 10557/100000 *. …)
                                       +. 60757/100000 *. …)
                                      +. -16157/50000 *. …)
                                     +. 47933/100000 *. …)
                                    +. -6219/25000
                                  else 0))
                          +. 1473/3125))
                     -. 0 *. 42957/25000
                   else
                   if (444323/100000
                       *. ((((((3531/12500
                                *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                            +. -19063/100000 *. …)
                                           +. -27281/50000 *. …)
                                          +. 137/4000 *. …)
                                         +. 6263/12500 *. …)
                                        +. -173/6250)
                                       >. 0
                                    then
                                      (((((5031/25000 *. … +. -7861/50000 *. …)
                                          +. -19063/100000 *. …)
                                         +. -27281/50000 *. …)
                                        +. 137/4000 *. …)
                                       +. 6263/12500 *. …)
                                      +. -173/6250
                                    else 0)
                                +. -3151/12500
                                   *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                               +. -1021/6250 *. …)
                                              +. 17919/100000 *. …)
                                             +. 32971/100000 *. …)
                                            +. -21603/50000 *. …)
                                           +. -131/5000)
                                          >. 0
                                       then
                                         (((((29103/100000 *. … +. 159/5000 *. …)
                                             +. -1021/6250 *. …)
                                            +. 17919/100000 *. …)
                                           +. 32971/100000 *. …)
                                          +. -21603/50000 *. …)
                                         +. -131/5000
                                       else 0))
                               +. -2003/4000
                                  *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                              +. 449/100000 *. …)
                                             +. 3841/100000 *. …)
                                            +. -25741/50000 *. …)
                                           +. 58299/100000 *. …)
                                          +. 5929/50000)
                                         >. 0
                                      then
                                        (((((66419/100000 *. … +. 25399/100000 *. …)
                                            +. 449/100000 *. …)
                                           +. 3841/100000 *. …)
                                          +. -25741/50000 *. …)
                                         +. 58299/100000 *. …)
                                        +. 5929/50000
                                      else 0))
                              +. -1773/25000
                                 *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                             +. 38981/100000 *. …)
                                            +. 1727/6250 *. …)
                                           +. -61231/100000 *. …)
                                          +. -1831/50000 *. …)
                                         +. -289/10000)
                                        >. 0
                                     then
                                       (((((23799/50000 *. … +. -18071/50000 *. …)
                                           +. 38981/100000 *. …)
                                          +. 1727/6250 *. …)
                                         +. -61231/100000 *. …)
                                        +. -1831/50000 *. …)
                                       +. -289/10000
                                     else 0))
                             +. -43189/100000
                                *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                            +. 4637/100000 *. …)
                                           +. 3601/12500 *. …)
                                          +. 5957/100000 *. …)
                                         +. -22041/100000 *. …)
                                        +. 1827/10000)
                                       >. 0
                                    then
                                      (((((10277/100000 *. … +. -28841/100000 *. …)
                                          +. 4637/100000 *. …)
                                         +. 3601/12500 *. …)
                                        +. 5957/100000 *. …)
                                       +. -22041/100000 *. …)
                                      +. 1827/10000
                                    else 0))
                            +. 12013/20000
                               *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                           +. 10557/100000 *. …)
                                          +. 60757/100000 *. …)
                                         +. -16157/50000 *. …)
                                        +. 47933/100000 *. …)
                                       +. -6219/25000)
                                      >. 0
                                   then
                                     (((((13901/25000 *. … +. -803/20000 *. …)
                                         +. 10557/100000 *. …)
                                        +. 60757/100000 *. …)
                                       +. -16157/50000 *. …)
                                      +. 47933/100000 *. …)
                                     +. -6219/25000
                                   else 0))
                           +. 1473/3125))
                      <=. 2
                   then
                     (444323/100000
                      *. ((((((3531/12500
                               *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                           +. -19063/100000 *. …)
                                          +. -27281/50000 *. …)
                                         +. 137/4000 *. …)
                                        +. 6263/12500 *. …)
                                       +. -173/6250)
                                      >. 0
                                   then
                                     (((((5031/25000 *. … +. -7861/50000 *. …)
                                         +. -19063/100000 *. …)
                                        +. -27281/50000 *. …)
                                       +. 137/4000 *. …)
                                      +. 6263/12500 *. …)
                                     +. -173/6250
                                   else 0)
                               +. -3151/12500
                                  *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                              +. -1021/6250 *. …)
                                             +. 17919/100000 *. …)
                                            +. 32971/100000 *. …)
                                           +. -21603/50000 *. …)
                                          +. -131/5000)
                                         >. 0
                                      then
                                        (((((29103/100000 *. … +. 159/5000 *. …)
                                            +. -1021/6250 *. …)
                                           +. 17919/100000 *. …)
                                          +. 32971/100000 *. …)
                                         +. -21603/50000 *. …)
                                        +. -131/5000
                                      else 0))
                              +. -2003/4000
                                 *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                             +. 449/100000 *. …)
                                            +. 3841/100000 *. …)
                                           +. -25741/50000 *. …)
                                          +. 58299/100000 *. …)
                                         +. 5929/50000)
                                        >. 0
                                     then
                                       (((((66419/100000 *. … +. 25399/100000 *. …)
                                           +. 449/100000 *. …)
                                          +. 3841/100000 *. …)
                                         +. -25741/50000 *. …)
                                        +. 58299/100000 *. …)
                                       +. 5929/50000
                                     else 0))
                             +. -1773/25000
                                *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                            +. 38981/100000 *. …)
                                           +. 1727/6250 *. …)
                                          +. -61231/100000 *. …)
                                         +. -1831/50000 *. …)
                                        +. -289/10000)
                                       >. 0
                                    then
                                      (((((23799/50000 *. … +. -18071/50000 *. …)
                                          +. 38981/100000 *. …)
                                         +. 1727/6250 *. …)
                                        +. -61231/100000 *. …)
                                       +. -1831/50000 *. …)
                                      +. -289/10000
                                    else 0))
                            +. -43189/100000
                               *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                           +. 4637/100000 *. …)
                                          +. 3601/12500 *. …)
                                         +. 5957/100000 *. …)
                                        +. -22041/100000 *. …)
                                       +. 1827/10000)
                                      >. 0
                                   then
                                     (((((10277/100000 *. … +. -28841/100000 *. …)
                                         +. 4637/100000 *. …)
                                        +. 3601/12500 *. …)
                                       +. 5957/100000 *. …)
                                      +. -22041/100000 *. …)
                                     +. 1827/10000
                                   else 0))
                           +. 12013/20000
                              *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                          +. 10557/100000 *. …)
                                         +. 60757/100000 *. …)
                                        +. -16157/50000 *. …)
                                       +. 47933/100000 *. …)
                                      +. -6219/25000)
                                     >. 0
                                  then
                                    (((((13901/25000 *. … +. -803/20000 *. …)
                                        +. 10557/100000 *. …)
                                       +. 60757/100000 *. …)
                                      +. -16157/50000 *. …)
                                     +. 47933/100000 *. …)
                                    +. -6219/25000
                                  else 0))
                          +. 1473/3125))
                     -. 15803/25000 *. 467077/100000
                   else
                   if (444323/100000
                       *. ((((((3531/12500
                                *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                            +. -19063/100000 *. …)
                                           +. -27281/50000 *. …)
                                          +. 137/4000 *. …)
                                         +. 6263/12500 *. …)
                                        +. -173/6250)
                                       >. 0
                                    then
                                      (((((5031/25000 *. … +. -7861/50000 *. …)
                                          +. -19063/100000 *. …)
                                         +. -27281/50000 *. …)
                                        +. 137/4000 *. …)
                                       +. 6263/12500 *. …)
                                      +. -173/6250
                                    else 0)
                                +. -3151/12500
                                   *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                               +. -1021/6250 *. …)
                                              +. 17919/100000 *. …)
                                             +. 32971/100000 *. …)
                                            +. -21603/50000 *. …)
                                           +. -131/5000)
                                          >. 0
                                       then
                                         (((((29103/100000 *. … +. 159/5000 *. …)
                                             +. -1021/6250 *. …)
                                            +. 17919/100000 *. …)
                                           +. 32971/100000 *. …)
                                          +. -21603/50000 *. …)
                                         +. -131/5000
                                       else 0))
                               +. -2003/4000
                                  *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                              +. 449/100000 *. …)
                                             +. 3841/100000 *. …)
                                            +. -25741/50000 *. …)
                                           +. 58299/100000 *. …)
                                          +. 5929/50000)
                                         >. 0
                                      then
                                        (((((66419/100000 *. … +. 25399/100000 *. …)
                                            +. 449/100000 *. …)
                                           +. 3841/100000 *. …)
                                          +. -25741/50000 *. …)
                                         +. 58299/100000 *. …)
                                        +. 5929/50000
                                      else 0))
                              +. -1773/25000
                                 *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                             +. 38981/100000 *. …)
                                            +. 1727/6250 *. …)
                                           +. -61231/100000 *. …)
                                          +. -1831/50000 *. …)
                                         +. -289/10000)
                                        >. 0
                                     then
                                       (((((23799/50000 *. … +. -18071/50000 *. …)
                                           +. 38981/100000 *. …)
                                          +. 1727/6250 *. …)
                                         +. -61231/100000 *. …)
                                        +. -1831/50000 *. …)
                                       +. -289/10000
                                     else 0))
                             +. -43189/100000
                                *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                            +. 4637/100000 *. …)
                                           +. 3601/12500 *. …)
                                          +. 5957/100000 *. …)
                                         +. -22041/100000 *. …)
                                        +. 1827/10000)
                                       >. 0
                                    then
                                      (((((10277/100000 *. … +. -28841/100000 *. …)
                                          +. 4637/100000 *. …)
                                         +. 3601/12500 *. …)
                                        +. 5957/100000 *. …)
                                       +. -22041/100000 *. …)
                                      +. 1827/10000
                                    else 0))
                            +. 12013/20000
                               *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                           +. 10557/100000 *. …)
                                          +. 60757/100000 *. …)
                                         +. -16157/50000 *. …)
                                        +. 47933/100000 *. …)
                                       +. -6219/25000)
                                      >. 0
                                   then
                                     (((((13901/25000 *. … +. -803/20000 *. …)
                                         +. 10557/100000 *. …)
                                        +. 60757/100000 *. …)
                                       +. -16157/50000 *. …)
                                      +. 47933/100000 *. …)
                                     +. -6219/25000
                                   else 0))
                           +. 1473/3125))
                      <=. 3
                   then
                     (444323/100000
                      *. ((((((3531/12500
                               *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                           +. -19063/100000 *. …)
                                          +. -27281/50000 *. …)
                                         +. 137/4000 *. …)
                                        +. 6263/12500 *. …)
                                       +. -173/6250)
                                      >. 0
                                   then
                                     (((((5031/25000 *. … +. -7861/50000 *. …)
                                         +. -19063/100000 *. …)
                                        +. -27281/50000 *. …)
                                       +. 137/4000 *. …)
                                      +. 6263/12500 *. …)
                                     +. -173/6250
                                   else 0)
                               +. -3151/12500
                                  *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                              +. -1021/6250 *. …)
                                             +. 17919/100000 *. …)
                                            +. 32971/100000 *. …)
                                           +. -21603/50000 *. …)
                                          +. -131/5000)
                                         >. 0
                                      then
                                        (((((29103/100000 *. … +. 159/5000 *. …)
                                            +. -1021/6250 *. …)
                                           +. 17919/100000 *. …)
                                          +. 32971/100000 *. …)
                                         +. -21603/50000 *. …)
                                        +. -131/5000
                                      else 0))
                              +. -2003/4000
                                 *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                             +. 449/100000 *. …)
                                            +. 3841/100000 *. …)
                                           +. -25741/50000 *. …)
                                          +. 58299/100000 *. …)
                                         +. 5929/50000)
                                        >. 0
                                     then
                                       (((((66419/100000 *. … +. 25399/100000 *. …)
                                           +. 449/100000 *. …)
                                          +. 3841/100000 *. …)
                                         +. -25741/50000 *. …)
                                        +. 58299/100000 *. …)
                                       +. 5929/50000
                                     else 0))
                             +. -1773/25000
                                *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                            +. 38981/100000 *. …)
                                           +. 1727/6250 *. …)
                                          +. -61231/100000 *. …)
                                         +. -1831/50000 *. …)
                                        +. -289/10000)
                                       >. 0
                                    then
                                      (((((23799/50000 *. … +. -18071/50000 *. …)
                                          +. 38981/100000 *. …)
                                         +. 1727/6250 *. …)
                                        +. -61231/100000 *. …)
                                       +. -1831/50000 *. …)
                                      +. -289/10000
                                    else 0))
                            +. -43189/100000
                               *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                           +. 4637/100000 *. …)
                                          +. 3601/12500 *. …)
                                         +. 5957/100000 *. …)
                                        +. -22041/100000 *. …)
                                       +. 1827/10000)
                                      >. 0
                                   then
                                     (((((10277/100000 *. … +. -28841/100000 *. …)
                                         +. 4637/100000 *. …)
                                        +. 3601/12500 *. …)
                                       +. 5957/100000 *. …)
                                      +. -22041/100000 *. …)
                                     +. 1827/10000
                                   else 0))
                           +. 12013/20000
                              *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                          +. 10557/100000 *. …)
                                         +. 60757/100000 *. …)
                                        +. -16157/50000 *. …)
                                       +. 47933/100000 *. …)
                                      +. -6219/25000)
                                     >. 0
                                  then
                                    (((((13901/25000 *. … +. -803/20000 *. …)
                                        +. 10557/100000 *. …)
                                       +. 60757/100000 *. …)
                                      +. -16157/50000 *. …)
                                     +. 47933/100000 *. …)
                                    +. -6219/25000
                                  else 0))
                          +. 1473/3125))
                     -. 149679/100000 *. 79353/6250
                   else
                   if (444323/100000
                       *. ((((((3531/12500
                                *. (if ((((((5031/25000 *. … +. -7861/50000 *. …)
                                            +. -19063/100000 *. …)
                                           +. -27281/50000 *. …)
                                          +. 137/4000 *. …)
                                         +. 6263/12500 *. …)
                                        +. -173/6250)
                                       >. 0
                                    then
                                      (((((5031/25000 *. … +. -7861/50000 *. …)
                                          +. -19063/100000 *. …)
                                         +. -27281/50000 *. …)
                                        +. 137/4000 *. …)
                                       +. 6263/12500 *. …)
                                      +. -173/6250
                                    else 0)
                                +. -3151/12500
                                   *. (if ((((((29103/100000 *. … +. 159/5000 *. …)
                                               +. -1021/6250 *. …)
                                              +. 17919/100000 *. …)
                                             +. 32971/100000 *. …)
                                            +. -21603/50000 *. …)
                                           +. -131/5000)
                                          >. 0
                                       then
                                         (((((29103/100000 *. … +. 159/5000 *. …)
                                             +. -1021/6250 *. …)
                                            +. 17919/100000 *. …)
                                           +. 32971/100000 *. …)
                                          +. -21603/50000 *. …)
                                         +. -131/5000
                                       else 0))
                               +. -2003/4000
                                  *. (if ((((((66419/100000 *. … +. 25399/100000 *. …)
                                              +. 449/100000 *. …)
                                             +. 3841/100000 *. …)
                                            +. -25741/50000 *. …)
                                           +. 58299/100000 *. …)
                                          +. 5929/50000)
                                         >. 0
                                      then
                                        (((((66419/100000 *. … +. 25399/100000 *. …)
                                            +. 449/100000 *. …)
                                           +. 3841/100000 *. …)
                                          +. -25741/50000 *. …)
                                         +. 58299/100000 *. …)
                                        +. 5929/50000
                                      else 0))
                              +. -1773/25000
                                 *. (if ((((((23799/50000 *. … +. -18071/50000 *. …)
                                             +. 38981/100000 *. …)
                                            +. 1727/6250 *. …)
                                           +. -61231/100000 *. …)
                                          +. -1831/50000 *. …)
                                         +. -289/10000)
                                        >. 0
                                     then
                                       (((((23799/50000 *. … +. -18071/50000 *. …)
                                           +. 38981/100000 *. …)
                                          +. 1727/6250 *. …)
                                         +. -61231/100000 *. …)
                                        +. -1831/50000 *. …)
                                       +. -289/10000
                                     else 0))
                             +. -43189/100000
                                *. (if ((((((10277/100000 *. … +. -28841/100000 *. …)
                                            +. 4637/100000 *. …)
                                           +. 3601/12500 *. …)
                                          +. 5957/100000 *. …)
                                         +. -22041/100000 *. …)
                                        +. 1827/10000)
                                       >. 0
                                    then
                                      (((((10277/100000 *. … +. -28841/100000 *. …)
                                          +. 4637/100000 *. …)
                                         +. 3601/12500 *. …)
                                        +. 5957/100000 *. …)
                                       +. -22041/100000 *. …)
                                      +. 1827/10000
                                    else 0))
                            +. 12013/20000
                               *. (if ((((((13901/25000 *. … +. -803/20000 *. …)
                                           +. 10557/100000 *. …)
                                          +. 60757/100000 *. …)
                                         +. -16157/50000 *. …)
                                        +. 47933/100000 *. …)
                                       +. -6219/25000)
                                      >. 0
                                   then
                                     (((((13901/25000 *. … +. -803/20000 *. …)
                                         +. 10557/100000 *. …)
                                        +. 60757/100000 *. …)
                                       +. -16157/50000 *. …)
                                      +. 47933/100000 *. …)
                                     +. -6219/25000
                                   else 0))
                           +. 1473/3125))
                      <=. 4
                   then … else …)
                  >. 20 && :var_0:.temp = 20 && :var_0:.month = May
              • simplify

                into
                (not
                 ((if (((((1568904513/1250000000
                           *. (if (((((5031/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -7861/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -19063/29020000 *. :var_0:.dmc)
                                     +. -27281/1555000 *. :var_0:.temp)
                                    +. 137/340000 *. :var_0:.rh)
                                   +. 6263/80000 *. :var_0:.rain)
                                  <=. -1716983137/306857480000
                               then 0
                               else
                                 ((((((1716983137/306857480000
                                       +. 5031/50000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -7861/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. -19063/29020000 *. :var_0:.dmc)
                                    +. -27281/1555000 *. :var_0:.temp)
                                   +. 137/340000 *. :var_0:.rh)
                                  +. 6263/80000 *. :var_0:.rain))
                           +. -1400061773/1250000000
                              *. (if (((((29103/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …)
                                          +. 159/9505
                                             *. (if :var_0:.day = Mon then 377/1000
                                                 else
                                                 if :var_0:.day = Tue then 1223/1000
                                                 else
                                                 if :var_0:.day = Wed then 1901/1000
                                                 else
                                                 if :var_0:.day = Thu then 1901/1000 else …))
                                         +. -1021/1813750 *. :var_0:.dmc)
                                        +. 17919/3110000 *. :var_0:.temp)
                                       +. 32971/8500000 *. :var_0:.rh)
                                      +. -21603/320000 *. :var_0:.rain)
                                     <=. 73983893263/767143700000
                                  then 0
                                  else
                                    ((((((-73983893263/767143700000
                                          +. 29103/200000
                                             *. (if :var_0:.month = Jan then 67/500
                                                 else
                                                 if :var_0:.month = Feb then 1/2
                                                 else
                                                 if :var_0:.month = Mar then 1
                                                 else
                                                 if :var_0:.month = Apr then 3/2 else …))
                                         +. 159/9505
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -1021/1813750 *. :var_0:.dmc)
                                       +. 17919/3110000 *. :var_0:.temp)
                                      +. 32971/8500000 *. :var_0:.rh)
                                     +. -21603/320000 *. :var_0:.rain)))
                          +. -889978969/400000000
                             *. (if (((((66419/200000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. 25399/190100
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. 449/29020000 *. :var_0:.dmc)
                                       +. 3841/3110000 *. :var_0:.temp)
                                      +. -25741/4250000 *. :var_0:.rh)
                                     +. 58299/640000 *. :var_0:.rain)
                                    <=. -317131778543/1534287400000
                                 then 0
                                 else
                                   ((((((317131778543/1534287400000
                                         +. 66419/200000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. 25399/190100
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 449/29020000 *. :var_0:.dmc)
                                      +. 3841/3110000 *. :var_0:.temp)
                                     +. -25741/4250000 *. :var_0:.rh)
                                    +. 58299/640000 *. :var_0:.rain)))
                         +. -787784679/2500000000
                            *. (if (((((23799/100000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. -18071/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 38981/29020000 *. :var_0:.dmc)
                                      +. 1727/194375 *. :var_0:.temp)
                                     +. -61231/8500000 *. :var_0:.rh)
                                    +. -1831/320000 *. :var_0:.rain)
                                   <=. -89188713933/1534287400000
                                then 0
                                else
                                  ((((((89188713933/1534287400000
                                        +. 23799/100000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. -18071/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 38981/29020000 *. :var_0:.dmc)
                                     +. 1727/194375 *. :var_0:.temp)
                                    +. -61231/8500000 *. :var_0:.rh)
                                   +. -1831/320000 *. :var_0:.rain)))
                        +. -19189866047/10000000000
                           *. (if (((((10277/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -28841/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 4637/29020000 *. :var_0:.dmc)
                                     +. 3601/388750 *. :var_0:.temp)
                                    +. 5957/8500000 *. :var_0:.rh)
                                   +. -22041/640000 *. :var_0:.rain)
                                  <=. -372238333/2454859840
                               then 0
                               else
                                 ((((((372238333/2454859840
                                       +. 10277/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -28841/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 4637/29020000 *. :var_0:.dmc)
                                    +. 3601/388750 *. :var_0:.temp)
                                   +. 5957/8500000 *. :var_0:.rh)
                                  +. -22041/640000 *. :var_0:.rain)))
                       +. 5337652199/2000000000
                          *. (if (((((13901/50000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -803/38020
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 10557/29020000 *. :var_0:.dmc)
                                    +. 60757/3110000 *. :var_0:.temp)
                                   +. -16157/4250000 *. :var_0:.rh)
                                  +. 47933/640000 *. :var_0:.rain)
                                 <=. 72146699557/306857480000
                              then 0
                              else
                                ((((((-72146699557/306857480000
                                      +. 13901/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -803/38020
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 10557/29020000 *. :var_0:.dmc)
                                   +. 60757/3110000 *. :var_0:.temp)
                                  +. -16157/4250000 *. :var_0:.rh)
                                 +. 47933/640000 *. :var_0:.rain)))
                      <=. -341987779/312500000
                   then
                     (((((28114831522503/7812500000000
                          +. 67395431164941/31250000000000
                             *. (if (((((5031/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. -7861/95050
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -19063/29020000 *. :var_0:.dmc)
                                       +. -27281/1555000 *. :var_0:.temp)
                                      +. 137/340000 *. :var_0:.rh)
                                     +. 6263/80000 *. :var_0:.rain)
                                    <=. -1716983137/306857480000
                                 then 0
                                 else
                                   ((((((1716983137/306857480000
                                         +. 5031/50000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. -7861/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -19063/29020000 *. :var_0:.dmc)
                                      +. -27281/1555000 *. :var_0:.temp)
                                     +. 137/340000 *. :var_0:.rh)
                                    +. 6263/80000 *. :var_0:.rain)))
                         +. -60142453582761/31250000000000
                            *. (if (((((29103/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. 159/9505
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -1021/1813750 *. :var_0:.dmc)
                                      +. 17919/3110000 *. :var_0:.temp)
                                     +. 32971/8500000 *. :var_0:.rh)
                                    +. -21603/320000 *. :var_0:.rain)
                                   <=. 73983893263/767143700000
                                then 0
                                else
                                  ((((((-73983893263/767143700000
                                        +. 29103/200000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. 159/9505
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -1021/1813750 *. :var_0:.dmc)
                                     +. 17919/3110000 *. :var_0:.temp)
                                    +. 32971/8500000 *. :var_0:.rh)
                                   +. -21603/320000 *. :var_0:.rain)))
                        +. -38230826571333/10000000000000
                           *. (if (((((66419/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. 25399/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 449/29020000 *. :var_0:.dmc)
                                     +. 3841/3110000 *. :var_0:.temp)
                                    +. -25741/4250000 *. :var_0:.rh)
                                   +. 58299/640000 *. :var_0:.rain)
                                  <=. -317131778543/1534287400000
                               then 0
                               else
                                 ((((((317131778543/1534287400000
                                       +. 66419/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. 25399/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 449/29020000 *. :var_0:.dmc)
                                    +. 3841/3110000 *. :var_0:.temp)
                                   +. -25741/4250000 *. :var_0:.rh)
                                  +. 58299/640000 *. :var_0:.rain)))
                       +. -33840866455803/62500000000000
                          *. (if (((((23799/100000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -18071/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 38981/29020000 *. :var_0:.dmc)
                                    +. 1727/194375 *. :var_0:.temp)
                                   +. -61231/8500000 *. :var_0:.rh)
                                  +. -1831/320000 *. :var_0:.rain)
                                 <=. -89188713933/1534287400000
                              then 0
                              else
                                ((((((89188713933/1534287400000
                                      +. 23799/100000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -18071/95050
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 38981/29020000 *. :var_0:.dmc)
                                   +. 1727/194375 *. :var_0:.temp)
                                  +. -61231/8500000 *. :var_0:.rh)
                                 +. -1831/320000 *. :var_0:.rain)))
                      +. -824339075780979/250000000000000
                         *. (if (((((10277/200000
                                     *. (if :var_0:.month = Jan then 67/500
                                         else
                                         if :var_0:.month = Feb then 1/2
                                         else
                                         if :var_0:.month = Mar then 1
                                         else if :var_0:.month = Apr then 3/2 else …)
                                     +. -28841/190100
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 4637/29020000 *. :var_0:.dmc)
                                   +. 3601/388750 *. :var_0:.temp)
                                  +. 5957/8500000 *. :var_0:.rh)
                                 +. -22041/640000 *. :var_0:.rain)
                                <=. -372238333/2454859840
                             then 0
                             else
                               ((((((372238333/2454859840
                                     +. 10277/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …))
                                    +. -28841/190100
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 4637/29020000 *. :var_0:.dmc)
                                  +. 3601/388750 *. :var_0:.temp)
                                 +. 5957/8500000 *. :var_0:.rh)
                                +. -22041/640000 *. :var_0:.rain)))
                     +. 229289525512443/50000000000000
                        *. (if (((((13901/50000
                                    *. (if :var_0:.month = Jan then 67/500
                                        else
                                        if :var_0:.month = Feb then 1/2
                                        else
                                        if :var_0:.month = Mar then 1
                                        else if :var_0:.month = Apr then 3/2 else …)
                                    +. -803/38020
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 10557/29020000 *. :var_0:.dmc)
                                  +. 60757/3110000 *. :var_0:.temp)
                                 +. -16157/4250000 *. :var_0:.rh)
                                +. 47933/640000 *. :var_0:.rain)
                               <=. 72146699557/306857480000
                            then 0
                            else
                              ((((((-72146699557/306857480000
                                    +. 13901/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …))
                                   +. -803/38020
                                      *. (if :var_0:.day = Mon then 377/1000
                                          else
                                          if :var_0:.day = Tue then 1223/1000
                                          else
                                          if :var_0:.day = Wed then 1901/1000
                                          else if :var_0:.day = Thu then 1901/1000 else …))
                                  +. 10557/29020000 *. :var_0:.dmc)
                                 +. 60757/3110000 *. :var_0:.temp)
                                +. -16157/4250000 *. :var_0:.rh)
                               +. 47933/640000 *. :var_0:.rain))
                   else
                   if (((((1568904513/1250000000
                           *. (if (((((5031/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -7861/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -19063/29020000 *. :var_0:.dmc)
                                     +. -27281/1555000 *. :var_0:.temp)
                                    +. 137/340000 *. :var_0:.rh)
                                   +. 6263/80000 *. :var_0:.rain)
                                  <=. -1716983137/306857480000
                               then 0
                               else
                                 ((((((1716983137/306857480000
                                       +. 5031/50000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -7861/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. -19063/29020000 *. :var_0:.dmc)
                                    +. -27281/1555000 *. :var_0:.temp)
                                   +. 137/340000 *. :var_0:.rh)
                                  +. 6263/80000 *. :var_0:.rain))
                           +. -1400061773/1250000000
                              *. (if (((((29103/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …)
                                          +. 159/9505
                                             *. (if :var_0:.day = Mon then 377/1000
                                                 else
                                                 if :var_0:.day = Tue then 1223/1000
                                                 else
                                                 if :var_0:.day = Wed then 1901/1000
                                                 else
                                                 if :var_0:.day = Thu then 1901/1000 else …))
                                         +. -1021/1813750 *. :var_0:.dmc)
                                        +. 17919/3110000 *. :var_0:.temp)
                                       +. 32971/8500000 *. :var_0:.rh)
                                      +. -21603/320000 *. :var_0:.rain)
                                     <=. 73983893263/767143700000
                                  then 0
                                  else
                                    ((((((-73983893263/767143700000
                                          +. 29103/200000
                                             *. (if :var_0:.month = Jan then 67/500
                                                 else
                                                 if :var_0:.month = Feb then 1/2
                                                 else
                                                 if :var_0:.month = Mar then 1
                                                 else
                                                 if :var_0:.month = Apr then 3/2 else …))
                                         +. 159/9505
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -1021/1813750 *. :var_0:.dmc)
                                       +. 17919/3110000 *. :var_0:.temp)
                                      +. 32971/8500000 *. :var_0:.rh)
                                     +. -21603/320000 *. :var_0:.rain)))
                          +. -889978969/400000000
                             *. (if (((((66419/200000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. 25399/190100
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. 449/29020000 *. :var_0:.dmc)
                                       +. 3841/3110000 *. :var_0:.temp)
                                      +. -25741/4250000 *. :var_0:.rh)
                                     +. 58299/640000 *. :var_0:.rain)
                                    <=. -317131778543/1534287400000
                                 then 0
                                 else
                                   ((((((317131778543/1534287400000
                                         +. 66419/200000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. 25399/190100
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 449/29020000 *. :var_0:.dmc)
                                      +. 3841/3110000 *. :var_0:.temp)
                                     +. -25741/4250000 *. :var_0:.rh)
                                    +. 58299/640000 *. :var_0:.rain)))
                         +. -787784679/2500000000
                            *. (if (((((23799/100000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. -18071/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 38981/29020000 *. :var_0:.dmc)
                                      +. 1727/194375 *. :var_0:.temp)
                                     +. -61231/8500000 *. :var_0:.rh)
                                    +. -1831/320000 *. :var_0:.rain)
                                   <=. -89188713933/1534287400000
                                then 0
                                else
                                  ((((((89188713933/1534287400000
                                        +. 23799/100000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. -18071/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 38981/29020000 *. :var_0:.dmc)
                                     +. 1727/194375 *. :var_0:.temp)
                                    +. -61231/8500000 *. :var_0:.rh)
                                   +. -1831/320000 *. :var_0:.rain)))
                        +. -19189866047/10000000000
                           *. (if (((((10277/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -28841/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 4637/29020000 *. :var_0:.dmc)
                                     +. 3601/388750 *. :var_0:.temp)
                                    +. 5957/8500000 *. :var_0:.rh)
                                   +. -22041/640000 *. :var_0:.rain)
                                  <=. -372238333/2454859840
                               then 0
                               else
                                 ((((((372238333/2454859840
                                       +. 10277/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -28841/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 4637/29020000 *. :var_0:.dmc)
                                    +. 3601/388750 *. :var_0:.temp)
                                   +. 5957/8500000 *. :var_0:.rh)
                                  +. -22041/640000 *. :var_0:.rain)))
                       +. 5337652199/2000000000
                          *. (if (((((13901/50000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -803/38020
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 10557/29020000 *. :var_0:.dmc)
                                    +. 60757/3110000 *. :var_0:.temp)
                                   +. -16157/4250000 *. :var_0:.rh)
                                  +. 47933/640000 *. :var_0:.rain)
                                 <=. 72146699557/306857480000
                              then 0
                              else
                                ((((((-72146699557/306857480000
                                      +. 13901/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -803/38020
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 10557/29020000 *. :var_0:.dmc)
                                   +. 60757/3110000 *. :var_0:.temp)
                                  +. -16157/4250000 *. :var_0:.rh)
                                 +. 47933/640000 *. :var_0:.rain)))
                      <=. -29487779/312500000
                   then
                     (((((213430965464483/31250000000000
                          +. 732799213218501/125000000000000
                             *. (if (((((5031/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. -7861/95050
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -19063/29020000 *. :var_0:.dmc)
                                       +. -27281/1555000 *. :var_0:.temp)
                                      +. 137/340000 *. :var_0:.rh)
                                     +. 6263/80000 *. :var_0:.rain)
                                    <=. -1716983137/306857480000
                                 then 0
                                 else
                                   ((((((1716983137/306857480000
                                         +. 5031/50000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. -7861/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -19063/29020000 *. :var_0:.dmc)
                                      +. -27281/1555000 *. :var_0:.temp)
                                     +. 137/340000 *. :var_0:.rh)
                                    +. 6263/80000 *. :var_0:.rain)))
                         +. -653936652747521/125000000000000
                            *. (if (((((29103/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. 159/9505
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -1021/1813750 *. :var_0:.dmc)
                                      +. 17919/3110000 *. :var_0:.temp)
                                     +. 32971/8500000 *. :var_0:.rh)
                                    +. -21603/320000 *. :var_0:.rain)
                                   <=. 73983893263/767143700000
                                then 0
                                else
                                  ((((((-73983893263/767143700000
                                        +. 29103/200000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. 159/9505
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -1021/1813750 *. :var_0:.dmc)
                                     +. 17919/3110000 *. :var_0:.temp)
                                    +. 32971/8500000 *. :var_0:.rh)
                                   +. -21603/320000 *. :var_0:.rain)))
                        +. -415688706903613/40000000000000
                           *. (if (((((66419/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. 25399/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 449/29020000 *. :var_0:.dmc)
                                     +. 3841/3110000 *. :var_0:.temp)
                                    +. -25741/4250000 *. :var_0:.rh)
                                   +. 58299/640000 *. :var_0:.rain)
                                  <=. -317131778543/1534287400000
                               then 0
                               else
                                 ((((((317131778543/1534287400000
                                       +. 66419/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. 25399/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 449/29020000 *. :var_0:.dmc)
                                    +. 3841/3110000 *. :var_0:.temp)
                                   +. -25741/4250000 *. :var_0:.rh)
                                  +. 58299/640000 *. :var_0:.rain)))
                       +. -367956104513283/250000000000000
                          *. (if (((((23799/100000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -18071/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 38981/29020000 *. :var_0:.dmc)
                                    +. 1727/194375 *. :var_0:.temp)
                                   +. -61231/8500000 *. :var_0:.rh)
                                  +. -1831/320000 *. :var_0:.rain)
                                 <=. -89188713933/1534287400000
                              then 0
                              else
                                ((((((89188713933/1534287400000
                                      +. 23799/100000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -18071/95050
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 38981/29020000 *. :var_0:.dmc)
                                   +. 1727/194375 *. :var_0:.temp)
                                  +. -61231/8500000 *. :var_0:.rh)
                                 +. -1831/320000 *. :var_0:.rain)))
                      +. -8963145063634619/1000000000000000
                         *. (if (((((10277/200000
                                     *. (if :var_0:.month = Jan then 67/500
                                         else
                                         if :var_0:.month = Feb then 1/2
                                         else
                                         if :var_0:.month = Mar then 1
                                         else if :var_0:.month = Apr then 3/2 else …)
                                     +. -28841/190100
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 4637/29020000 *. :var_0:.dmc)
                                   +. 3601/388750 *. :var_0:.temp)
                                  +. 5957/8500000 *. :var_0:.rh)
                                 +. -22041/640000 *. :var_0:.rain)
                                <=. -372238333/2454859840
                             then 0
                             else
                               ((((((372238333/2454859840
                                     +. 10277/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …))
                                    +. -28841/190100
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 4637/29020000 *. :var_0:.dmc)
                                  +. 3601/388750 *. :var_0:.temp)
                                 +. 5957/8500000 *. :var_0:.rh)
                                +. -22041/640000 *. :var_0:.rain)))
                     +. 2493094576152323/200000000000000
                        *. (if (((((13901/50000
                                    *. (if :var_0:.month = Jan then 67/500
                                        else
                                        if :var_0:.month = Feb then 1/2
                                        else
                                        if :var_0:.month = Mar then 1
                                        else if :var_0:.month = Apr then 3/2 else …)
                                    +. -803/38020
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 10557/29020000 *. :var_0:.dmc)
                                  +. 60757/3110000 *. :var_0:.temp)
                                 +. -16157/4250000 *. :var_0:.rh)
                                +. 47933/640000 *. :var_0:.rain)
                               <=. 72146699557/306857480000
                            then 0
                            else
                              ((((((-72146699557/306857480000
                                    +. 13901/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …))
                                   +. -803/38020
                                      *. (if :var_0:.day = Mon then 377/1000
                                          else
                                          if :var_0:.day = Tue then 1223/1000
                                          else
                                          if :var_0:.day = Wed then 1901/1000
                                          else if :var_0:.day = Thu then 1901/1000 else …))
                                  +. 10557/29020000 *. :var_0:.dmc)
                                 +. 60757/3110000 *. :var_0:.temp)
                                +. -16157/4250000 *. :var_0:.rh)
                               +. 47933/640000 *. :var_0:.rain))
                   else
                   if (((((1568904513/1250000000
                           *. (if (((((5031/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -7861/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -19063/29020000 *. :var_0:.dmc)
                                     +. -27281/1555000 *. :var_0:.temp)
                                    +. 137/340000 *. :var_0:.rh)
                                   +. 6263/80000 *. :var_0:.rain)
                                  <=. -1716983137/306857480000
                               then 0
                               else
                                 ((((((1716983137/306857480000
                                       +. 5031/50000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -7861/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. -19063/29020000 *. :var_0:.dmc)
                                    +. -27281/1555000 *. :var_0:.temp)
                                   +. 137/340000 *. :var_0:.rh)
                                  +. 6263/80000 *. :var_0:.rain))
                           +. -1400061773/1250000000
                              *. (if (((((29103/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …)
                                          +. 159/9505
                                             *. (if :var_0:.day = Mon then 377/1000
                                                 else
                                                 if :var_0:.day = Tue then 1223/1000
                                                 else
                                                 if :var_0:.day = Wed then 1901/1000
                                                 else
                                                 if :var_0:.day = Thu then 1901/1000 else …))
                                         +. -1021/1813750 *. :var_0:.dmc)
                                        +. 17919/3110000 *. :var_0:.temp)
                                       +. 32971/8500000 *. :var_0:.rh)
                                      +. -21603/320000 *. :var_0:.rain)
                                     <=. 73983893263/767143700000
                                  then 0
                                  else
                                    ((((((-73983893263/767143700000
                                          +. 29103/200000
                                             *. (if :var_0:.month = Jan then 67/500
                                                 else
                                                 if :var_0:.month = Feb then 1/2
                                                 else
                                                 if :var_0:.month = Mar then 1
                                                 else
                                                 if :var_0:.month = Apr then 3/2 else …))
                                         +. 159/9505
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -1021/1813750 *. :var_0:.dmc)
                                       +. 17919/3110000 *. :var_0:.temp)
                                      +. 32971/8500000 *. :var_0:.rh)
                                     +. -21603/320000 *. :var_0:.rain)))
                          +. -889978969/400000000
                             *. (if (((((66419/200000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. 25399/190100
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. 449/29020000 *. :var_0:.dmc)
                                       +. 3841/3110000 *. :var_0:.temp)
                                      +. -25741/4250000 *. :var_0:.rh)
                                     +. 58299/640000 *. :var_0:.rain)
                                    <=. -317131778543/1534287400000
                                 then 0
                                 else
                                   ((((((317131778543/1534287400000
                                         +. 66419/200000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. 25399/190100
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 449/29020000 *. :var_0:.dmc)
                                      +. 3841/3110000 *. :var_0:.temp)
                                     +. -25741/4250000 *. :var_0:.rh)
                                    +. 58299/640000 *. :var_0:.rain)))
                         +. -787784679/2500000000
                            *. (if (((((23799/100000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. -18071/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 38981/29020000 *. :var_0:.dmc)
                                      +. 1727/194375 *. :var_0:.temp)
                                     +. -61231/8500000 *. :var_0:.rh)
                                    +. -1831/320000 *. :var_0:.rain)
                                   <=. -89188713933/1534287400000
                                then 0
                                else
                                  ((((((89188713933/1534287400000
                                        +. 23799/100000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. -18071/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 38981/29020000 *. :var_0:.dmc)
                                     +. 1727/194375 *. :var_0:.temp)
                                    +. -61231/8500000 *. :var_0:.rh)
                                   +. -1831/320000 *. :var_0:.rain)))
                        +. -19189866047/10000000000
                           *. (if (((((10277/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -28841/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 4637/29020000 *. :var_0:.dmc)
                                     +. 3601/388750 *. :var_0:.temp)
                                    +. 5957/8500000 *. :var_0:.rh)
                                   +. -22041/640000 *. :var_0:.rain)
                                  <=. -372238333/2454859840
                               then 0
                               else
                                 ((((((372238333/2454859840
                                       +. 10277/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -28841/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 4637/29020000 *. :var_0:.dmc)
                                    +. 3601/388750 *. :var_0:.temp)
                                   +. 5957/8500000 *. :var_0:.rh)
                                  +. -22041/640000 *. :var_0:.rain)))
                       +. 5337652199/2000000000
                          *. (if (((((13901/50000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -803/38020
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 10557/29020000 *. :var_0:.dmc)
                                    +. 60757/3110000 *. :var_0:.temp)
                                   +. -16157/4250000 *. :var_0:.rh)
                                  +. 47933/640000 *. :var_0:.rain)
                                 <=. 72146699557/306857480000
                              then 0
                              else
                                ((((((-72146699557/306857480000
                                      +. 13901/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -803/38020
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 10557/29020000 *. :var_0:.dmc)
                                   +. 60757/3110000 *. :var_0:.temp)
                                  +. -16157/4250000 *. :var_0:.rh)
                                 +. 47933/640000 *. :var_0:.rain)))
                      <=. 283012221/312500000
                   then
                     (((((1852306369389/244140625000
                          +. 124497279820089/7812500000000
                             *. (if (((((5031/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. -7861/95050
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -19063/29020000 *. :var_0:.dmc)
                                       +. -27281/1555000 *. :var_0:.temp)
                                      +. 137/340000 *. :var_0:.rh)
                                     +. 6263/80000 *. :var_0:.rain)
                                    <=. -1716983137/306857480000
                                 then 0
                                 else
                                   ((((((1716983137/306857480000
                                         +. 5031/50000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. -7861/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -19063/29020000 *. :var_0:.dmc)
                                      +. -27281/1555000 *. :var_0:.temp)
                                     +. 137/340000 *. :var_0:.rh)
                                    +. 6263/80000 *. :var_0:.rain)))
                         +. -111099101872869/7812500000000
                            *. (if (((((29103/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. 159/9505
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. -1021/1813750 *. :var_0:.dmc)
                                      +. 17919/3110000 *. :var_0:.temp)
                                     +. 32971/8500000 *. :var_0:.rh)
                                    +. -21603/320000 *. :var_0:.rain)
                                   <=. 73983893263/767143700000
                                then 0
                                else
                                  ((((((-73983893263/767143700000
                                        +. 29103/200000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. 159/9505
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -1021/1813750 *. :var_0:.dmc)
                                     +. 17919/3110000 *. :var_0:.temp)
                                    +. 32971/8500000 *. :var_0:.rh)
                                   +. -21603/320000 *. :var_0:.rain)))
                        +. -70622501127057/2500000000000
                           *. (if (((((66419/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. 25399/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 449/29020000 *. :var_0:.dmc)
                                     +. 3841/3110000 *. :var_0:.temp)
                                    +. -25741/4250000 *. :var_0:.rh)
                                   +. 58299/640000 *. :var_0:.rain)
                                  <=. -317131778543/1534287400000
                               then 0
                               else
                                 ((((((317131778543/1534287400000
                                       +. 66419/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. 25399/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 449/29020000 *. :var_0:.dmc)
                                    +. 3841/3110000 *. :var_0:.temp)
                                   +. -25741/4250000 *. :var_0:.rh)
                                  +. 58299/640000 *. :var_0:.rain)))
                       +. -62513077632687/15625000000000
                          *. (if (((((23799/100000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -18071/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 38981/29020000 *. :var_0:.dmc)
                                    +. 1727/194375 *. :var_0:.temp)
                                   +. -61231/8500000 *. :var_0:.rh)
                                  +. -1831/320000 *. :var_0:.rain)
                                 <=. -89188713933/1534287400000
                              then 0
                              else
                                ((((((89188713933/1534287400000
                                      +. 23799/100000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -18071/95050
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 38981/29020000 *. :var_0:.dmc)
                                   +. 1727/194375 *. :var_0:.temp)
                                  +. -61231/8500000 *. :var_0:.rh)
                                 +. -1831/320000 *. :var_0:.rain)))
                      +. -1522773440427591/62500000000000
                         *. (if (((((10277/200000
                                     *. (if :var_0:.month = Jan then 67/500
                                         else
                                         if :var_0:.month = Feb then 1/2
                                         else
                                         if :var_0:.month = Mar then 1
                                         else if :var_0:.month = Apr then 3/2 else …)
                                     +. -28841/190100
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 4637/29020000 *. :var_0:.dmc)
                                   +. 3601/388750 *. :var_0:.temp)
                                  +. 5957/8500000 *. :var_0:.rh)
                                 +. -22041/640000 *. :var_0:.rain)
                                <=. -372238333/2454859840
                             then 0
                             else
                               ((((((372238333/2454859840
                                     +. 10277/200000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …))
                                    +. -28841/190100
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 4637/29020000 *. :var_0:.dmc)
                                  +. 3601/388750 *. :var_0:.temp)
                                 +. 5957/8500000 *. :var_0:.rh)
                                +. -22041/640000 *. :var_0:.rain)))
                     +. 423558714947247/12500000000000
                        *. (if (((((13901/50000
                                    *. (if :var_0:.month = Jan then 67/500
                                        else
                                        if :var_0:.month = Feb then 1/2
                                        else
                                        if :var_0:.month = Mar then 1
                                        else if :var_0:.month = Apr then 3/2 else …)
                                    +. -803/38020
                                       *. (if :var_0:.day = Mon then 377/1000
                                           else
                                           if :var_0:.day = Tue then 1223/1000
                                           else
                                           if :var_0:.day = Wed then 1901/1000
                                           else if :var_0:.day = Thu then 1901/1000 else …))
                                   +. 10557/29020000 *. :var_0:.dmc)
                                  +. 60757/3110000 *. :var_0:.temp)
                                 +. -16157/4250000 *. :var_0:.rh)
                                +. 47933/640000 *. :var_0:.rain)
                               <=. 72146699557/306857480000
                            then 0
                            else
                              ((((((-72146699557/306857480000
                                    +. 13901/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …))
                                   +. -803/38020
                                      *. (if :var_0:.day = Mon then 377/1000
                                          else
                                          if :var_0:.day = Tue then 1223/1000
                                          else
                                          if :var_0:.day = Wed then 1901/1000
                                          else if :var_0:.day = Thu then 1901/1000 else …))
                                  +. 10557/29020000 *. :var_0:.dmc)
                                 +. 60757/3110000 *. :var_0:.temp)
                                +. -16157/4250000 *. :var_0:.rh)
                               +. 47933/640000 *. :var_0:.rain))
                   else
                   if (((((1568904513/1250000000
                           *. (if (((((5031/50000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -7861/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. -19063/29020000 *. :var_0:.dmc)
                                     +. -27281/1555000 *. :var_0:.temp)
                                    +. 137/340000 *. :var_0:.rh)
                                   +. 6263/80000 *. :var_0:.rain)
                                  <=. -1716983137/306857480000
                               then 0
                               else
                                 ((((((1716983137/306857480000
                                       +. 5031/50000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -7861/95050
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. -19063/29020000 *. :var_0:.dmc)
                                    +. -27281/1555000 *. :var_0:.temp)
                                   +. 137/340000 *. :var_0:.rh)
                                  +. 6263/80000 *. :var_0:.rain))
                           +. -1400061773/1250000000
                              *. (if (((((29103/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …)
                                          +. 159/9505
                                             *. (if :var_0:.day = Mon then 377/1000
                                                 else
                                                 if :var_0:.day = Tue then 1223/1000
                                                 else
                                                 if :var_0:.day = Wed then 1901/1000
                                                 else
                                                 if :var_0:.day = Thu then 1901/1000 else …))
                                         +. -1021/1813750 *. :var_0:.dmc)
                                        +. 17919/3110000 *. :var_0:.temp)
                                       +. 32971/8500000 *. :var_0:.rh)
                                      +. -21603/320000 *. :var_0:.rain)
                                     <=. 73983893263/767143700000
                                  then 0
                                  else
                                    ((((((-73983893263/767143700000
                                          +. 29103/200000
                                             *. (if :var_0:.month = Jan then 67/500
                                                 else
                                                 if :var_0:.month = Feb then 1/2
                                                 else
                                                 if :var_0:.month = Mar then 1
                                                 else
                                                 if :var_0:.month = Apr then 3/2 else …))
                                         +. 159/9505
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. -1021/1813750 *. :var_0:.dmc)
                                       +. 17919/3110000 *. :var_0:.temp)
                                      +. 32971/8500000 *. :var_0:.rh)
                                     +. -21603/320000 *. :var_0:.rain)))
                          +. -889978969/400000000
                             *. (if (((((66419/200000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …)
                                         +. 25399/190100
                                            *. (if :var_0:.day = Mon then 377/1000
                                                else
                                                if :var_0:.day = Tue then 1223/1000
                                                else
                                                if :var_0:.day = Wed then 1901/1000
                                                else
                                                if :var_0:.day = Thu then 1901/1000 else …))
                                        +. 449/29020000 *. :var_0:.dmc)
                                       +. 3841/3110000 *. :var_0:.temp)
                                      +. -25741/4250000 *. :var_0:.rh)
                                     +. 58299/640000 *. :var_0:.rain)
                                    <=. -317131778543/1534287400000
                                 then 0
                                 else
                                   ((((((317131778543/1534287400000
                                         +. 66419/200000
                                            *. (if :var_0:.month = Jan then 67/500
                                                else
                                                if :var_0:.month = Feb then 1/2
                                                else
                                                if :var_0:.month = Mar then 1
                                                else if :var_0:.month = Apr then 3/2 else …))
                                        +. 25399/190100
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 449/29020000 *. :var_0:.dmc)
                                      +. 3841/3110000 *. :var_0:.temp)
                                     +. -25741/4250000 *. :var_0:.rh)
                                    +. 58299/640000 *. :var_0:.rain)))
                         +. -787784679/2500000000
                            *. (if (((((23799/100000
                                        *. (if :var_0:.month = Jan then 67/500
                                            else
                                            if :var_0:.month = Feb then 1/2
                                            else
                                            if :var_0:.month = Mar then 1
                                            else if :var_0:.month = Apr then 3/2 else …)
                                        +. -18071/95050
                                           *. (if :var_0:.day = Mon then 377/1000
                                               else
                                               if :var_0:.day = Tue then 1223/1000
                                               else
                                               if :var_0:.day = Wed then 1901/1000
                                               else
                                               if :var_0:.day = Thu then 1901/1000 else …))
                                       +. 38981/29020000 *. :var_0:.dmc)
                                      +. 1727/194375 *. :var_0:.temp)
                                     +. -61231/8500000 *. :var_0:.rh)
                                    +. -1831/320000 *. :var_0:.rain)
                                   <=. -89188713933/1534287400000
                                then 0
                                else
                                  ((((((89188713933/1534287400000
                                        +. 23799/100000
                                           *. (if :var_0:.month = Jan then 67/500
                                               else
                                               if :var_0:.month = Feb then 1/2
                                               else
                                               if :var_0:.month = Mar then 1
                                               else if :var_0:.month = Apr then 3/2 else …))
                                       +. -18071/95050
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 38981/29020000 *. :var_0:.dmc)
                                     +. 1727/194375 *. :var_0:.temp)
                                    +. -61231/8500000 *. :var_0:.rh)
                                   +. -1831/320000 *. :var_0:.rain)))
                        +. -19189866047/10000000000
                           *. (if (((((10277/200000
                                       *. (if :var_0:.month = Jan then 67/500
                                           else
                                           if :var_0:.month = Feb then 1/2
                                           else
                                           if :var_0:.month = Mar then 1
                                           else if :var_0:.month = Apr then 3/2 else …)
                                       +. -28841/190100
                                          *. (if :var_0:.day = Mon then 377/1000
                                              else
                                              if :var_0:.day = Tue then 1223/1000
                                              else
                                              if :var_0:.day = Wed then 1901/1000
                                              else
                                              if :var_0:.day = Thu then 1901/1000 else …))
                                      +. 4637/29020000 *. :var_0:.dmc)
                                     +. 3601/388750 *. :var_0:.temp)
                                    +. 5957/8500000 *. :var_0:.rh)
                                   +. -22041/640000 *. :var_0:.rain)
                                  <=. -372238333/2454859840
                               then 0
                               else
                                 ((((((372238333/2454859840
                                       +. 10277/200000
                                          *. (if :var_0:.month = Jan then 67/500
                                              else
                                              if :var_0:.month = Feb then 1/2
                                              else
                                              if :var_0:.month = Mar then 1
                                              else if :var_0:.month = Apr then 3/2 else …))
                                      +. -28841/190100
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 4637/29020000 *. :var_0:.dmc)
                                    +. 3601/388750 *. :var_0:.temp)
                                   +. 5957/8500000 *. :var_0:.rh)
                                  +. -22041/640000 *. :var_0:.rain)))
                       +. 5337652199/2000000000
                          *. (if (((((13901/50000
                                      *. (if :var_0:.month = Jan then 67/500
                                          else
                                          if :var_0:.month = Feb then 1/2
                                          else
                                          if :var_0:.month = Mar then 1
                                          else if :var_0:.month = Apr then 3/2 else …)
                                      +. -803/38020
                                         *. (if :var_0:.day = Mon then 377/1000
                                             else
                                             if :var_0:.day = Tue then 1223/1000
                                             else
                                             if :var_0:.day = Wed then 1901/1000
                                             else
                                             if :var_0:.day = Thu then 1901/1000 else …))
                                     +. 10557/29020000 *. :var_0:.dmc)
                                    +. 60757/3110000 *. :var_0:.temp)
                                   +. -16157/4250000 *. :var_0:.rh)
                                  +. 47933/640000 *. :var_0:.rain)
                                 <=. 72146699557/306857480000
                              then 0
                              else
                                ((((((-72146699557/306857480000
                                      +. 13901/50000
                                         *. (if :var_0:.month = Jan then 67/500
                                             else
                                             if :var_0:.month = Feb then 1/2
                                             else
                                             if :var_0:.month = Mar then 1
                                             else if :var_0:.month = Apr then 3/2 else …))
                                     +. -803/38020
                                        *. (if :var_0:.day = Mon then 377/1000
                                            else
                                            if :var_0:.day = Tue then 1223/1000
                                            else
                                            if :var_0:.day = Wed then 1901/1000
                                            else if :var_0:.day = Thu then 1901/1000 else …))
                                    +. 10557/29020000 *. :var_0:.dmc)
                                   +. 60757/3110000 *. :var_0:.temp)
                                  +. -16157/4250000 *. :var_0:.rh)
                                 +. 47933/640000 *. :var_0:.rain)))
                      <=. 595512221/312500000
                   then … else …)
                  <=. 20)
                 && :var_0:.temp = 20)
                && :var_0:.month = May
                expansions
                []
                rewrite_steps
                  forward_chaining
                  • Sat (Some let (x : nn_input) = {month = May; day = Wed; dmc = (Real.mk_of_string "7597491365091646983788244502461274105063710103/1285912235995896196222304684839556138615000"); temp = 20.0; rh = (Real.mk_of_string "116321417146729453300761696944820485610293761/51436489439835847848892187393582245544600"); rain = (Real.mk_of_string "2495451056678694134139316951586229474021508/32147805899897404905557617120988903465375")} )
                  In [19]:
                  CX.x
                  
                  Out[19]:
                  - : nn_input =
                  {month = May; day = Wed; dmc = 5908.25030855; temp = 20.; rh = 2261.45715646;
                   rain = 77.6243039556}
                  

                  Notice how the unspecified input variables are unbounded, just as in our original classification instances. Using the description of each variable in the data (plus some reasonable assumptions about Portugal's climate) we can form the following condition describing valid inputs to the network.

                  In [20]:
                  let is_valid_nn input =
                    0.0 <=. input.dmc && input.dmc <=. 500.0 &&
                    0.0 <=. input.temp && input.temp <=. 40.0 &&
                    0.0 <=. input.rh && input.rh <=. 100.0 &&
                    0.0 <=. input.rain && input.rain <=. 15.0
                  
                  instance (fun x -> nn_model x >. 20.0 && x.temp = 20.0 && x.month = May && is_valid_nn x)
                  
                  Out[20]:
                  val is_valid_nn : nn_input -> bool = <fun>
                  - : nn_input -> bool = <fun>
                  module CX : sig val x : nn_input end
                  
                  Instance (after 0 steps, 0.340s):
                   let (x : nn_input) =
                     {month = May; day = Mon; dmc = 0.0; temp = 20.0;
                      rh =
                       (Real.mk_of_string "10119821984260014680837698839718225142002486937570488900385690895602012656396301/136842728928994700407353274130606160961592990641058626263785617248877730000000");
                      rain =
                       (Real.mk_of_string "2572767638112562557199585747693715072784663131197540851576234534890872782596547/213816763951554219386489490829072126502489047876654103537165026951371453125000")}
                  
                  Instance