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 : Format.formatter -> real -> 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 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = 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 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = 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 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = 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 -> real -> real -> real -> real -> real -> real -> real * real = <fun>
val tree_1 :
  real -> real -> real -> real -> real -> real -> real -> real * real = <fun>
val tree_2 :
  real -> real -> real -> real -> real -> real -> real -> real * real = <fun>
val rf : real * real * real * real * real * 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.134s):
 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.134s
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 allocs1052396991
final checks1
added eqs93
del clause1
arith eq adapter6
memory23.110000
max memory26.950000
Expand
  • start[0.134s]
      (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.036s):
       let (x : rf_input) =
         {radius_mean = (Real.mk_of_string "28061993138323/5000000000000");
          compactness_mean = (Real.mk_of_string "8487976201/5000000000000");
          concavity_mean = (Real.mk_of_string "162320931909/2500000000000");
          radius_se = (Real.mk_of_string "40971/20000");
          compactness_worst = (Real.mk_of_string "321/5000");
          concavity_worst = (Real.mk_of_string "415811319441/25000000000000");
          concave_points_worst = (Real.mk_of_string "3877904791/781250000000")}
      
      Instance
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.036s
      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 allocs1248283383
      final checks1
      added eqs93
      del clause1
      arith eq adapter6
      memory11.430000
      max memory26.950000
      Expand
      • start[0.036s]
          (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 "28061993138323/5000000000000"); compactness_mean = (Real.mk_of_string "8487976201/5000000000000"); concavity_mean = (Real.mk_of_string "162320931909/2500000000000"); radius_se = (Real.mk_of_string "40971/20000"); compactness_worst = (Real.mk_of_string "321/5000"); concavity_worst = (Real.mk_of_string "415811319441/25000000000000"); concave_points_worst = (Real.mk_of_string "3877904791/781250000000")} )
          In [9]:
          CX.x
          
          Out[9]:
          - : rf_input =
          {radius_mean = 5.61239862766; compactness_mean = 0.0016975952402;
           concavity_mean = 0.0649283727636; radius_se = 2.04855;
           compactness_worst = 0.0642; concavity_worst = 0.0166324527776;
           concave_points_worst = 0.00496371813248}
          

          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.038s
          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 allocs1326607074
          added eqs99
          del clause36
          arith eq adapter8
          memory13.710000
          max memory26.950000
          Expand
          • start[0.038s]
              (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_56 x_86) (/ 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]:
              Modular_decomp.top ~assuming:"is_valid_rf" "rf_model"
              
              Out[11]:
              - : Top_result.modular_decomposition =
              {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
               md_f =
                {Imandra_surface.Uid.name = "rf_model"; id = <abstr>;
                 special_tag = <abstr>; namespace = <abstr>;
                 chash = Some OdDjCbSrRn0cKge4O2CXI4yUH5xJkTvG8tDCwV3WegI;
                 depth = (5i, 2i)};
               md_args = [(input : rf_input)]; md_regions = <abstr>}
              
              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
              decomp of (rf_model input
              Reg_idConstraintsInvariant
              1023
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000)
              • ((7 +. 110) +. 4) >. ((5 +. 3) +. 21)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1022
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000
              • ((7 +. 110) +. 3) >. ((5 +. 3) +. 122)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1021
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000)
              • ((7 +. 110) +. 1) >. ((5 +. 3) +. 4)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1020
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000
              • ((7 +. 110) +. 28) >. ((5 +. 3) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1019
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                 -7927/100000)
              • ((7 +. 110) +. 25) >. ((5 +. 3) +. 17)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1018
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                -7927/100000
              • ((7 +. 110) +. 38) >. ((5 +. 3) +. 2)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1017
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000)
              • ((7 +. 110) +. 44) >. ((5 +. 3) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1016
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000
              • ((7 +. 110) +. 139) >. ((5 +. 3) +. 1)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • ((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1015
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000)
              • ((7 +. 137) +. 4) >. ((5 +. 0) +. 21)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1014
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000
              • ((7 +. 137) +. 3) >. ((5 +. 0) +. 122)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1013
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000)
              • ((7 +. 137) +. 1) >. ((5 +. 0) +. 4)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1012
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000
              • ((7 +. 137) +. 28) >. ((5 +. 0) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1011
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                 -7927/100000)
              • ((7 +. 137) +. 25) >. ((5 +. 0) +. 17)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1010
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                -7927/100000
              • ((7 +. 137) +. 38) >. ((5 +. 0) +. 2)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1009
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000)
              • ((7 +. 137) +. 44) >. ((5 +. 0) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1008
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000
              • ((7 +. 137) +. 139) >. ((5 +. 0) +. 1)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000
              • not (((input.compactness_mean -. 5217/50000) /. 5281/100000) <=. -4159/5000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1007
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000)
              • ((7 +. 1) +. 4) >. ((5 +. 8) +. 21)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1006
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000
              • ((7 +. 1) +. 3) >. ((5 +. 8) +. 122)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1005
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000)
              • ((7 +. 1) +. 1) >. ((5 +. 8) +. 4)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1004
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000
              • ((7 +. 1) +. 28) >. ((5 +. 8) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1003
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                 -7927/100000)
              • ((7 +. 1) +. 25) >. ((5 +. 8) +. 17)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1002
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                -7927/100000
              • ((7 +. 1) +. 38) >. ((5 +. 8) +. 2)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1001
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000)
              • ((7 +. 1) +. 44) >. ((5 +. 8) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              1000
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000
              • ((7 +. 1) +. 139) >. ((5 +. 8) +. 1)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              999
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000)
              • ((7 +. 0) +. 4) >. ((5 +. 7) +. 21)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              998
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000
              • ((7 +. 0) +. 3) >. ((5 +. 7) +. 122)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              997
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000)
              • ((7 +. 0) +. 1) >. ((5 +. 7) +. 4)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              996
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000
              • ((7 +. 0) +. 28) >. ((5 +. 7) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              995
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                 -7927/100000)
              • ((7 +. 0) +. 25) >. ((5 +. 7) +. 17)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              994
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                -7927/100000
              • ((7 +. 0) +. 38) >. ((5 +. 7) +. 2)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              993
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000)
              • ((7 +. 0) +. 44) >. ((5 +. 7) +. 3)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              992
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000
              • ((7 +. 0) +. 139) >. ((5 +. 7) +. 1)
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000
              • not (((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. 17131/25000)
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 1422/3125)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              991
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000)
              • ((7 +. 39) +. 4) >. ((5 +. 0) +. 21)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              990
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500)
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 174327/100000
              • ((7 +. 39) +. 3) >. ((5 +. 0) +. 122)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              989
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • not (((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000)
              • ((7 +. 39) +. 1) >. ((5 +. 0) +. 4)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              988
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 5861/12500
              • ((input.radius_se -. 40517/100000) /. 27731/100000) <=. 20821/50000
              • ((7 +. 39) +. 28) >. ((5 +. 0) +. 3)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              987
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                 -7927/100000)
              • ((7 +. 39) +. 25) >. ((5 +. 0) +. 17)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              986
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000)
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=.
                -7927/100000
              • ((7 +. 39) +. 38) >. ((5 +. 0) +. 2)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              985
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000)
              • ((7 +. 39) +. 44) >. ((5 +. 0) +. 3)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/25000
              • ((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 22607/50000
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. -2163/20000)
              • not
                (((input.concave_points_worst -. 11461/100000) /. 6573/100000) <=. 2453/25000)
              • not (((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 265413/100000)
              • 5 <=. input.radius_mean
              • input.radius_mean <=. 35
              • 0 <=. input.compactness_mean
              • input.compactness_mean <=. 2/5
              • 0 <=. input.concavity_mean
              • input.concavity_mean <=. 1/2
              • 0 <=. input.radius_se
              • input.radius_se <=. 7/2
              • 0 <=. input.compactness_worst
              • input.compactness_worst <=. 6/5
              • 0 <=. input.concavity_worst
              • input.concavity_worst <=. 3/2
              • 0 <=. input.concave_points_worst
              • input.concave_points_worst <=. 7/20
              "benign"
              984
              • ((input.concavity_mean -. 111/1250) /. 1993/25000) <=. 10459/100000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -7603/20000
              • ((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -60659/100000
              • ((7 +. 39) +. 139) >. ((5 +. 0) +. 1)
              • not
                (((input.concavity_worst -. 27219/100000) /. 10431/50000) <=. -5799/100000)
              • ((input.radius_mean -. 1412729/100000) /. 70481/20000) <=. -4667/250