diff --git a/Project.toml b/Project.toml
index 85578e5..ebecfab 100644
--- a/Project.toml
+++ b/Project.toml
@@ -43,6 +43,7 @@ DataFrames = "1"
 DataStructures = "0.18"
 Graphs = "1.8"
 HTTP = "1.9"
+IntervalSets = "0.7.10"
 Lazy = "0.15"
 MLJModelInterface = "1.9"
 MultiData = "0 - 0.1"
@@ -53,7 +54,7 @@ Reexport = "1"
 Revise = "3"
 ScientificTypes = "3"
 SoleBase = "0.12"
-SoleLogics = "0.11"
+SoleLogics = "0.9 - 0.11"
 StatsBase = "0.30 - 0.34"
 Tables = "1"
 ThreadSafeDicts = "0.1"
@@ -66,8 +67,8 @@ Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6"
 InteractiveUtils = "b77e0a4c-d291-57a0-90e8-8db25a27a240"
 MLJBase = "a7f614a8-145f-11e9-1d2a-a57a1082229d"
 Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a"
-PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
 Plots = "91a5bcdd-55d7-5caf-9e0b-520d859cae80"
+PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
 
 [targets]
diff --git a/src/deprecate.jl b/src/deprecate.jl
index 99f9c93..9c07e25 100644
--- a/src/deprecate.jl
+++ b/src/deprecate.jl
@@ -1,4 +1,4 @@
-const BoundedScalarConditions = MultivariateScalarAlphabet{ScalarCondition}
+const BoundedScalarConditions = MultivariateScalarAlphabet{ScalarCondition} 
 
 function BoundedScalarConditions(
     metaconditions::Vector{<:ScalarMetaCondition},
diff --git a/src/minimize.jl b/src/minimize.jl
index 6744842..b74b255 100644
--- a/src/minimize.jl
+++ b/src/minimize.jl
@@ -1,7 +1,17 @@
 
-function espresso_minimize(syntaxtree::SoleLogics.Formula, silent::Bool = true, Dflag = "exact", Sflag = nothing, eflag = nothing, args...; otherflags = [], kwargs...)
+function espresso_minimize(
+    syntaxtree::SoleLogics.Formula,
+    silent::Bool = true,
+    Dflag = "exact",
+    Sflag = nothing,
+    eflag = nothing,
+    args...;
+    otherflags = [],
+    use_scalar_range_conditions = false,
+    kwargs...
+)
     dc_set = false
-    pla_string, others... = PLA._formula_to_pla(syntaxtree, dc_set, silent, args...; kwargs...)
+    pla_string, pla_args, pla_kwargs = PLA._formula_to_pla(syntaxtree, dc_set, silent, args...; use_scalar_range_conditions, kwargs...)
 
     silent || println()
     silent || println(pla_string)
@@ -41,5 +51,6 @@ function espresso_minimize(syntaxtree::SoleLogics.Formula, silent::Bool = true,
 
     minimized_pla = String(read(out))
     silent || println(minimized_pla)
-    return PLA._pla_to_formula(minimized_pla, others...)
+    conditionstype = use_scalar_range_conditions ? SoleData.RangeScalarCondition : SoleData.ScalarCondition
+    return PLA._pla_to_formula(minimized_pla, silent, pla_args...; conditionstype, pla_kwargs...)
 end
diff --git a/src/scalar-pla.jl b/src/scalar-pla.jl
index 7cc8357..978badc 100644
--- a/src/scalar-pla.jl
+++ b/src/scalar-pla.jl
@@ -29,45 +29,59 @@ _removewhitespaces = x->replace(x, (' ' => ""))
 
 
 # Function to encode a disjunct into a PLA row
-function encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVector, conditions::AbstractVector, includes, excludes, cond_idxss)
+function encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVector, conditions::AbstractVector, includes, excludes, feat_condindxss)
     pla_row = fill("-", length(conditions))
     # For each atom in the disjunct, add zeros or ones to relevants
     for lit in SoleLogics.grandchildren(disjunct)
-        # @show lit
+        # @show syntaxstring(lit)
+        ispos = SoleLogics.ispos(lit)
         cond = SoleLogics.value(atom(lit))
-        feature = SoleData.feature(cond)
-        i_feat = findfirst((f)->f==feature, features)
-        cond_idxs = cond_idxss[i_feat]
-        @show cond_idxs
-        @show cond
-        icond = findfirst(c->c==cond, conditions[cond_idxs])
-        @show icond
-        # pla_row[map(c->c==cond, conditions)] .= SoleLogics.ispos(lit) ? "1" : "0"
-        if SoleData.hasdual(cond)
-            idualcond = findfirst(c->c==SoleData.dual(cond), conditions[cond_idxs])
-            @show idualcond
-            # pla_row[map(c->c==SoleData.dual(cond), conditions)] .= SoleLogics.ispos(lit) ? "0" : "1"
+        # @show cond
+
+        i_feat = findfirst((f)->f==SoleData.feature(cond), features)
+        feat_condindxs = feat_condindxss[i_feat]
+        # @show feat_condindxs
+        feat_icond = findfirst(c->c==cond, conditions[feat_condindxs])
+        feat_idualcond = SoleData.hasdual(cond) ? findfirst(c->c==SoleData.dual(cond), conditions[feat_condindxs]) : nothing
+        # @show feat_icond, feat_idualcond
+        @assert !(isnothing(feat_icond) && isnothing(feat_idualcond))
+
+        # if ispos
+        #     @show excludes[i_feat]
+        #     if !isnothing(feat_icond)
+        #         @views pla_row[feat_condindxs][map(ic->includes[i_feat][feat_icond,ic], eachindex(feat_condindxs))] .= "1"
+        #         @views pla_row[feat_condindxs][map(ic->excludes[i_feat][feat_icond,ic], eachindex(feat_condindxs))] .= "0"
+        #     end
+        # else
+        #     # if !isnothing(feat_idualcond)
+        #     #     @views pla_row[feat_condindxs][map(ic->includes[i_feat][feat_idualcond,ic], eachindex(feat_condindxs))] .= "0"
+        #     #     @views pla_row[feat_condindxs][map(ic->excludes[i_feat][feat_idualcond,ic], eachindex(feat_condindxs))] .= "1"
+        #     # end
+        # end
+        POS, NEG = ispos ? ("1", "0") : ("0", "1")
+        if !isnothing(feat_icond)
+            @views pla_row[feat_condindxs][map(((ic,c),)->includes[i_feat][feat_icond,ic], enumerate(feat_condindxs))] .= POS
+            @views pla_row[feat_condindxs][map(((ic,c),)->excludes[i_feat][feat_icond,ic], enumerate(feat_condindxs))] .= NEG
         end
-
-        if SoleLogics.ispos(lit)
-            if !isnothing(icond)
-                @views pla_row[cond_idxs][map(((ic,c),)->includes[i_feat][icond,ic], enumerate(cond_idxs))] .= "1"
-                @views pla_row[cond_idxs][map(((ic,c),)->excludes[i_feat][icond,ic], enumerate(cond_idxs))] .= "0"
-            end
-        else
-            if SoleData.hasdual(cond) && !isnothing(idualcond)
-                @views pla_row[cond_idxs][map(((ic,c),)->includes[i_feat][idualcond,ic], enumerate(cond_idxs))] .= "1"
-                @views pla_row[cond_idxs][map(((ic,c),)->excludes[i_feat][idualcond,ic], enumerate(cond_idxs))] .= "0"
-            end
+        if !isnothing(feat_idualcond)
+            @views pla_row[feat_condindxs][map(((ic,c),)->includes[i_feat][feat_idualcond,ic], enumerate(feat_condindxs))] .= NEG
+            @views pla_row[feat_condindxs][map(((ic,c),)->excludes[i_feat][feat_idualcond,ic], enumerate(feat_condindxs))] .= POS
         end
     end
-
+    # println(pla_row)
     return pla_row
 end
 
 # Function to parse and process the formula into PLA
-# function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent = true, args...; encoding = :multivariate, kwargs...)
-function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent = true, args...; encoding = :univariate, kwargs...)
+function _formula_to_pla(
+    formula::SoleLogics.Formula,
+    dc_set = false,
+    silent = true,
+    args...;
+    encoding = :univariate,
+    use_scalar_range_conditions = false,
+    kwargs...
+)
     @assert encoding in [:univariate, :multivariate]
     
     scalar_kwargs = (;
@@ -75,11 +89,17 @@ function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent
         allow_atom_flipping = true,
     )
 
-    dnfformula = SoleLogics.dnf(syntaxtree, Atom; scalar_kwargs..., kwargs...)
+    dnfformula = SoleLogics.dnf(formula, Atom; scalar_kwargs..., kwargs...)
 
+    scalar_simplification_kwargs = (;
+        force_scalar_range_conditions = use_scalar_range_conditions, 
+        allow_scalar_range_conditions = use_scalar_range_conditions,
+    )
     silent || @show dnfformula
-
-    dnfformula = SoleLogics.LeftmostDisjunctiveForm(map(d->SoleData.scalar_simplification(d; force_scalar_range_conditions=true), SoleLogics.disjuncts(dnfformula)))
+    
+    dnfformula = SoleData.scalar_simplification(dnfformula;
+        scalar_simplification_kwargs...
+    )
 
     silent || @show dnfformula
 
@@ -90,132 +110,106 @@ function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent
     #     # flip_atom = a -> SoleData.polarity(SoleData.test_operator(SoleLogics.value(a))) == false
     # )
 
-    dnfformula = SoleLogics.dnf(dnfformula; scalar_kwargs..., kwargs...)
+    dnfformula = SoleLogics.dnf(dnfformula; scalar_kwargs..., 
+    kwargs...)
 
     _patchnothing(v, d) = isnothing(v) ? d : v
-    condsortby = cond->(syntaxstring(SoleData.feature(cond)), _patchnothing(SoleData.minval(cond), -Inf), _patchnothing(SoleData.maxval(cond), Inf))
 
     for ch in SoleLogics.grandchildren(dnfformula)
-        sort!(SoleLogics.grandchildren(ch), by=lit->condsortby(SoleLogics.value(SoleLogics.atom(lit))))
+        sort!(SoleLogics.grandchildren(ch), by=lit->SoleData._scalarcondition_sortby(SoleLogics.value(SoleLogics.atom(lit))))
     end
     silent || @show dnfformula
 
     # Extract domains
     conditions = unique(map(SoleLogics.value, atoms(dnfformula)))
     features = unique(SoleData.feature.(conditions))
+    sort!(features, by=syntaxstring)
     # nnbinary_vars =div(length(setdiff(_duals, conditions)), 2)
-    sort!(conditions, by=condsortby)
-    original_conditions = conditions
-    println(SoleLogics.displaysyntaxvector(original_conditions))
-    conditions = begin
-        newconds = SoleData.AbstractCondition[]
-        for feat in features
-            conds = filter(c->feature(c) == feat, conditions)
-            # @show syntaxstring.(conds)
-            minextremes = [(true, (SoleData.minval(cond), !SoleData.minincluded(cond))) for cond in conds]
-            maxextremes = [(false, (SoleData.maxval(cond), SoleData.maxincluded(cond))) for cond in conds]
-            extremes = [minextremes..., maxextremes...]
-            sort!(extremes, by=((ismin, (mv, mi)),)->(_patchnothing(mv, ismin ? -Inf : Inf), mi))
-            extremes = map(last, extremes)
-            extremes = unique(extremes)
-            @show extremes
-            for (minextreme,maxextreme) in zip(extremes[1:end-1], extremes[2:end])
-                # @show maxextreme
-                cond = SoleData.RangeScalarCondition(feat, minextreme[1], maxextreme[1], !minextreme[2], maxextreme[2])
-                push!(newconds, cond)
-            end
-        end
-        # @show syntaxstring.(newconds)
-        newconds
-    end
-    @assert length(setdiff(original_conditions, conditions)) == 0 "$(setdiff(original_conditions, conditions))"
-    # readline()
-    conditions = begin
-        SoleData.hasdual.(conditions)
-        newconditions = similar(conditions, (0,))
-        for cond in conditions
-            if !SoleData.hasdual(cond) || !(SoleData.dual(cond) in newconditions)
-                push!(newconditions, cond)
-            end
-        end
-        # conditions = [condition for condition in conditions if !(condition in _duals)]
-        newconditions
+    sort!(conditions, by=SoleData._scalarcondition_sortby)
+    silent || println(SoleLogics.displaysyntaxvector(features))
+    silent || println(SoleLogics.displaysyntaxvector(conditions))
+    if use_scalar_range_conditions
+        original_conditions = conditions
+        silent || println(SoleLogics.displaysyntaxvector(conditions))
+        conditions = SoleData.scalartiling(conditions, features)
+        @assert length(setdiff(original_conditions, conditions)) == 0 "$(SoleLogics.displaysyntaxvector(setdiff(original_conditions, conditions)))"
     end
     # readline()
-    sort!(conditions, by=cond->(syntaxstring(SoleData.feature(cond)), _patchnothing(SoleData.minval(cond), -Inf), _patchnothing(SoleData.maxval(cond), Inf)))
-    # @show length(conditions)
-    # @show syntaxstring.(conditions)
-
-    println(SoleLogics.displaysyntaxvector(conditions))
-    feat_nvars = []
-    varlabelss = []
-    for feat in features
+    conditions = SoleData.removeduals(conditions)
+    silent || println(SoleLogics.displaysyntaxvector(conditions))
+
+    # For each feature, derive the conditions, and their names.
+    feat_condindxss, feat_conds, feat_condnames = zip(map(features) do feat
+        feat_condindxs = findall(c->feature(c) == feat, conditions)
         conds = filter(c->feature(c) == feat, conditions)
-        push!(feat_nvars, length(conds))
-        varlabels = _removewhitespaces.(syntaxstring.(conds))
-        push!(varlabelss, varlabels)
-    end
+        condname = _removewhitespaces.(syntaxstring.(conds))
+        (feat_condindxs, conds, condname)
+    end...)
 
-    @show syntaxstring.(conditions)
-    @show feat_nvars
-    # @show varlabelss
+    feat_nconds = length.(feat_conds)
     
-    cond_idxss = []
-    includes = []
-    excludes = []
-    for feat in features
-        cond_idxs = findall(c->feature(c) == feat, conditions)
-        push!(cond_idxss, cond_idxs)
-        push!(includes, [SoleData.includes(conditions[cond_i], conditions[cond_j]) for cond_i in cond_idxs, cond_j in cond_idxs])
-        push!(excludes, [SoleData.excludes(conditions[cond_j], conditions[cond_i]) for cond_i in cond_idxs, cond_j in cond_idxs])
+    silent || @show feat_nconds
+    silent || @show feat_condnames
+    
+    # Derive inclusions and exclusions between conditions
+    includes, excludes = [], []
+    for (i,feat_condindxs) in enumerate(feat_condindxss)
+        # silent || @show feat_condnames[i]
+        this_includes = [SoleData.includes(conditions[cond_i], conditions[cond_j]) for cond_i in feat_condindxs, cond_j in feat_condindxs]
+        this_excludes = [SoleData.excludes(conditions[cond_j], conditions[cond_i]) for cond_i in feat_condindxs, cond_j in feat_condindxs]
+        # println(this_includes)
+        # println(this_excludes)
+        push!(includes, this_includes)
+        push!(excludes, this_excludes)
     end
 
-    # @show ilb_str
+    # silent || @show ilb_str
     # Generate PLA header
     pla_header = []
     if encoding == :multivariate
-        num_binary_vars = sum(feat_nvars .== 1)
-        num_nonbinary_vars = sum(feat_nvars .> 1) + 1
-        @show feat_nvars .== 1
-        @show num_binary_vars
-        @show num_nonbinary_vars
+        @warn "encoding = :multivariate is untested."
+        num_binary_vars = sum(feat_nconds .== 1)
+        num_nonbinary_vars = sum(feat_nconds .> 1) + 1
+        silent || @show feat_nconds .== 1
+        silent || @show num_binary_vars
+        silent || @show num_nonbinary_vars
         num_vars = num_binary_vars + num_nonbinary_vars
-        push!(pla_header, ".mv $(num_vars) $(num_binary_vars) $(join(feat_nvars[feat_nvars .> 1], " ")) 1")
+        push!(pla_header, ".mv $(num_vars) $(num_binary_vars) $(join(feat_nconds[feat_nconds .> 1], " ")) 1")
         if num_binary_vars > 0
-            ilb_str = join(vcat(varlabelss[feat_nvars .== 1]...), " ")
+            ilb_str = join(vcat(feat_condnames[feat_nconds .== 1]...), " ")
             push!(pla_header, ".ilb " * ilb_str)  # Input variable labels
         end
-        for i_var in 1:length(feat_nvars[feat_nvars .> 1])
-            if feat_nvars[feat_nvars .> 1][i_var] > 1
-                this_ilb_str = join(varlabelss[feat_nvars .> 1][i_var], " ")
+        for i_var in 1:length(feat_nconds[feat_nconds .> 1])
+            if feat_nconds[feat_nconds .> 1][i_var] > 1
+                this_ilb_str = join(feat_condnames[feat_nconds .> 1][i_var], " ")
                 push!(pla_header, ".label var=$(num_binary_vars+i_var-1) $(this_ilb_str)")
             end
         end
     else
         num_outputs = 1
         num_vars = length(conditions)
-        ilb_str = join(vcat(varlabelss...), " ")
+        ilb_str = join(vcat(feat_condnames...), " ")
         push!(pla_header, ".i $(num_vars)")
         push!(pla_header, ".o $(num_outputs)")
         push!(pla_header, ".ilb " * ilb_str)  # Input variable labels
         push!(pla_header, ".ob formula_output")
     end
 
-    @show pla_header
+    silent || @show pla_header
 
     # Generate ON-set rows for each disjunct
-    end_idxs = cumsum(feat_nvars)
-    @show feat_nvars
-    feat_varidxs = [(startidx:endidx) for (startidx,endidx) in zip([1, (end_idxs.+1)...],end_idxs)]
-    @show feat_varidxs
+    end_idxs = cumsum(feat_nconds)
+    silent || @show feat_nconds
+    feat_varidxs = [(startidx:endidx) for (startidx,endidx) in zip([1, (end_idxs.+1)...], end_idxs)]
+    silent || @show feat_varidxs
     pla_onset_rows = []
     for disjunct in SoleLogics.disjuncts(dnfformula)
-        row = encode_disjunct(disjunct, features, conditions, includes, excludes, cond_idxss)
+        row = encode_disjunct(disjunct, features, conditions, includes, excludes, feat_condindxss)
         if encoding == :multivariate
             # Binary variables first
-            @show row
-            binary_variable_idxs = findall(feat_nvar->feat_nvar == 1, feat_nvars)
-            nonbinary_variable_idxs = findall(feat_nvar->feat_nvar > 1, feat_nvars)
+            silent || @show row
+            binary_variable_idxs = findall(feat_nvar->feat_nvar == 1, feat_nconds)
+            nonbinary_variable_idxs = findall(feat_nvar->feat_nvar > 1, feat_nconds)
             row = vcat(
                 [row[feat_varidxs[i_var]] for i_var in binary_variable_idxs]...,
                 (num_binary_vars > 0 ? ["|"] : [])...,
@@ -233,13 +227,13 @@ function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent
     # @assert !(dc_set && encoding == :multivariate)
     # if dc_set
     #     for feat in features
-    #         cond_idxs = findall(c->feature(c) == feat, conditions)
-    #         # cond_idxs = collect(eachindex(conditions))
+    #         feat_condindxs = findall(c->feature(c) == feat, conditions)
+    #         # feat_condindxs = collect(eachindex(conditions))
     #         # cond_mask = map((c)->feature(c) == feat, conditions)
-    #         includes = [SoleData.includes(conditions[cond_i], conditions[cond_j]) for cond_i in cond_idxs, cond_j in cond_idxs]
-    #         excludes = [SoleData.excludes(conditions[cond_i], conditions[cond_j]) for cond_i in cond_idxs, cond_j in cond_idxs]
-    #         for (i,cond_i) in enumerate(cond_idxs)
-    #             for (j,cond_j) in enumerate(cond_idxs)
+    #         includes = [SoleData.includes(conditions[cond_i], conditions[cond_j]) for cond_i in feat_condindxs, cond_j in feat_condindxs]
+    #         excludes = [SoleData.excludes(conditions[cond_i], conditions[cond_j]) for cond_i in feat_condindxs, cond_j in feat_condindxs]
+    #         for (i,cond_i) in enumerate(feat_condindxs)
+    #             for (j,cond_j) in enumerate(feat_condindxs)
     #                 if includes[i, j]
     #                     println("$(syntaxstring(conditions[cond_i])) -> $(syntaxstring(conditions[cond_j]))")
     #                 end
@@ -250,14 +244,14 @@ function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent
     #         end
     #         print(includes)
     #         print(excludes)
-    #         for (i,cond_i) in enumerate(cond_idxs)
+    #         for (i,cond_i) in enumerate(feat_condindxs)
     #             row = fill("-", length(conditions))
     #             row[cond_i] = "1"
-    #             for (j,cond_j) in enumerate(cond_idxs)
+    #             for (j,cond_j) in enumerate(feat_condindxs)
     #                 if includes[j, i]
     #                     row[cond_j] = "1"
     #                 elseif excludes[j, i]
-    #                     row[cond_j] = "0"
+    #                     row[cond_j] = NEG
     #                 end
     #             end
     #             push!(pla_dcset_rows, "$(join(row, "")) -") # Append "-" for the DC-set output
@@ -276,10 +270,23 @@ function _formula_to_pla(syntaxtree::SoleLogics.Formula, dc_set = false, silent
         ".e"
     ]
     c = strip(join(pla_content, "\n"))
-    return c, nothing, conditions
+    return c, (nothing, conditions), (
+        encoding = encoding,
+        use_scalar_range_conditions = use_scalar_range_conditions,
+        kwargs...
+    )
 end
 
-function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = nothing)
+function _pla_to_formula(
+    pla::AbstractString,
+    silent = true,
+    ilb_str = nothing,
+    conditions = nothing;
+    conditionstype = SoleData.ScalarCondition,
+    featuretype = SoleData.VariableValue,
+    featvaltype = nothing,
+    kwargs...
+)
     # @show ilb_str, conditions
     # Split the PLA into lines and parse key components
     lines = split(pla, '\n')
@@ -289,11 +296,11 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
 
     multivalued_info = Dict()  # To store multi-valued variable metadata
     total_vars, nbinary_vars, multivalued_sizes = 0, 0, []
-    println(lines)
+    silent || println(lines)
     # Parse header and rows
     for line in lines
         line = strip(line)
-        @show line
+        silent || @show line
         parts = split(line)
 
         isempty(parts) && continue
@@ -301,6 +308,7 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
         cmd, args = parts[1], parts[2:end]
 
         if cmd == ".mv"
+            @warn "PLA: Multivalued variables not tested."
             total_vars, nbinary_vars = parse(Int, args[1]), parse(Int, args[2])
             multivalued_sizes = parse.(Int, args[3:end])
         elseif cmd == ".label"
@@ -317,7 +325,7 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
         elseif cmd == ".ilb"  # Input labels
             this_ilb_str = join(args, " ")
             if !isnothing(ilb_str)
-                @assert ilb_str == this_ilb_str "Mismatch between given ilb_str and parsed .ilb."
+                @assert ilb_str == this_ilb_str "Mismatch between given ilb_str and parsed .ilb.\n$(ilb_str)\n$(this_ilb_str)."
             end
             input_vars = split(this_ilb_str)  # Extract input variable labels
         elseif cmd == ".ob"  # Output labels
@@ -332,14 +340,14 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
     end
 
     # Map input variables to conditions
-    conditions_map = if !isempty(conditions)
+    conditions_map = if !isnothing(conditions)
         Dict(_removewhitespaces(syntaxstring(c)) => c for c in conditions)
     else
         Dict()
     end
 
-    @show total_vars, nbinary_vars
-    @show input_vars
+    silent || @show total_vars, nbinary_vars
+    silent || @show input_vars
     # parsed_conditions = [begin
     #     if !isnothing(conditions)
     #         idx = findfirst(c->_removewhitespaces(syntaxstring(c)) == _removewhitespaces(var_str), conditions)
@@ -349,30 +357,35 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
     #     end
     # end for var_str in input_vars]
 
-    @show multivalued_info
+    silent || @show multivalued_info
     parsed_conditions = []
     binary_idx = 1
-    parsefun = c->parsecondition(SoleData.RangeScalarCondition, c, featuretype = SoleData.VariableValue)
-    for (i, size) in enumerate([(1:nbinary_vars)..., multivalued_sizes...])
-        if i <= nbinary_vars
-            cond = (binary_idx ∈ eachindex(input_vars) ? conditions_map[input_vars[binary_idx]] : parsefun(input_vars[binary_idx]))
+    parsefun = c->parsecondition(conditionstype, c; featuretype, featvaltype)
+    silent || @show nbinary_vars, multivalued_sizes
+    for (i_var, domain_size) in enumerate([fill(2, nbinary_vars)..., multivalued_sizes...])
+        silent || @show (i_var, domain_size)
+        if i_var <= nbinary_vars
+            silent || @show i_var ∈ eachindex(input_vars)
+            silent || @show input_vars
+            silent || @show conditions_map
+            condname = i_var ∈ eachindex(input_vars) ? input_vars[i_var] : "?"
+            cond = (condname ∈ keys(conditions_map) ? conditions_map[condname] : parsefun(condname))
             push!(parsed_conditions, cond)
-            binary_idx += 1
         else
             # Multi-valued conditions are stored as a group
-            condnames = (haskey(multivalued_info, i) ? multivalued_info[i] : [])
+            condnames = (haskey(multivalued_info, i_var) ? multivalued_info[i_var] : [])
             conds = map(parsefun, condnames)
             push!(parsed_conditions, conds)
         end
     end
 
-    @show syntaxstring.(parsed_conditions)
+    silent || @show syntaxstring.(parsed_conditions)
 
     # Process rows to build the formula
     disjuncts = []
     for row in rows
         parts = split(row, r" |\|")
-        @show parts
+        silent || @show parts
         binary_part = parts[1]
 
         if (total_vars == nbinary_vars)
@@ -387,12 +400,16 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
         # Process binary variables
         # Convert row values back into parsed_conditions
         for (idx, value) in enumerate(binary_part)
-            @show value            
+            # @show value            
             cond = parsed_conditions[idx]
             if value == '1'
                 push!(conjuncts, Literal(true, Atom(cond)))
             elseif value == '0'
                 push!(conjuncts, Literal(false, Atom(cond)))
+            elseif value == '-'
+                nothing
+            else
+                error("Unexpected truth value: '$(value)'.")
             end
         end
         
@@ -417,7 +434,10 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
 
     # Combine disjuncts into a disjunctive form
     φ = if !isempty(disjuncts)
-        map!(d->SoleData.scalar_simplification(d; force_scalar_range_conditions=false), disjuncts, disjuncts)
+        map!(d->SoleData.scalar_simplification(d;
+            force_scalar_range_conditions=false,
+            allow_scalar_range_conditions=false,
+        ), disjuncts, disjuncts)
         return SL.LeftmostDisjunctiveForm(disjuncts)
     else
         return ⊤  # True formula
@@ -425,7 +445,7 @@ function _pla_to_formula(pla::AbstractString, ilb_str = nothing, conditions = no
 end
 
 
-function formula_to_emacs(expr::SyntaxTree) end
+# function formula_to_emacs(expr::SyntaxTree) end
 
 
 end
diff --git a/src/scalar/conditions.jl b/src/scalar/conditions.jl
index 32da526..2c3b510 100644
--- a/src/scalar/conditions.jl
+++ b/src/scalar/conditions.jl
@@ -5,6 +5,68 @@ const DEFAULT_SCALARCOND_FEATTYPE = SoleData.VarFeature
 
 abstract type AbstractScalarCondition{FT} <: AbstractCondition{FT} end
 
+
+_patchnothing(v, d) = isnothing(v) ? d : v
+function _scalarcondition_sortby(cond)
+    (syntaxstring(SoleData.feature(cond)),
+    _patchnothing(SoleData.minval(cond), -Inf),
+    !SoleData.minincluded(cond),
+    _patchnothing(SoleData.maxval(cond), Inf),
+    SoleData.maxincluded(cond)
+    )
+end
+
+function scalartiling(conditions::Vector, features = unique(SoleData.feature.(conditions)))
+    newconds = SoleData.AbstractScalarCondition[]
+    for feat in features
+        conds = filter(c->feature(c) == feat, conditions)
+        # @show syntaxstring.(conds)
+        minextremes = [(true, (SoleData.minval(cond), !SoleData.minincluded(cond))) for cond in conds]
+        maxextremes = [(false, (SoleData.maxval(cond), SoleData.maxincluded(cond))) for cond in conds]
+        extremes = [minextremes..., maxextremes...]
+        sort!(extremes, by=((ismin, (mv, mi)),)->(_patchnothing(mv, ismin ? -Inf : Inf), mi))
+        extremes = map(last, extremes)
+        extremes = unique(extremes)
+        @show extremes
+        for (minextreme,maxextreme) in zip(extremes[1:end-1], extremes[2:end])
+            # @show maxextreme
+            cond = SoleData.RangeScalarCondition(feat, minextreme[1], maxextreme[1], !minextreme[2], maxextreme[2])
+            push!(newconds, cond)
+        end
+    end
+    # @show syntaxstring.(newconds)
+    newconds
+end
+
+function tointervalset(a::AbstractScalarCondition)
+    f1 = minincluded(a) ? :closed : :open
+    f2 = maxincluded(a) ? :closed : :open
+    IntervalSetsWrap.Interval{f1,f2}(isnothing(minval(a)) ? -Inf : minval(a), isnothing(maxval(a)) ? Inf : maxval(a))
+end
+
+function includes(a::AbstractScalarCondition, b::AbstractScalarCondition)
+    (feature(a) == feature(b)) || return false
+    return issubset(tointervalset(b),tointervalset(a))
+end
+
+function excludes(a::AbstractScalarCondition, b::AbstractScalarCondition)
+    (feature(a) == feature(b)) || return false
+    # @show tointervalset(a)
+    # @show tointervalset(b)
+    return isdisjoint(tointervalset(a),tointervalset(b))
+end
+
+function removeduals(values::Vector)
+    newvalues = similar(values, (0,))
+    for cond in values
+        if !SoleData.hasdual(cond) || !(SoleData.dual(cond) in newvalues)
+            push!(newvalues, cond)
+        end
+    end
+    newvalues
+end
+
+
 # TODO ScalarMetaCondition is more like... an Alphabet, than a Condition.
 """
     struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractScalarCondition{FT}
@@ -184,6 +246,51 @@ test_operator(c::ScalarCondition) = test_operator(metacond(c))
 hasdual(::ScalarCondition) = true
 dual(c::ScalarCondition) = ScalarCondition(dual(metacond(c)), threshold(c))
 
+function minval(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        threshold(c)
+    elseif isnothing(pol)
+        error("Unknown minval for test_operator $(testop).")
+    else
+        pol ? threshold(c) : -Inf
+    end
+end
+function minincluded(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        true
+    elseif isnothing(pol)
+        error("Unknown minincluded for test_operator $(testop).")
+    else
+        pol ? !isstrict(testop) : true
+    end
+end
+function maxval(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        threshold(c)
+    elseif isnothing(pol)
+        error("Unknown maxval for test_operator $(testop).")
+    else
+        pol ? Inf : threshold(c)
+    end
+end
+function maxincluded(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        true
+    elseif isnothing(pol)
+        error("Unknown maxincluded for test_operator $(testop).")
+    else
+        pol ? true : !isstrict(test_operator(c))
+    end
+end
+
 function checkcondition(c::ScalarCondition, args...; kwargs...)
     apply_test_operator(test_operator(c), featvalue(feature(c), args...; kwargs...), threshold(c))
 end
@@ -253,9 +360,9 @@ function _parsecondition(
     expr::AbstractString;
     kwargs...
 ) where {U,FT<:AbstractFeature,C<:ScalarCondition{U,FT}}
-    r = Regex("^\\s*(\\S+)\\s*([^\\s\\d]+)\\s*(\\S+)\\s*\$")
+    r = Regex("^\\s*([^\\s><!=≥≤]+)\\s*([^\\s\\d]+)\\s*(\\S+)\\s*\$")
     slices = match(r, expr)
-    
+
     if isnothing(slices) || length(slices) != 3
         throw(ArgumentError("Could not parse ScalarCondition from " *
             "expression $(repr(expr)). Regex slices = $(slices)"))
@@ -264,6 +371,7 @@ function _parsecondition(
     slices = string.(slices)
 
     feature = parsefeature(FT, slices[1]; featvaltype = U, kwargs...)
+    # @show slices
     test_operator = eval(Meta.parse(slices[2]))
     threshold = eval(Meta.parse(slices[3]))
 
@@ -547,6 +655,13 @@ function hasdual(c::RangeScalarCondition)
     )
 end
 
+function _rangescalarcond_to_scalarconds_in_conjunction(cond)
+    conds = []
+    !isnothing(SoleData.minval(cond)) && push!(conds, ScalarCondition(feature(cond), _isgreater_test_operator(cond), SoleData.minval(cond)))
+    !isnothing(SoleData.maxval(cond)) && push!(conds, ScalarCondition(feature(cond), _isless_test_operator(cond), SoleData.maxval(cond)))
+    conds
+end
+
 module IntervalSetsWrap
 using IntervalSets: Interval
 end
@@ -567,29 +682,6 @@ end
 #     return aismin && !bismin
 # end
 
-function tointervalset(a::RangeScalarCondition)
-    f1 = minincluded(a) ? :closed : :open
-    f2 = maxincluded(a) ? :closed : :open
-    IntervalSetsWrap.Interval{f1,f2}(isnothing(minval(a)) ? -Inf : minval(a), isnothing(maxval(a)) ? Inf : maxval(a))
-end
-
-function includes(a::RangeScalarCondition, b::RangeScalarCondition)
-    (feature(a) == feature(b)) || return false
-    return issubset(tointervalset(b),tointervalset(a))
-    # return 
-    #         (minincluded(a) ? (!myisless(b.minval, true, a.minval, true)) : (myisless(a.minval, true, b.minval, true) || (!(minincluded(b)) && a.minval == b.minval))) &&
-    #         (maxincluded(a) ? (!myisless(a.maxval, false, b.maxval, false)) : (myisless(a.maxval, false, b.maxval, false) || (!(maxincluded(b)) && a.maxval == b.maxval)))
-end
-
-function excludes(a::RangeScalarCondition, b::RangeScalarCondition)
-    (feature(a) == feature(b)) || return false
-    return isdisjoint(tointervalset(a),tointervalset(b))
-    # intersect = 
-    #         (minincluded(a) ? (!myisless(b.maxval, false, a.minval, true) || ((maxincluded(b)) && a.minval == b.maxval)) : (myisless(a.minval, true, b.maxval, false))) ||
-    #         (maxincluded(a) ? (!myisless(a.maxval, false, b.minval, true) || ((minincluded(b)) && a.maxval == b.minval)) : (myisless(a.maxval, false, b.minval, true)))
-    # return !intersect
-end
-
 @inline function honors_minval(c::RangeScalarCondition, featval)
     isnothing(c.minval) || apply_test_operator(_isgreater_test_operator(c), featval, c.minval)
 end
@@ -650,7 +742,7 @@ function _parsecondition(
     # r = Regex("^\\s*(\\S+)\\s*([^\\s\\d]+)\\s*(\\[|\\()\\s*(\\S+)\\s*,\\s*(\\S+)\\s*(\\]|\\))\\s*\$")
     slices = match(r, expr)
     if isnothing(slices) || length(slices) != 5
-        throw(ArgumentError("Could not parse ScalarCondition from " *
+        throw(ArgumentError("Could not parse RangeScalarCondition from " *
             "expression $(repr(expr)). Regex slices = $(slices)"))
     end
 
diff --git a/src/scalar/propositional-formula-simplification.jl b/src/scalar/propositional-formula-simplification.jl
index 2008258..c5b85d8 100644
--- a/src/scalar/propositional-formula-simplification.jl
+++ b/src/scalar/propositional-formula-simplification.jl
@@ -16,22 +16,38 @@ function scalar_simplification(φ::SoleLogics.SyntaxLeaf; silent = false, kwargs
 end
 
 function scalar_simplification(φ::DNF, args...; kwargs...)
-    return map(d->scalar_simplification(d; args...), SoleLogics.disjuncts(φ)) |> LeftmostDisjunctiveForm
+    return map(d->scalar_simplification(d, args...; kwargs...), SoleLogics.disjuncts(φ)) |> LeftmostDisjunctiveForm
 end
 function scalar_simplification(φ::CNF, args...; kwargs...)
-    return map(d->scalar_simplification(d; args...), SoleLogics.conjuncts(φ)) |> LeftmostConjunctiveForm
+    return map(d->scalar_simplification(d, args...; kwargs...), SoleLogics.conjuncts(φ)) |> LeftmostConjunctiveForm
 end
 function scalar_simplification(
     φ::Union{LeftmostConjunctiveForm,LeftmostDisjunctiveForm};
     silent = false,
     force_scalar_range_conditions = false,
-    force_no_scalar_range_conditions = false,
+    # force_no_scalar_range_conditions = false,
     allow_scalar_range_conditions = true,
-    kwargs...,
 )
     # @show φ
     # @show typeof.(SoleLogics.grandchildren(φ))
     # @show all(c->c isa Atom{<:ScalarCondition}, SoleLogics.grandchildren(φ))
+    
+    φ = LeftmostLinearForm(SoleLogics.connective(φ), map(ch->begin
+        if ch isa Atom
+            ch
+        elseif ch isa Literal
+            if SoleLogics.ispos(ch)
+                atom(ch)
+            elseif SoleLogics.hasdual(atom(ch))
+                SoleLogics.dual(atom(ch))
+            else
+                ch
+            end
+        else
+            ch
+        end
+    end, SoleLogics.grandchildren(φ)))
+    
     if !all(c->c isa Atom{<:Union{ScalarCondition,RangeScalarCondition}}, SoleLogics.grandchildren(φ))
     # if (!all(c->c isa Atom{<:ScalarCondition}, SoleLogics.grandchildren(φ)))
         !silent && println("Cannot perform scalar simplification on linear form:\n$(syntaxstring(φ))\n on" *
@@ -69,14 +85,27 @@ function scalar_simplification(
     ch = collect(Iterators.flatten([begin
             conds = scalar_conditions[bitmask]
 
+            conds = [if cond isa ScalarCondition && (test_operator(cond) == (==))
+                        RangeScalarCondition(
+                            SoleData.feature(cond),
+                            SoleData.minval(cond),
+                            SoleData.maxval(cond),
+                            SoleData.minincluded(cond),
+                            SoleData.maxincluded(cond),
+                        )
+                    else
+                        cond
+                    end for cond in conds]
+
             conds = Iterators.flatten([
                 if cond isa ScalarCondition
                     [cond]
                 elseif cond isa RangeScalarCondition
-                    conds = []
-                    !isnothing(SoleData.minval(cond)) && push!(conds, ScalarCondition(feat, _isgreater_test_operator(cond), SoleData.minval(cond)))
-                    !isnothing(SoleData.maxval(cond)) && push!(conds, ScalarCondition(feat, _isless_test_operator(cond), SoleData.maxval(cond)))
-                    conds
+                    if conn_polarity
+                        conds = _rangescalarcond_to_scalarconds_in_conjunction(cond)
+                    else
+                        error("Cannot convert RangeScalarCondition to ScalarCondition: $(cond).")
+                    end
                 else
                     error("Unexpected condition: $(cond)")
                 end for cond in conds])
diff --git a/src/scalar/scalarlogiset.jl b/src/scalar/scalarlogiset.jl
index 61ba8be..511edd1 100644
--- a/src/scalar/scalarlogiset.jl
+++ b/src/scalar/scalarlogiset.jl
@@ -438,7 +438,7 @@ function naturalconditions(
     metaconditions = ScalarMetaCondition[]
 
     mixed_conditions = vcat(unpackcondition.(mixed_conditions)...)
-    @show mixed_conditions
+    # @show mixed_conditions
     readymade_conditions          = filter(x->
         isa(x, ScalarMetaCondition),
         mixed_conditions,
diff --git a/test/pla.jl b/test/pla.jl
index a8ea6fe..376ae16 100644
--- a/test/pla.jl
+++ b/test/pla.jl
@@ -4,14 +4,40 @@ using SoleData
 using SoleData: PLA
 using SoleLogics
 
+function cleanlines(str::AbstractString)
+  join(filter(!isempty, split(str, "\n")), "\n")
+end
+
 formula0 = @scalarformula ((V1 > 10) ∧ (V2 < 0) ∧ (V2 < 0) ∧ (V2 <= 0)) ∨ ((V1 <= 0) ∧ ((V1 <= 3)) ∧ (V2 == 2))
-@test_broken PLA._formula_to_pla(formula0)
+@test cleanlines(PLA._formula_to_pla(formula0)[1]) == cleanlines("""
+.i 4
+.o 1
+.ilb V1≤0 V1>10 V2<0 V2∈[2,2]
+.ob formula_output
+
+.p 2
+1001 1
+0110 1
+.e
+""")
 
 formula0 = @scalarformula ((V1 > 10) ∧ (V2 < 0) ∧ (V2 < 0) ∧ (V2 <= 0)) ∨ ((V1 <= 0) ∧ ((V1 <= 3)) ∧ (V2 >= 2))
-SoleData.scalar_simplification(dnf(formula0, Atom))
-PLA._formula_to_pla(formula0, true)[1] |> println
+@test_nowarn SoleData.scalar_simplification(dnf(formula0, Atom))
+@test_nowarn PLA._formula_to_pla(formula0, true)[1] |> println
+@test cleanlines(PLA._formula_to_pla(formula0, true)[1]) == cleanlines("""
+.i 4
+.o 1
+.ilb V1≤0 V1>10 V2<0 V2≥2
+.ob formula_output
 
-formula01 = tree(PLA._pla_to_formula(PLA._formula_to_pla(formula0)...))
+.p 2
+1001 1
+0110 1
+.e
+""")
+
+f, args, kwargs = PLA._formula_to_pla(formula0)
+formula01 = tree(PLA._pla_to_formula(f, true, args...; kwargs...))
 formula0_min = SoleData.espresso_minimize(formula0)
 
 
@@ -37,14 +63,17 @@ println(formula0); println(formula0_min);
 (V4 < 0.7 && V2 < 2.6500000000000004 && V3 < 5.0 && V3 ≥ 4.95) ||
 (V4 < 0.7 && V2 ≥ 2.6500000000000004 && V3 < 4.95) ||
 (V4 < 0.7 && V2 < 2.6500000000000004 && V3 < 4.95)
+# φ_min = SoleData.espresso_minimize(φ, false; encoding = :univariate)
 φ_min = SoleData.espresso_minimize(φ; encoding = :univariate)
-println(φ); println(φ_min);
-@test syntaxstring(φ_min) == syntaxstring(@scalarformula (V4 < 0.7))
+φ_min = SoleData.espresso_minimize(φ, false, "exact"; encoding = :univariate)
 
-φ_min = SoleData.espresso_minimize(φ, false; encoding = :multivariate)
 println(φ); println(φ_min);
 @test syntaxstring(φ_min) == syntaxstring(@scalarformula (V4 < 0.7))
 
+# φ_min = SoleData.espresso_minimize(φ, false; encoding = :multivariate)
+# println(φ); println(φ_min);
+# @test syntaxstring(φ_min) == syntaxstring(@scalarformula (V4 < 0.7))
+
 
 φ = @scalarformula (V4 ≥ 1.7000000000000002) ∧ (V2 ≥ 2.6500000000000004) ∧ (V3 ≥ 5.0) ∨
 (V4 ≥ 1.7000000000000002) ∧ (V2 < 2.6500000000000004) ∧ (V3 ≥ 5.0) ∨
@@ -52,10 +81,15 @@ println(φ); println(φ_min);
 (V4 ≥ 1.7000000000000002) ∧ (V2 < 2.6500000000000004) ∧ (V3 < 5.0) ∧ (V3 ≥ 4.95) ∨
 (V4 ≥ 1.7000000000000002) ∧ (V2 ≥ 2.6500000000000004) ∧ (V3 < 4.95) ∨
 (V4 ≥ 1.7000000000000002) ∧ (V2 < 2.6500000000000004) ∧ (V3 < 4.95)
-φ_min = SoleData.espresso_minimize(φ, false; encoding = :multivariate)
+φ_min = SoleData.espresso_minimize(φ)
+# φ_min = SoleData.espresso_minimize(φ, false)
 println(φ); println(φ_min);
 @test syntaxstring(φ_min) == syntaxstring(@scalarformula (V4 ≥ 1.7000000000000002))
 
+# φ_min = SoleData.espresso_minimize(φ, false; encoding = :multivariate)
+# println(φ); println(φ_min);
+# @test syntaxstring(φ_min) == syntaxstring(@scalarformula (V4 ≥ 1.7000000000000002))
+
 
 # Looks okay?
 
@@ -71,6 +105,55 @@ pla = """
 """
 
 @test_nowarn formula = PLA._pla_to_formula(pla)
+@test_broken @test_nowarn formula = PLA._pla_to_formula(""".i 5
+.o 1
+.ilb V1>10 V2<0 V2<=2 V3>10 V4!=10
+.p 2
+01--0 1
+01-1- 1
+.e
+""")
+
+@test_nowarn formula = PLA._pla_to_formula(""".i 5
+.o 1
+.ilb V1>10 V2<0 V2<=2 V3>10 V4>=10
+.p 2
+01--0 1
+01-1- 1
+.e
+""", featvaltype = Float32)
+
+
+
+formula = @test_nowarn PLA._pla_to_formula(""".i 5
+.o 1
+.ilb V1>10 V2<0 V2<=2 V3>10 V4>=10
+01010 1
+01110 1
+01011 1
+01111 1
+01010 1
+01000 1
+01100 1
+.e
+""", featvaltype = Float32)
+
+
+@test cleanlines(PLA._formula_to_pla(formula)[1]) == cleanlines("""
+.i 4
+.o 1
+.ilb V1≤10 V2<0 V3≤10 V4<10
+.ob formula_output
+
+.p 6
+1-01 1
+1101 1
+1-00 1
+1100 1
+1-11 1
+1111 1
+.e
+""")
 
 
 pla = """.i 2
@@ -81,13 +164,15 @@ pla = """.i 2
 0-1 1
 .e"""
 
-@test PLA._formula_to_pla(@scalarformula ((V1 <= 0)) ∨ ((V1 <= 0) ∧ (V2 <= 0)))[1] == """.i 2
+@test cleanlines(PLA._formula_to_pla(@scalarformula ((V1 <= 0)) ∨ ((V1 <= 0) ∧ (V2 <= 0)))[1]) == cleanlines("""
+.i 2
 .o 1
-.ilb V1>0 V2>0
+.ilb V1≤0 V2≤0
 .ob formula_output
-0- 1
-00 1
-.e"""
+11 1
+1- 1
+.e
+""")
 
 formula = PLA._pla_to_formula(""".i 2
 .o 1
@@ -101,3 +186,10 @@ PLA._formula_to_pla(@scalarformula ((V1 <= 0)) ∨ (¬(V1 <= 0) ∧ (V2 <= 0)))
 
 formula = PLA._pla_to_formula(pla)
 @test isa(formula, SoleLogics.LeftmostDisjunctiveForm)
+
+
+# Espresso minimization
+
+@test_nowarn SoleData.espresso_minimize(@scalarformula ((V1 <= 0)) ∨ ((V1 <= 0) ∧ (V2 <= 0)))
+
+@test syntaxstring(SoleData.espresso_minimize(@scalarformula ((V1 <= 0)) ∨ ((V1 <= 0) ∧ (V2 <= 0)))) == "(V1 ≤ 0)"