diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 433f3cac0..c3c31267c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -56681,17 +56681,13 @@ usage:
 int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
   extern void seteSLIMParams(eSLIM_ParamStruct* params);
   extern Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params);
-  extern Gia_Man_t* applyeSLIMIncremental(Gia_Man_t * pGia, const eSLIM_ParamStruct* params, unsigned int restarts, unsigned int deepsynTimeout);
-
-  int nruns = 0;
-  int deepsynTimeout = 180;
-  int runOneShotMode = 0;
+  
   eSLIM_ParamStruct params;
   int c;
   Gia_Man_t * pTemp;
   seteSLIMParams(&params);
   Extra_UtilGetoptReset();
-  while ( ( c = Extra_UtilGetopt( argc, argv, "DIPRSTVZfhnos" ) ) != EOF ) {
+  while ( ( c = Extra_UtilGetopt( argc, argv, "DIMPRSTVZdfhns" ) ) != EOF ) {
       switch ( c ) {
         case 'D':
           if ( globalUtilOptind >= argc )
@@ -56699,9 +56695,9 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
               Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
               goto usage;
           }
-          deepsynTimeout = atoi(argv[globalUtilOptind]);
+          params.timeout_inprocessing = atoi(argv[globalUtilOptind]);
           globalUtilOptind++;
-          if ( deepsynTimeout < 1 )
+          if ( params.timeout_inprocessing < 1 )
               goto usage;
           break;
         case 'I':
@@ -56715,6 +56711,17 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
           if ( params.iterations < 0 )
               goto usage;
           break;
+        case 'M':
+          if ( globalUtilOptind >= argc )
+          {
+              Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+              goto usage;
+          }
+          params.mode = atoi(argv[globalUtilOptind]);
+          globalUtilOptind++;
+          if ( params.mode < 0 || params.mode > 2)
+              goto usage;
+          break;
         case 'P':
           if ( globalUtilOptind >= argc )
           {
@@ -56723,7 +56730,7 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
           }
           params.expansion_probability = atof(argv[globalUtilOptind]);
           globalUtilOptind++;
-          if ( params.expansion_probability < 0 )
+          if ( params.expansion_probability <= 0 || params.expansion_probability > 1)
               goto usage;
           break;
         case 'R':
@@ -56732,9 +56739,9 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
               Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
               goto usage;
           }
-          nruns = atoi(argv[globalUtilOptind]);
+          params.nruns = atoi(argv[globalUtilOptind]);
           globalUtilOptind++;
-          if ( nruns < 0 )
+          if ( params.nruns < 1 )
               goto usage;
           break;
         case 'S':
@@ -56765,9 +56772,9 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
               Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
               goto usage;
           }
-          params.verbose = atoi(argv[globalUtilOptind]);
+          params.verbosity_level = atoi(argv[globalUtilOptind]);
           globalUtilOptind++;
-          if ( params.verbose < 0 || params.verbose > 2 )
+          if ( params.verbosity_level < 0 || params.verbosity_level > 3 )
               goto usage;
           break;
         case 'Z':
@@ -56780,6 +56787,9 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
           params.seed = atoi(argv[globalUtilOptind]);
           globalUtilOptind++;
           break;
+        case 'd' :
+          params.apply_inprocessing ^= 1;
+          break;
         case 'f' :
           params.forbidden_pairs ^= 1;
           break;
@@ -56788,9 +56798,6 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
         case 'n' :
           params.extended_normality_processing ^= 1;
           break;
-        case 'o' :
-          runOneShotMode ^= 1;
-          break;
         case 's' :
           params.fill_subcircuits ^= 1;
           break;
@@ -56803,31 +56810,28 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
         return 1;
   }
 
-  if (runOneShotMode) {
-    pTemp = applyeSLIM(pAbc->pGia, &params);
-  } else {
-    pTemp = applyeSLIMIncremental(pAbc->pGia, &params, nruns, deepsynTimeout);     
-  }
-  
+  pTemp = applyeSLIM(pAbc->pGia, &params);
+    
   Abc_FrameUpdateGia( pAbc, pTemp );
   return 0;
 
   usage:
-    Abc_Print( -2, "usage: &eslim [-RTIDSPAV <num>] [-ch]\n" );
+    Abc_Print( -2, "usage: &eslim [-DIMPRSTVZ <num>] [-dfhns]\n" );
     Abc_Print( -2, "\t           circuit minimization using exact synthesis and the SAT-based local improvement method (SLIM)\n" );
-    Abc_Print( -2, "\t-D <num> : the timeout in seconds for the individual deepsyn runs [default = %d]\n",    deepsynTimeout );
+    Abc_Print( -2, "\t-D <num> : the timeout in seconds for the individual deepsyn runs [default = %d]\n",    params.timeout_inprocessing );
     Abc_Print( -2, "\t-I <num> : the maximal number of iterations (0 = no limit) for the individual eSLIM runs [default = %d]\n",  params.iterations  );
+    Abc_Print( -2, "\t-M <num> : the synthesis mode to use [default = %d]\n",  params.mode  );
     Abc_Print( -2, "\t-P <num> : the probability of expanding a node [default = %.2f]\n",    params.expansion_probability );
-    Abc_Print( -2, "\t-R <num> : the number of runs of eSLIM + Inprocessing [default = %d]\n",    nruns );
+    Abc_Print( -2, "\t-R <num> : the number of runs of eSLIM + Inprocessing [default = %d]\n",    params.nruns );
     Abc_Print( -2, "\t-S <num> : the maximal size of considered subcircuits [default = %d]\n",    params.subcircuit_size_bound );
     Abc_Print( -2, "\t-T <num> : the timeout in seconds for the individual eSLIM runs [default = %d]\n",    params.timeout );
-    Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n",       params.verbose);
+    Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n",       params.verbosity_level);
     Abc_Print( -2, "\t-Z <num> : use a fixed seed\n",       params.seed);
+    Abc_Print( -2, "\t-d       : toggle inprocessing with deepsyn\n");
     Abc_Print( -2, "\t-f       : toggle using subcircuits with forbidden pairs\n");
     Abc_Print( -2, "\t-h       : print the command usage\n");
-    Abc_Print( -2, "\t-n       : extended normality processing\n");
-    Abc_Print( -2, "\t-o       : single run of eSLIM without inprocessing\n");
-    Abc_Print( -2, "\t-s       : fill subcircuits\n");
+    Abc_Print( -2, "\t-n       : toggle extended normality processing\n");
+    Abc_Print( -2, "\t-s       : toggle fill subcircuits\n");
     Abc_Print( -2, "\t\n" );
     Abc_Print( -2, "\t           This command was contributed by Franz-Xaver Reichl from University of Freiburg.\n" );
     return 1;
diff --git a/src/opt/eslim/eSLIM.cpp b/src/opt/eslim/eSLIM.cpp
index 142531090..24200e6e2 100644
--- a/src/opt/eslim/eSLIM.cpp
+++ b/src/opt/eslim/eSLIM.cpp
@@ -46,7 +46,7 @@ eSLIM::eSLIMConfig getCfg(const eSLIM_ParamStruct* params) {
   config.strash_intervall = params->strash_intervall;
   config.nselection_trials = params->nselection_trials;
   config.seed = params->seed;
-  config.verbose = params->verbose;
+  config.verbosity_level = params->verbosity_level;
   config.expansion_probability = params->expansion_probability;
   return config;
 }
@@ -58,15 +58,18 @@ void seteSLIMParams(eSLIM_ParamStruct* params) {
   params->apply_strash = 1;
   params->fix_seed = 0;
   params->trial_limit_active = 1;
+  params->apply_inprocessing = 1;
   params->timeout = 1620;
+  params->timeout_inprocessing = 180;
   params->iterations = 0;
   params->subcircuit_size_bound = 6;
   params->strash_intervall = 100;
   params->nselection_trials = 100;
+  params->nruns = 1;
   params->mode = 0;
   params->seed = 0;
-  params->verbose = 0;
-  params->expansion_probability = 0.4;
+  params->verbosity_level = 1;
+  params->expansion_probability = 0.4;           
 }
    
 Gia_Man_t* selectApproach(Gia_Man_t* pGia, eSLIM::eSLIMConfig params, eSLIM::eSLIMLog& log, int approach, bool allow_forbidden_pairs) {
@@ -83,6 +86,12 @@ Gia_Man_t* selectApproach(Gia_Man_t* pGia, eSLIM::eSLIMConfig params, eSLIM::eSL
       } else {
         return eSLIM::eSLIM_Man<eSLIM::KissatOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
       };
+    case 2:
+      if (allow_forbidden_pairs) {
+        return eSLIM::eSLIM_Man<eSLIM::KissatCmdOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
+      } else {
+        return eSLIM::eSLIM_Man<eSLIM::KissatCmdOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
+      };
     default:
       std::cerr << "eSLIM -- Invalid mode given\n";
       assert (false && "Invalid approach selected");
@@ -90,89 +99,113 @@ Gia_Man_t* selectApproach(Gia_Man_t* pGia, eSLIM::eSLIMConfig params, eSLIM::eSL
   }
 }
 
-Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) {
-  eSLIM::eSLIMConfig config = getCfg(params);
-  int initial_size = Gia_ManAndNum(pGia);
-  Gia_Man_t * temp = Gia_ManDup(pGia);
-  eSLIM::eSLIMLog log(params->subcircuit_size_bound);
-  Gia_Man_t* result = selectApproach(temp, config, log, params->mode, params->forbidden_pairs);
-  if (params->verbose > 0) {
-    std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n";
-    int new_size = initial_size - Gia_ManAndNum(result);
-    std::cout << "#reduced gates: " << new_size << "\n";
+Gia_Man_t* runInprocessing(Gia_Man_t * pGia, const eSLIM_ParamStruct* params, unsigned int it) {
+  Gia_Man_t * tmp = Gia_ManDeepSyn( pGia, 1, ABC_INFINITY, params->timeout_inprocessing, 0, params->seed + it, 0, 0);
+  if ( Gia_ManAndNum(pGia) > Gia_ManAndNum(tmp) ) {
+    Gia_ManStop( pGia );
+    pGia = tmp;
+  } else {
+    Gia_ManStop( tmp );
   }
-  return result;
-
+  return pGia;
 }
 
-Gia_Man_t* applyeSLIMIncremental(Gia_Man_t* pGia, const eSLIM_ParamStruct* params, unsigned int restarts, unsigned int deepsynTimeout) {
+void printSetting(const eSLIM_ParamStruct* params) {
+  std::cout << "Apply eSLIM (timeout: " << params->timeout << ") ";
+  if (params->apply_inprocessing) {
+    std::cout << "+ deepsyn (timeout: " << params->timeout_inprocessing << ") ";
+  }
+  std::cout << params->nruns << " times.\n";
+  if (params->iterations > 0) {
+    std::cout << "Stop eSLIM runs after " << params->iterations << " iterations.\n";
+  }
+  std::cout << "Consider subcircuits with up to " << params->subcircuit_size_bound << " gates.\n";
+  printf("When expanding subcircuits, select gates with a probability of %.2f %%.\n", 100 * params->expansion_probability);
+  if (params->forbidden_pairs) {
+    std::cout << "Consider subcircuits containing gates, which are connected outside of the subcircuit.\n";
+  }
+  if (params->mode == 0) {
+    std::cout << "Use an incremental SAT encoding for exact synthesis and the SAT solver CaDiCaL.\n";
+  } else {
+    std::cout << "Use a one-shot SAT encoding for exact synthesis and the SAT solver Kissat.\n";
+  }
+}
+
+Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) {
   eSLIM::eSLIMConfig config = getCfg(params);
-  config.verbose = params->verbose > 1;
+  config.verbosity_level = params->verbosity_level;
 
   int eSLIM_reductions = 0;
   int deepsyn_reductions = 0;
 
   Gia_Man_t * pThis = Gia_ManDup(pGia);
-  Gia_Man_t * tmp;
   eSLIM::eSLIMLog log(params->subcircuit_size_bound);
   int initial_size = Gia_ManAndNum(pThis);
-  if (params->verbose > 0) {
+  if (params->verbosity_level > 0) {
+    printSetting(params);
     std::cout << "Initial size: " << initial_size << "\n";
   }
-
-  for (unsigned int i = 0; i <= restarts; i++) {
+  for (unsigned int i = 0; i < params->nruns; i++) {
     if (config.fix_seed) {
       config.seed = params->seed + i;
     }
-
     int size_iteration_start = Gia_ManAndNum(pThis);
+    if (params->verbosity_level > 0) {
+      std::cout << "Start eslim run " << i + 1 << "\n";
+    }
     pThis = selectApproach(pThis, config, log, params->mode, params->forbidden_pairs);
     int size_eslim = Gia_ManAndNum(pThis);
     eSLIM_reductions += size_iteration_start - size_eslim;
-    if (params->verbose > 0) {
-      std::cout << "Size eSLIM it-" << i << " : " << size_eslim << "\n";
-    }
 
-    tmp = Gia_ManDeepSyn( pThis, 1, ABC_INFINITY, deepsynTimeout, 0, params->seed + i, 0, 0);
-    int size_deepsyn = Gia_ManAndNum(tmp);
-
-    if ( Gia_ManAndNum(pThis) > Gia_ManAndNum(tmp) ) {
-      Gia_ManStop( pThis );
-      pThis = tmp;
-      deepsyn_reductions += size_eslim - size_deepsyn;
-    } else {
-      Gia_ManStop( tmp );
+    if (params->apply_inprocessing) {
+      if (params->verbosity_level > 0) {
+        std::cout << "Start inprocessing run " << i + 1 << "\n";
+      }
+      pThis = runInprocessing(pThis, params, i);
+      if (params->verbosity_level > 0) {
+        std::cout << "Inprocessing: Initial size: " << size_eslim << " final size: " << Gia_ManAndNum(pThis) << "\n";
+      }
+      deepsyn_reductions += size_eslim - Gia_ManAndNum(pThis);
     }
   }
+  if (params->verbosity_level > 0) {
+    int final_size = Gia_ManAndNum(pThis);
+    std::cout << "Final size: " << final_size << "\n";
+    int total_reductions = eSLIM_reductions + deepsyn_reductions;
+    double reduction_ratio = 100 * static_cast<double>(total_reductions) / initial_size; 
+    printf("Total reduction: %d (%.2f %%)\n", total_reductions, reduction_ratio);
+    if (params->apply_inprocessing) {
+      std::cout << "#Gates reduced by eSLIM: " << eSLIM_reductions << " ";
+      std::cout << "#Gates reduced by deepsyn: " << deepsyn_reductions << "\n";
+    } 
+  }
 
-  if (params->verbose > 0) {
-    std::cout << "#Gates reduced by eSLIM: " << eSLIM_reductions << "\n";
-    std::cout << "#Gates reduced by deepsyn: " << deepsyn_reductions << "\n";
+  if (params->verbosity_level > 1) {
     std::cout << "Total #iterations: " << log.iteration_count << "\n";
     std::cout << "Total relation generation time (s): " << log.relation_generation_time << "\n";
     std::cout << "Total synthesis time (s): " << log.synthesis_time << "\n";
     std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n";
-
+  }
+  if (params->verbosity_level > 2) {
     for (int i = 2; i < log.nof_analyzed_circuits_per_size.size(); i++) {
       int replaced = log.nof_replaced_circuits_per_size.size() > i ? log.nof_replaced_circuits_per_size[i] : 0;
       int reduced = log.nof_reduced_circuits_per_size.size() > i ? log.nof_reduced_circuits_per_size[i] : 0;
       std::cout << "#gates: " << i << " - #analysed: " << log.nof_analyzed_circuits_per_size[i] << " - #replaced: " << replaced << " - #reduced: " << reduced << "\n";
     }
-  }
-
-  if (params->verbose > 1) {
-    for (int i = 0; i < log.nof_sat_calls_per_size.size(); i++) {
-      if (log.nof_sat_calls_per_size[i] == 0) {
-        std::cout << "#gates: " << i << " - avg. sat time: -\n";
-      } else {
-        std::cout << "#gates: " << i << " - avg. sat time: " << static_cast<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]) << " sec\n";
+    if (params->mode == 0) {
+      for (int i = 0; i < log.nof_sat_calls_per_size.size(); i++) {
+        if (log.nof_sat_calls_per_size[i] == 0) {
+          std::cout << "#gates: " << i << " - avg. sat time: -\n";
+        } else {
+          std::cout << "#gates: " << i << " - avg. sat time: " << static_cast<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]) << " sec\n";
+        }
       }
-    }
-    for (int i = 0; i < log.nof_unsat_calls_per_size.size(); i++) {
-      if (log.nof_unsat_calls_per_size[i] == 0) {
-        std::cout << "#gates: " << i << " - avg. unsat time: -\n";
-      } else {
-        std::cout << "#gates: " << i << " - avg. unsat time: " << static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n";
+      for (int i = 0; i < log.nof_unsat_calls_per_size.size(); i++) {
+        if (log.nof_unsat_calls_per_size[i] == 0) {
+          std::cout << "#gates: " << i << " - avg. unsat time: -\n";
+        } else {
+          std::cout << "#gates: " << i << " - avg. unsat time: " << static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n";
+        }
       }
     }
   }
diff --git a/src/opt/eslim/eSLIM.h b/src/opt/eslim/eSLIM.h
index 1d4bc2175..857e32f47 100644
--- a/src/opt/eslim/eSLIM.h
+++ b/src/opt/eslim/eSLIM.h
@@ -30,21 +30,25 @@ ABC_NAMESPACE_HEADER_START
   struct eSLIM_ParamStruct_ {
     int forbidden_pairs;                                // Allow forbidden pairs in the selected subcircuits
     int extended_normality_processing;                  // Additional checks for non normal subcircuits
-    double expansion_probability;                       // the probability that a node is added to the subcircuit
     int fill_subcircuits;                               // If a subcircuit has fewer than subcircuit_size_bound gates, try to fill it with rejected gates.
     int apply_strash;                                   
     int fix_seed;                                       
     int trial_limit_active;
+    int apply_inprocessing;
     
     unsigned int timeout;                               // available time in seconds (soft limit)
+    unsigned int timeout_inprocessing;
     unsigned int iterations;                            // maximal number of iterations. No limit if 0
     unsigned int subcircuit_size_bound;                 // upper bound for the subcircuit sizes
     unsigned int strash_intervall;    
     unsigned int nselection_trials;
+    unsigned int nruns;
+
+    double expansion_probability;                       // the probability that a node is added to the subcircuit
 
     int mode;                                           // 0: Cadical Incremental, 1: Kissat Oneshot                                       
     int seed;
-    int verbose;                                        
+    int verbosity_level;                                        
 
   };
 
diff --git a/src/opt/eslim/eSLIMMan.hpp b/src/opt/eslim/eSLIMMan.hpp
index 5a6718099..22114dd09 100644
--- a/src/opt/eslim/eSLIMMan.hpp
+++ b/src/opt/eslim/eSLIMMan.hpp
@@ -54,10 +54,6 @@ namespace eSLIM {
       void findReplacement();
       Mini_Aig_t* findMinimumAig(const Subcircuit& subcir);
 
-      Abc_RData_t* generateRelation(const Subcircuit& subcir);
-      Vec_Int_t* generateRelationPatterns(const Subcircuit& subcir);
-      Abc_RData_t* constructABCRelationRepresentation(int nof_inputs, int nof_outputs, Vec_Int_t * patterns);
-
       Vec_Wrd_t* getSimsIn(Abc_RData_t* relation);
       Vec_Wrd_t* getSimsOut(Abc_RData_t* relation);
       word getAllFalseBehaviour(const Subcircuit& subcir);
diff --git a/src/opt/eslim/eSLIMMan.tpp b/src/opt/eslim/eSLIMMan.tpp
index ae12e2bb7..8eb46db5c 100644
--- a/src/opt/eslim/eSLIMMan.tpp
+++ b/src/opt/eslim/eSLIMMan.tpp
@@ -32,7 +32,6 @@
 
 
 ABC_NAMESPACE_HEADER_START
-  Vec_Int_t* Gia_ManGenIoCombs( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, int fVerbose );
   Mini_Aig_t * Mini_AigDupCompl( Mini_Aig_t * p, int ComplIns, int ComplOuts );
   int Exa6_ManFindPolar( word First, int nOuts );
   Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns );
@@ -47,13 +46,11 @@ namespace eSLIM {
   Gia_Man_t* eSLIM_Man<Y, R, S>::applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log) {
     eSLIM_Man<Y, R, S> eslim(p, cfg, log);
     eslim.minimize();
-    if (cfg.verbose > 0) {
-      std::cout << "Relation generation time: " << log.relation_generation_time - eslim.relation_generation_time << "\n";
-      std::cout << "Synthesis time: " << log.synthesis_time - eslim.synthesis_time << "\n";
-    }
     return eslim.getCircuit();
   }
 
+
+
   template <typename Y, typename R, typename S>
   eSLIM_Man<Y, R, S>::eSLIM_Man(Gia_Man_t * pGia, const eSLIMConfig& cfg, eSLIMLog& log) 
             : gia_man(pGia), cfg(cfg), log(log), 
@@ -71,6 +68,7 @@ namespace eSLIM {
     abctime nTimeToStop = clkStart + cfg.timeout * CLOCKS_PER_SEC;
     unsigned int iteration = 0;
     unsigned int iterMax = cfg.iterations ? cfg.iterations - 1 : UINT_MAX;
+    int current_size = Gia_ManAndNum(gia_man);
     while (Abc_Clock() <= nTimeToStop && iteration <= iterMax && !stopeSLIM) {
       iteration++;
       findReplacement();
@@ -84,59 +82,26 @@ namespace eSLIM {
         gia_man = Gia_ManRehash( pTemp, 0 );
         Gia_ManStop( pTemp );
       }
-    }
-    log.iteration_count += iteration;
-
-    if (cfg.verbose) {
-      printf( "Time %8.2f sec\n", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC );
-      std::cout << "#Iterations: " << iteration << "\n";
-    }
-  }
-
-  template <typename Y, typename R, typename S>
-  Abc_RData_t* eSLIM_Man<Y, R, S>::generateRelation(const Subcircuit& subcir) {
-    int nof_outputs = Vec_IntSize(subcir.io) - subcir.nof_inputs;
-    assert(Vec_IntSize(subcir.io) <= 32); 
-    abctime relation_generation_start = Abc_Clock();
-    Vec_Int_t* relation_patterns_masks = generateRelationPatterns(subcir);
-    log.relation_generation_time += (double)1.0*(Abc_Clock() - relation_generation_start)/CLOCKS_PER_SEC;
-    Abc_RData_t* relation = constructABCRelationRepresentation(subcir.nof_inputs, nof_outputs, relation_patterns_masks);
-    Vec_IntFree(relation_patterns_masks);
-    return relation;
-  }
-
-  template <typename Y, typename R, typename S>
-  Vec_Int_t* eSLIM_Man<Y, R, S>::generateRelationPatterns(const Subcircuit& subcir) {
-    Vec_Int_t * vRes = RelationGenerator<R>::computeRelation(gia_man, subcir);
-    if ( vRes == NULL ) {
-      return nullptr;
-    }
-    return vRes;
-  }
-
-  template <typename Y, typename R, typename S>
-  Abc_RData_t* eSLIM_Man<Y, R, S>::constructABCRelationRepresentation(int nof_inputs, int nof_outputs, Vec_Int_t * patterns) {
-    int i, mask;
-    int nof_vars = nof_inputs + nof_outputs;
-    Abc_RData_t* p = Abc_RDataStart( nof_inputs, nof_outputs, Vec_IntSize(patterns) );
-    Vec_IntForEachEntry( patterns, mask, i ) {
-      for ( int k = 0; k < nof_vars; k++ ) {
-        if ( (mask >> (nof_vars-1-k)) & 1 ) { 
-          if ( k < nof_inputs ) {
-            Abc_RDataSetIn( p, k, i );
-          } else {
-            Abc_RDataSetOut( p, 2*(k-nof_inputs)+1, i );
-          }      
-        } else { 
-          if ( k >= nof_inputs ) {
-            Abc_RDataSetOut( p, 2*(k-nof_inputs), i );
-          }
+      if (cfg.verbosity_level > 0) {
+        int sz = Gia_ManAndNum(gia_man);
+        if (sz < current_size) {
+          current_size = sz;
+          printf("\rIteration %8d : #and = %7d elapsed time = %7.2f sec\n", iteration, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
+        } else {
+          printf("\rIteration %8d", iteration);
+          fflush(stdout);
         }
       }
     }
-    Abc_RData_t* p2 = Abc_RData2Rel(p);
-    Abc_RDataStop(p);
-    return p2;
+    log.iteration_count += iteration;
+    if (cfg.verbosity_level > 0) {
+      int sz = Gia_ManAndNum(gia_man);
+      printf("\r#Iterations %8d #and = %7d elapsed time = %7.2f sec\n", iteration, sz, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC);
+      if (cfg.verbosity_level > 1) {
+        printf("Relation generation time: %.2f sec\n", log.relation_generation_time - relation_generation_time);
+        printf("Synthesis time: %.2f sec\n", log.synthesis_time - synthesis_time);
+      } 
+    }
   }
 
   template <typename Y, typename R, typename S>
@@ -190,15 +155,18 @@ namespace eSLIM {
     if (subcir.forbidden_pairs.size() > 0) {
       log.subcircuits_with_forbidden_pairs++;
     }
+    
+    abctime relation_generation_start = Abc_Clock();
+    Abc_RData_t* relation = RelationGenerator<R>::computeRelation(gia_man, subcir);
+    log.relation_generation_time += (double)1.0*(Abc_Clock() - relation_generation_start)/CLOCKS_PER_SEC;
 
-    Abc_RData_t* relation = generateRelation(subcir);
     int nDivs = 0;
     int nOuts = relation->nOuts;
     int nVars = relation->nIns;
     if ( nVars == 0 ) {
       return nullptr;
     }
-    assert (nVars <= 8); //Assertion from original ABC code
+    // assert (nVars <= 8);
     Vec_Wrd_t* vSimsDiv = getSimsIn(relation);
     Vec_Wrd_t* vSimsOut = getSimsOut(relation);
 
diff --git a/src/opt/eslim/relationGeneration.hpp b/src/opt/eslim/relationGeneration.hpp
index 2d29fe8ef..28d8dc512 100644
--- a/src/opt/eslim/relationGeneration.hpp
+++ b/src/opt/eslim/relationGeneration.hpp
@@ -28,6 +28,8 @@
 #include "misc/util/abc_namespaces.h"
 #include <misc/util/abc_global.h>
 #include "aig/gia/gia.h"
+#include "misc/util/utilTruth.h" // ioResub.h depends on utilTruth.h
+#include "base/io/ioResub.h"
 
 #include "utils.hpp"
 // #include "satInterfaces.hpp"
@@ -41,8 +43,8 @@ namespace eSLIM {
   class RelationGenerator {
 
     public:
-      static Vec_Int_t* computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir);
-
+      static Abc_RData_t* computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir);
+      
     private:
       Gia_Man_t* pGia;
       const Subcircuit& subcir; 
@@ -51,6 +53,12 @@ namespace eSLIM {
       void setup();
       Vec_Int_t* getRelation();
 
+      static Abc_RData_t* constructABCRelationRepresentation(Vec_Int_t * patterns, int nof_inputs, int nof_outputs);
+      // Reimplementation with disabled prints
+      // We do not want to modify code in other parts of ABC
+      static Abc_RData_t * Abc_RData2Rel( Abc_RData_t * p );
+      
+
     friend Derived;
   };
 
@@ -85,10 +93,90 @@ namespace eSLIM {
   }
 
   template <typename T>
-  inline Vec_Int_t* RelationGenerator<T>::computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir) {
+  inline Abc_RData_t* RelationGenerator<T>::computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir) {
     T generator(gia_man, subcir);
     generator.setup();
-    return generator.getRelation();
+    Vec_Int_t* relation_patterns_masks = generator.getRelation();
+    if ( relation_patterns_masks == NULL ) {
+      return nullptr;
+    }
+    int nof_inputs = subcir.nof_inputs;
+    int nof_outputs = Vec_IntSize(subcir.io) - subcir.nof_inputs;
+    Abc_RData_t* r = constructABCRelationRepresentation(relation_patterns_masks, nof_inputs, nof_outputs);
+    Vec_IntFree(relation_patterns_masks);
+    return r;
+  }
+
+  template <typename T>
+  inline Abc_RData_t* RelationGenerator<T>::constructABCRelationRepresentation(Vec_Int_t * patterns,  int nof_inputs, int nof_outputs) {
+    int i, mask;
+    int nof_vars = nof_inputs + nof_outputs;
+    Abc_RData_t* p = Abc_RDataStart( nof_inputs, nof_outputs, Vec_IntSize(patterns) );
+    Vec_IntForEachEntry( patterns, mask, i ) {
+      for ( int k = 0; k < nof_vars; k++ ) {
+        if ( (mask >> (nof_vars-1-k)) & 1 ) { 
+          if ( k < nof_inputs ) {
+            Abc_RDataSetIn( p, k, i );
+          } else {
+            Abc_RDataSetOut( p, 2*(k-nof_inputs)+1, i );
+          }      
+        } else { 
+          if ( k >= nof_inputs ) {
+            Abc_RDataSetOut( p, 2*(k-nof_inputs), i );
+          }
+        }
+      }
+    }
+    Abc_RData_t* p2 = Abc_RData2Rel(p);
+    Abc_RDataStop(p);
+    return p2;
+  }
+
+  template <typename T>
+  inline Abc_RData_t * RelationGenerator<T>::Abc_RData2Rel( Abc_RData_t * p ) {
+    assert( p->nIns < 64 );
+    assert( p->nOuts < 32 );
+    int w;
+    Vec_Wrd_t * vSimsIn2  = Vec_WrdStart( 64*p->nSimWords );
+    Vec_Wrd_t * vSimsOut2 = Vec_WrdStart( 64*p->nSimWords );
+    for ( w = 0; w < p->nIns; w++ )
+        Abc_TtCopy( Vec_WrdEntryP(vSimsIn2,  w*p->nSimWords), Vec_WrdEntryP(p->vSimsIn, w*p->nSimWords), p->nSimWords, 0 );
+    for ( w = 0; w < p->nOuts; w++ )
+        Abc_TtCopy( Vec_WrdEntryP(vSimsOut2, w*p->nSimWords), Vec_WrdEntryP(p->vSimsOut, (2*w+1)*p->nSimWords), p->nSimWords, 0 );
+    Vec_Wrd_t * vTransIn  = Vec_WrdStart( 64*p->nSimWords );
+    Vec_Wrd_t * vTransOut = Vec_WrdStart( 64*p->nSimWords );
+    Extra_BitMatrixTransposeP( vSimsIn2,  p->nSimWords, vTransIn,  1 );
+    Extra_BitMatrixTransposeP( vSimsOut2, p->nSimWords, vTransOut, 1 );
+    Vec_WrdShrink( vTransIn,  p->nPats );
+    Vec_WrdShrink( vTransOut, p->nPats );
+    Vec_Wrd_t * vTransInCopy = Vec_WrdDup(vTransIn); 
+    Vec_WrdUniqify( vTransInCopy );
+    // if ( Vec_WrdSize(vTransInCopy) == p->nPats )
+    //     printf( "This resub problem is not a relation.\n" );
+    // create the relation
+    Abc_RData_t * pNew = Abc_RDataStart( p->nIns, 1 << (p->nOuts-1), Vec_WrdSize(vTransInCopy) );
+    pNew->nOuts = p->nOuts;
+    int i, k, n, iLine = 0; word Entry, Entry2;
+    Vec_WrdForEachEntry( vTransInCopy, Entry, i ) {
+        for ( n = 0; n < p->nIns; n++ )
+            if ( (Entry >> n) & 1 )
+                Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsIn, n*pNew->nSimWords), iLine );
+        Vec_WrdForEachEntry( vTransIn, Entry2, k ) {
+            if ( Entry != Entry2 )
+                continue;
+            Entry2 = Vec_WrdEntry( vTransOut, k );
+            assert( Entry2 < (1 << p->nOuts) );
+            Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsOut, Entry2*pNew->nSimWords), iLine );
+        }
+        iLine++;
+    }
+    assert( iLine == pNew->nPats );
+    Vec_WrdFree( vTransOut );
+    Vec_WrdFree( vTransInCopy );
+    Vec_WrdFree( vTransIn );
+    Vec_WrdFree( vSimsIn2 );
+    Vec_WrdFree( vSimsOut2 );
+    return pNew;    
   }
 
   template <typename T>
diff --git a/src/opt/eslim/selectionStrategy.hpp b/src/opt/eslim/selectionStrategy.hpp
index b4f0ccf80..29650a5d7 100644
--- a/src/opt/eslim/selectionStrategy.hpp
+++ b/src/opt/eslim/selectionStrategy.hpp
@@ -104,7 +104,7 @@ namespace eSLIM {
 
   template<typename T>
   SelectionStrategy<T>::SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
-                      : gia_man(gia_man), cfg(cfg), log(log), rng(std::random_device()()) {
+                      : gia_man(gia_man), cfg(cfg), log(log), rng(std::random_device()()), bdist(cfg.expansion_probability) {
   }
 
   template<typename T>
diff --git a/src/opt/eslim/selectionStrategy.tpp b/src/opt/eslim/selectionStrategy.tpp
index ba150d624..94f656a5b 100644
--- a/src/opt/eslim/selectionStrategy.tpp
+++ b/src/opt/eslim/selectionStrategy.tpp
@@ -45,9 +45,11 @@ namespace eSLIM {
 
   template<typename T>
   bool SelectionStrategy<T>::filterSubcircuit(const Subcircuit& subcir) {
-    if (subcir.nof_inputs > 8) {
+    // if (subcir.nof_inputs > 8) {
+    if (subcir.nof_inputs > 10) {
       return false;
     }
+    // ABC internally requires that the subcircuit has not more than 6 outputs (e.g. generateMinterm)
     if (Vec_IntSize(subcir.io)-subcir.nof_inputs > 6) {
       return false;
     }
diff --git a/src/opt/eslim/synthesisEngine.tpp b/src/opt/eslim/synthesisEngine.tpp
index cc1d3d610..6a8485f7f 100644
--- a/src/opt/eslim/synthesisEngine.tpp
+++ b/src/opt/eslim/synthesisEngine.tpp
@@ -19,6 +19,12 @@
 ***********************************************************************/
 
 #include <numeric>
+#ifdef WIN32
+  #include <process.h> 
+  #define unlink _unlink
+#else
+  #include <unistd.h>
+#endif
 
 #include "misc/util/utilTruth.h"
 
@@ -613,6 +619,7 @@ namespace eSLIM {
       return nullptr;
     }
     Vec_Int_t * vRes = Exa4_ManParse( pFileNameOut );
+    unlink( pFileNameIn );
     return vRes;
   }
 
diff --git a/src/opt/eslim/utils.hpp b/src/opt/eslim/utils.hpp
index bcf2262c1..fb942c417 100644
--- a/src/opt/eslim/utils.hpp
+++ b/src/opt/eslim/utils.hpp
@@ -55,7 +55,7 @@ namespace eSLIM {
     int minimum_dynamic_timeout_sample_size = 50;
     double dynamic_timeout_buffer_factor = 1.4;
 
-    int verbose = 0;
+    int verbosity_level = 0;
   };
 
   struct eSLIMLog {