diff --git a/README.md b/README.md
index 417f8e88..d9ebef52 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,7 @@ from pddl.parser.problem import ProblemParser
 from pylogics.parsers import parse_pltl
 from plan4past.compiler import Compiler
 
-formula = "on_b_a & O(ontable_c)"
+formula = '"on b a" & O("ontable c")'
 domain_parser = DomainParser()
 problem_parser = ProblemParser()
 
diff --git a/plan4past/__main__.py b/plan4past/__main__.py
index 543603c0..c7c12c9c 100644
--- a/plan4past/__main__.py
+++ b/plan4past/__main__.py
@@ -34,7 +34,6 @@
 from pylogics.syntax.base import Formula
 
 from plan4past.compiler import Compiler
-from plan4past.utils.mapping_parser import mapping_parser
 
 DEFAULT_NEW_DOMAIN_FILENAME: str = "new-domain.pddl"
 DEFAULT_NEW_PROBLEM_FILENAME: str = "new-problem.pddl"
@@ -62,13 +61,6 @@
     help="The path to the PPLTL goal formula.",
     type=click.Path(exists=True, readable=True),
 )
-@click.option(
-    "-m",
-    "--mapping",
-    help="The mapping file.",
-    type=click.Path(exists=True, readable=True),
-    default=None,
-)
 @click.option(
     "-od",
     "--out-domain",
@@ -83,20 +75,14 @@
     help="Path to PDDL file to store the new problem.",
     type=click.Path(dir_okay=False),
 )
-def cli(domain, problem, goal_inline, goal_file, mapping, out_domain, out_problem):
+def cli(domain, problem, goal_inline, goal_file, out_domain, out_problem):
     """Plan4Past: Planning for Pure-Past Temporally Extended Goals."""
     goal = _get_goal(goal_inline, goal_file)
 
     in_domain, in_problem, formula = _parse_instance(domain, problem, goal)
 
-    var_map = (
-        mapping_parser(Path(mapping).read_text(encoding="utf-8"), formula)
-        if mapping
-        else None
-    )
-
     compiled_domain, compiled_problem = _compile_instance(
-        in_domain, in_problem, formula, var_map
+        in_domain, in_problem, formula
     )
 
     try:
@@ -137,9 +123,9 @@ def _parse_instance(in_domain, in_problem, goal) -> Tuple[Domain, Problem, Formu
     return domain, problem, formula
 
 
-def _compile_instance(domain, problem, formula, mapping) -> Tuple[Domain, Problem]:
+def _compile_instance(domain, problem, formula) -> Tuple[Domain, Problem]:
     """Compile the PDDL domain and problem files and the PPLTL goal formula."""
-    compiler = Compiler(domain, problem, formula, mapping)
+    compiler = Compiler(domain, problem, formula)
     compiler.compile()
     compiled_domain, compiled_problem = compiler.result
 
diff --git a/plan4past/compiler.py b/plan4past/compiler.py
index 6fec28b4..e3bef8a8 100644
--- a/plan4past/compiler.py
+++ b/plan4past/compiler.py
@@ -21,10 +21,9 @@
 #
 
 """Compiler from PDDL Domain and PPLTL into a new PDDL domain."""
-from typing import AbstractSet, Dict, Optional, Set, Tuple
+from typing import AbstractSet, Optional, Set, Tuple
 
 from pddl.core import Action, Domain, Problem, Requirements
-from pddl.logic import Constant
 from pddl.logic.base import And, Not
 from pddl.logic.effects import AndEffect, When
 from pddl.logic.predicates import DerivedPredicate, Predicate
@@ -35,7 +34,6 @@
 from plan4past.helpers.utils import (
     add_val_prefix,
     check_,
-    default_mapping,
     remove_before_prefix,
     replace_symbols,
 )
@@ -54,7 +52,6 @@ def __init__(
         domain: Domain,
         problem: Problem,
         formula: Formula,
-        from_atoms_to_fluent: Optional[Dict[PLTLAtomic, Predicate]] = None,
     ) -> None:
         """
         Initialize the compiler.
@@ -62,16 +59,10 @@ def __init__(
         :param domain: the domain
         :param problem: the problem
         :param formula: the formula
-        :param from_atoms_to_fluent: optional mapping from atoms to fluent
         """
         self.domain = domain
         self.problem = problem
         self.formula = rewrite(formula)
-        if from_atoms_to_fluent:
-            self.from_atoms_to_fluent = from_atoms_to_fluent
-            self.validate_mapping(domain, formula, from_atoms_to_fluent)
-        else:
-            self.from_atoms_to_fluent = default_mapping(self.formula)
 
         check_(self.formula.logic == Logic.PLTL, "only PPLTL is supported!")
 
@@ -81,29 +72,6 @@ def __init__(
 
         self._derived_predicates: Set[DerivedPredicate] = set()
 
-    @classmethod
-    def validate_mapping(
-        cls,
-        _domain: Domain,
-        _formula: Formula,
-        from_atoms_to_fluent: Dict[PLTLAtomic, Predicate],
-    ):
-        """
-        Check that the mapping is valid wrt the problem instance.
-
-        In particular:
-        - check that all the formula atoms are covered (TODO)
-        - check that all the atoms are legal wrt the formula
-        - check that the fluents are legal wrt the domain
-
-        :param _domain:
-        :param _formula:
-        :param from_atoms_to_fluent:
-        :return:
-        """
-        for _atom, fluent in from_atoms_to_fluent.items():
-            check_(all(isinstance(t, Constant) for t in fluent.terms))
-
     @property
     def result(self) -> Tuple[Domain, Problem]:
         """Get the result."""
@@ -121,9 +89,7 @@ def compile(self):
     def _compile_domain(self):
         """Compute the new domain."""
         new_predicates = predicates(self.formula).union(val_predicates(self.formula))
-        new_derived_predicates = derived_predicates(
-            self.formula, self.from_atoms_to_fluent
-        )
+        new_derived_predicates = derived_predicates(self.formula)
         new_whens = _compute_whens(self.formula)
         domain_actions = _update_domain_actions_det(self.domain.actions, new_whens)
 
@@ -167,12 +133,13 @@ def _compile_problem(self):
 
 def _compute_whens(formula: Formula) -> Set[When]:
     """Compute conditional effects for formula progression."""
+    formula_predicates = predicates(formula)
     return {
         When(Predicate(add_val_prefix(remove_before_prefix(p.name))), p)
-        for p in predicates(formula)
+        for p in formula_predicates
     }.union(
         When(Not(Predicate(add_val_prefix(remove_before_prefix(p.name)))), Not(p))
-        for p in predicates(formula)
+        for p in formula_predicates
     )
 
 
diff --git a/plan4past/helpers/utils.py b/plan4past/helpers/utils.py
index a1b47738..a76028f9 100644
--- a/plan4past/helpers/utils.py
+++ b/plan4past/helpers/utils.py
@@ -21,64 +21,63 @@
 #
 
 """Miscellanea utilities."""
-from typing import Dict
+import re
+from typing import Collection, Type
 
 from pddl.logic import Predicate, constants
-from pylogics.syntax.base import Formula
-from pylogics.syntax.pltl import Atomic as PLTLAtomic
 
-from plan4past.utils.atoms_visitor import find_atoms
+_PDDL_NAME_REGEX = "[A-Za-z][-_A-Za-z0-9]*"
+_GROUND_FLUENT_REGEX = re.compile(
+    rf"(\"({_PDDL_NAME_REGEX})( {_PDDL_NAME_REGEX})*\")|({_PDDL_NAME_REGEX})"
+)
+VAL_PREFIX = "VAL__"
+_LEFT_PAR = "LPAR__"
+_RIGHT_PAR = "__RPAR"
+Y_PREFIX = "Y__"
+_NOT = "NOT__"
+_AND = "__AND__"
+_OR = "__OR__"
+_QUOTE = "__QUOTE__"
 
 
 def add_val_prefix(name: str):
     """Add the 'prime' prefix."""
-    return "val-" + name.replace('"', "")
+    return VAL_PREFIX + name.replace('"', _QUOTE)
 
 
 def remove_before_prefix(name: str):
     """Remove the 'Y' prefix."""
     return (
-        name.replace("Y-", "")
-        if name.startswith("Y-")
-        else name.replace("Y", "", 1)
-        if name.startswith("Y")
+        name.replace(Y_PREFIX, "")
+        if name.startswith(Y_PREFIX)
+        else re.sub(f"{_RIGHT_PAR}$", "", name.replace("Y" + _LEFT_PAR, "", 1))
+        if name.startswith("Y" + _LEFT_PAR)
         else name
     )
 
 
 def remove_val_prefix(name: str):
     """Remove the 'prime' prefix."""
-    return name.replace("val-", "") if name.startswith("val-") else name
+    return name.replace(VAL_PREFIX, "") if name.startswith(VAL_PREFIX) else name
 
 
 def replace_symbols(name: str):
     """Stringify symbols."""
     return (
-        name.replace('"', "")
-        .replace("(", "")
-        .replace(")", "")
-        .replace("&", "and")
-        .replace("|", "or")
-        .replace("~", "not-")
-        .replace("!", "not-")
+        name.replace('"', _QUOTE)
+        .replace("(", _LEFT_PAR)
+        .replace(")", _RIGHT_PAR)
+        .replace("&", _AND)
+        .replace("|", _OR)
+        .replace("~", _NOT)
+        .replace("!", _NOT)
         .replace(" ", "-")
     )
 
 
-def default_mapping(formula: Formula) -> Dict[PLTLAtomic, Predicate]:
-    """Compute mapping from atoms to fluents using underscores."""
-    symbols = find_atoms(formula)
-    from_atoms_to_fluents = {}
-    for symbol in symbols:
-        name, *cons = symbol.name.split("_")
-        if cons:
-            from_atoms_to_fluents[symbol] = Predicate(name, *constants(" ".join(cons)))
-        else:
-            from_atoms_to_fluents[symbol] = Predicate(name)
-    return from_atoms_to_fluents
-
-
-def check_(condition: bool, message: str = "") -> None:
+def check_(
+    condition: bool, message: str = "", exception_cls: Type[Exception] = AssertionError
+) -> None:
     """
     User-defined assert.
 
@@ -87,4 +86,73 @@ def check_(condition: bool, message: str = "") -> None:
         https://bandit.readthedocs.io/en/1.7.5/plugins/b101_assert_used.html
     """
     if not condition:
-        raise AssertionError(message)
+        raise exception_cls(message)
+
+
+def parse_ground_fluent(symbol: str) -> Predicate:
+    """
+    Parse a ground fluent.
+
+    :param symbol: the ground fluent
+    :return: the predicate
+    """
+    match = _GROUND_FLUENT_REGEX.fullmatch(symbol)
+    if match is None:
+        raise ValueError(f"invalid PDDL symbol in formula: {symbol}")
+
+    if '"' in symbol:
+        tokens = symbol[1:-1].split(" ", 1)
+        predicate_name, cons = (
+            (tokens[0], tokens[1]) if len(tokens) > 1 else (tokens[0], "")
+        )
+        return Predicate(predicate_name, *constants(cons))
+    return Predicate(symbol)
+
+
+def _check_does_not_start_with(symbol: str, prefixes: Collection[str]) -> None:
+    """
+    Check if a symbol does not start with a given prefix.
+
+    :param symbol: the symbol
+    :param prefixes: the prefixes to check
+    """
+    for prefix in prefixes:
+        check_(
+            not symbol.startswith(prefix),
+            f"invalid symbol: symbol '{symbol}' cannot start with {prefix}",
+            exception_cls=ValueError,
+        )
+
+
+def _check_not_in(symbol: str, forbidden_substrings: Collection[str]) -> None:
+    """
+    Check if a string is not in a set of symbols.
+
+    :param symbol: the symbol
+    :param forbidden_substrings: the set of forbidden substrings
+    """
+    for s in forbidden_substrings:
+        check_(
+            s not in symbol,
+            f"invalid symbol: symbol '{symbol}' contains {s}",
+            exception_cls=ValueError,
+        )
+
+
+def validate(symbol: str) -> None:
+    """
+    Validate a symbol.
+
+    :param symbol: the symbol
+    """
+    # remove the double quotes
+    symbol_unquoted = symbol.replace('"', "")
+
+    # check if the symbol does not start with the 'val__' or the 'Y__' prefix
+    _check_does_not_start_with(symbol_unquoted, [VAL_PREFIX, Y_PREFIX])
+
+    # check if the symbol does not contain forbidden substrings
+    _check_not_in(symbol_unquoted, [_LEFT_PAR, _RIGHT_PAR, _AND, _OR, _NOT, _QUOTE])
+
+    # check if the symbol is a valid PDDL ground fluent
+    parse_ground_fluent(symbol)
diff --git a/plan4past/utils/derived_visitor.py b/plan4past/utils/derived_visitor.py
index 7988d326..fb213240 100644
--- a/plan4past/utils/derived_visitor.py
+++ b/plan4past/utils/derived_visitor.py
@@ -22,7 +22,7 @@
 
 """Derived Predicates visitor."""
 from functools import singledispatch
-from typing import Dict, Set
+from typing import Set
 
 from pddl.logic.base import And, Not, Or
 from pddl.logic.predicates import DerivedPredicate, Predicate
@@ -39,49 +39,44 @@
 )
 from pylogics.utils.to_string import to_string
 
-from plan4past.helpers.utils import add_val_prefix, replace_symbols
+from plan4past.helpers.utils import (
+    Y_PREFIX,
+    add_val_prefix,
+    parse_ground_fluent,
+    replace_symbols,
+)
 
 
 @singledispatch
-def derived_predicates(
-    formula: object, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates(formula: object) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a formula."""
     raise NotImplementedError(f"handler not implemented for object {type(formula)}")
 
 
 @derived_predicates.register
-def derived_predicates_true(
-    _formula: PropositionalTrue, _atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_true(_formula: PropositionalTrue) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a true formula."""
     val = Predicate(add_val_prefix("true"))
     return {DerivedPredicate(val, And())}
 
 
 @derived_predicates.register
-def derived_predicates_false(
-    _formula: PropositionalFalse, _atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_false(_formula: PropositionalFalse) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a false formula."""
     val = Predicate(add_val_prefix("false"))
     return {DerivedPredicate(val, Or())}
 
 
 @derived_predicates.register
-def derived_predicates_atomic(
-    formula: PLTLAtomic, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_atomic(formula: PLTLAtomic) -> Set[DerivedPredicate]:
     """Compute the derived predicate for an atomic formula."""
-    val = Predicate(add_val_prefix(formula.name))
-    condition = atoms_to_fluents[formula]
+    val = Predicate(add_val_prefix(replace_symbols(formula.name)))
+    condition = parse_ground_fluent(formula.name)
     return {DerivedPredicate(val, condition)}
 
 
 @derived_predicates.register
-def derived_predicates_and(
-    formula: PLTLAnd, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_and(formula: PLTLAnd) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a PPLTL And formula."""
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
@@ -90,14 +85,12 @@ def derived_predicates_and(
         for op in formula.operands
     ]
     condition = And(*val_ops)
-    der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands]
+    der_pred_ops = [derived_predicates(op) for op in formula.operands]
     return {DerivedPredicate(val, condition)}.union(*der_pred_ops)
 
 
 @derived_predicates.register
-def derived_predicates_or(
-    formula: PLTLOr, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_or(formula: PLTLOr) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a PPLTL Or formula."""
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
@@ -106,67 +99,59 @@ def derived_predicates_or(
         for op in formula.operands
     ]
     condition = Or(*val_ops)
-    der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands]
+    der_pred_ops = [derived_predicates(op) for op in formula.operands]
     return {DerivedPredicate(val, condition)}.union(*der_pred_ops)
 
 
 @derived_predicates.register
-def derived_predicates_not(
-    formula: PLTLNot, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_not(formula: PLTLNot) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a PPLTL Not formula."""
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
     condition = Not(
         Predicate(add_val_prefix(replace_symbols(to_string(formula.argument))))
     )
-    der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents)
+    der_pred_arg = derived_predicates(formula.argument)
     return {DerivedPredicate(val, condition)}.union(der_pred_arg)
 
 
 @derived_predicates.register
-def derived_predicates_before(
-    formula: Before, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_before(formula: Before) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a Before formula."""
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
     condition = Predicate(replace_symbols(to_string(formula)))
-    der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents)
+    der_pred_arg = derived_predicates(formula.argument)
     return {DerivedPredicate(val, condition)}.union(der_pred_arg)
 
 
 @derived_predicates.register
-def derived_predicates_since(
-    formula: Since, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_since(formula: Since) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a Since formula."""
     if len(formula.operands) != 2:
         head = formula.operands[0]
         tail = Since(*formula.operands[1:])
-        return derived_predicates(Since(head, tail), atoms_to_fluents)
+        return derived_predicates(Since(head, tail))
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
     op_or_1 = Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[1]))))
     op_or_2 = And(
         Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[0])))),
-        Predicate(f"Y-{replace_symbols(to_string(formula))}"),
+        Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"),
     )
     condition = Or(op_or_1, op_or_2)
-    der_pred_ops = [derived_predicates(op, atoms_to_fluents) for op in formula.operands]
+    der_pred_ops = [derived_predicates(op) for op in formula.operands]
     return {DerivedPredicate(val, condition)}.union(*der_pred_ops)
 
 
 @derived_predicates.register
-def derived_predicates_once(
-    formula: Once, atoms_to_fluents: Dict[PLTLAtomic, Predicate]
-) -> Set[DerivedPredicate]:
+def derived_predicates_once(formula: Once) -> Set[DerivedPredicate]:
     """Compute the derived predicate for a Once formula."""
     formula_name = to_string(formula)
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
     condition = Or(
         Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))),
-        Predicate(f"Y-{replace_symbols(to_string(formula))}"),
+        Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"),
     )
-    der_pred_arg = derived_predicates(formula.argument, atoms_to_fluents)
+    der_pred_arg = derived_predicates(formula.argument)
     return {DerivedPredicate(val, condition)}.union(der_pred_arg)
diff --git a/plan4past/utils/mapping_parser.py b/plan4past/utils/mapping_parser.py
deleted file mode 100644
index f1e9f177..00000000
--- a/plan4past/utils/mapping_parser.py
+++ /dev/null
@@ -1,186 +0,0 @@
-# -*- coding: utf-8 -*-
-#
-# Copyright 2021 -- 2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of Plan4Past.
-#
-# Plan4Past is free software: you can redistribute it and/or modify
-# it under the terms of the GNU Lesser General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# Plan4Past is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU Lesser General Public License for more details.
-#
-# You should have received a copy of the GNU Lesser General Public License
-# along with Plan4Past.  If not, see <https://www.gnu.org/licenses/>.
-#
-
-"""Mapping parser."""
-import re
-from typing import Dict, Optional, Sequence, Set, Tuple
-
-from pddl.custom_types import name
-from pddl.logic import Constant, Predicate, constants
-from pylogics.syntax.base import Formula
-from pylogics.syntax.pltl import Atomic as PLTLAtomic
-
-from plan4past.utils.atoms_visitor import find_atoms
-
-
-class MappingParserError(Exception):
-    """Mapping parser error."""
-
-    def __init__(self, message: str, *args, row_id: Optional[int] = None) -> None:
-        """
-        Initialize a mapping parser error.
-
-        :param row_id: the row id
-        """
-        self.row_id = row_id
-
-        super().__init__(self._make_message_prefix() + message, *args)
-
-    def _make_message_prefix(self) -> str:
-        """Make the message prefix."""
-        if self.row_id is None:
-            return "invalid mapping: "
-        return f"invalid mapping at row {self.row_id}: "
-
-
-SYMBOL_REGEX = re.compile("[a-z_]([a-zA-Z0-9_-]+[a-zA-Z0-9_])|[a-z_][a-zA-Z0-9_]*")
-"""The following is a sub-regex of AtomName.REGEX in pylogics.syntax.base."""
-
-
-def _check_pddl_name(row_id: int, pddl_name: str, what: str) -> None:
-    """Check that a PDDL name is valid."""
-    try:
-        name(pddl_name)
-    except ValueError as e:
-        raise MappingParserError(
-            f"got an invalid name for {what}: '{pddl_name}'. It must match the regex {name.REGEX}",
-            row_id=row_id,
-        ) from e
-
-
-def _parse_constants(row_id: int, constants_str: str) -> Sequence[Constant]:
-    """
-    Parse a string of constants.
-
-    :param row_id: the row id
-    :param constants_str: the string of constants
-    :return: the sequence of constants
-    """
-    try:
-        return constants(constants_str)
-    except ValueError as e:
-        raise MappingParserError(f"got an invalid constant: {e}", row_id=row_id) from e
-
-
-def _parse_predicate(row_id: int, predicate_str: str) -> Predicate:
-    """
-    Parse a predicate.
-
-    :param predicate_str: the predicate string
-    :return: the predicate
-    """
-    predicate_name, cons = predicate_str.split(" ", maxsplit=1)
-
-    _check_pddl_name(row_id, predicate_name, "a predicate")
-    parsed_constants = _parse_constants(row_id, cons)
-    return Predicate(predicate_name, *parsed_constants)
-
-
-def _process_row(row_id: int, row_str: str) -> Tuple[str, Predicate]:
-    """
-    Process a row of the mapping file.
-
-    :param row_id: the row id
-    :param row_str: the row string
-    :return: the pair (symbol_name, predicate_str)
-    """
-    # check the row is a valid mapping
-    comma_separated_row_parts = row_str.split(",")
-    if len(comma_separated_row_parts) != 2:
-        raise MappingParserError(
-            "expected a mapping of the form '<symbol>,<predicate>'", row_id=row_id
-        )
-
-    symbol_name, predicate = comma_separated_row_parts
-
-    # strip leading and trailing whitespaces
-    symbol_name = symbol_name.strip()
-    predicate_str = predicate.strip()
-
-    if symbol_name == "" or SYMBOL_REGEX.fullmatch(symbol_name) is None:
-        raise MappingParserError(
-            "symbol cannot be empty string and must match the regex {SYMBOL_REGEX}",
-            row_id=row_id,
-        )
-    if predicate_str == "":
-        raise MappingParserError("predicate cannot be empty string", row_id=row_id)
-
-    predicate = _parse_predicate(row_id, predicate_str)
-    return symbol_name, predicate
-
-
-def _check_unmapped_symbols(
-    all_symbol_names: Set[str], mapped_symbol_names: Set[str]
-) -> None:
-    """Check that all symbols are mapped."""
-    # check if there are unmapped symbols (exclude 'true' and 'false')
-    unmapped_symbols = all_symbol_names - {"true", "false"} - mapped_symbol_names
-    # if some symbols are not mapped, raise an error
-    if unmapped_symbols:
-        raise MappingParserError(
-            f"the following symbols of the formula are not mapped: {unmapped_symbols}"
-        )
-
-
-def should_skip_row(row_str: str) -> bool:
-    """Check if a row should be skipped."""
-    # skip empty lines
-    if row_str.strip() == "":
-        return True
-
-    # skip comments
-    if row_str.strip().startswith(";"):
-        return True
-
-    return False
-
-
-def mapping_parser(text: str, formula: Formula) -> Dict[PLTLAtomic, Predicate]:
-    """Parse symbols to ground predicates mapping."""
-    symbols = find_atoms(formula)
-    symbols_by_name = {symbol.name: symbol for symbol in symbols}
-    maps = text.splitlines(keepends=False)
-    from_atoms_to_fluents = {}
-    mapped_symbol_names = set()
-
-    for row_id, vmap in enumerate(maps):
-        if should_skip_row(vmap):
-            continue
-
-        symbol_name, predicate = _process_row(row_id, vmap)
-
-        if symbol_name not in symbols_by_name:
-            # don't need to process this row, since the symbol does not occur in the formula
-            continue
-
-        if symbol_name in mapped_symbol_names:
-            raise MappingParserError(
-                f"symbol '{symbol_name}' is mapped multiple times", row_id=row_id
-            )
-
-        symbol = symbols_by_name[symbol_name]
-        mapped_symbol_names.add(symbol_name)
-
-        from_atoms_to_fluents[symbol] = predicate
-
-    _check_unmapped_symbols(set(symbols_by_name.keys()), mapped_symbol_names)
-    return from_atoms_to_fluents
diff --git a/plan4past/utils/predicates_visitor.py b/plan4past/utils/predicates_visitor.py
index da81c05b..03ac4a07 100644
--- a/plan4past/utils/predicates_visitor.py
+++ b/plan4past/utils/predicates_visitor.py
@@ -40,7 +40,7 @@
 )
 from pylogics.utils.to_string import to_string
 
-from plan4past.helpers.utils import replace_symbols
+from plan4past.helpers.utils import Y_PREFIX, replace_symbols
 
 
 def predicates_binaryop(formula: _BinaryOp):
@@ -113,7 +113,7 @@ def predicates_since(formula: Since) -> Set[Predicate]:
         tail = Since(*formula.operands[1:])
         return predicates(Since(head, tail))
     formula_name = replace_symbols(to_string(formula))
-    quoted = Predicate(f"Y-{formula_name}")
+    quoted = Predicate(f"{Y_PREFIX}{formula_name}")
     subsinces = predicates_binaryop(formula)
     return {quoted}.union(subsinces)
 
@@ -122,6 +122,6 @@ def predicates_since(formula: Since) -> Set[Predicate]:
 def predicates_once(formula: Once) -> Set[Predicate]:
     """Compute predicate for a Once formula."""
     formula_name = replace_symbols(to_string(formula))
-    quoted = Predicate(f"Y-{formula_name}")
+    quoted = Predicate(f"{Y_PREFIX}{formula_name}")
     sub = predicates_unaryop(formula)
     return sub.union({quoted})
diff --git a/plan4past/utils/rewrite_formula_visitor.py b/plan4past/utils/rewrite_formula_visitor.py
index d0981895..36162b9a 100644
--- a/plan4past/utils/rewrite_formula_visitor.py
+++ b/plan4past/utils/rewrite_formula_visitor.py
@@ -40,6 +40,8 @@
     Since,
 )
 
+from plan4past.helpers.utils import validate
+
 
 def rewrite_unaryop(formula: _UnaryOp):
     """Rewrite the formula for a unary operator."""
@@ -69,6 +71,8 @@ def rewrite_false(formula: PropositionalFalse) -> Formula:
 @rewrite.register
 def rewrite_atomic(formula: PLTLAtomic) -> Formula:
     """Compute the basic formula for an atomic formula."""
+    # validate atomic formula symbol - it must be a PDDL ground fluent
+    validate(formula.name)
     return formula
 
 
diff --git a/plan4past/utils/val_predicates_visitor.py b/plan4past/utils/val_predicates_visitor.py
index 83ae37b0..a1c7006e 100644
--- a/plan4past/utils/val_predicates_visitor.py
+++ b/plan4past/utils/val_predicates_visitor.py
@@ -76,7 +76,7 @@ def val_predicates_false(_formula: PropositionalFalse) -> Set[Predicate]:
 @val_predicates.register
 def val_predicates_atomic(formula: PLTLAtomic) -> Set[Predicate]:
     """Compute the value predicate for an atomic formula."""
-    return {Predicate(add_val_prefix(formula.name))}
+    return {Predicate(add_val_prefix(replace_symbols(formula.name)))}
 
 
 @val_predicates.register
diff --git a/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json b/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json
index c062b3c8..70b5d880 100644
--- a/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json
+++ b/tests/benchmarks/deterministic/BF/elevators_ppltl/elevators_teg.json
@@ -1,31 +1,31 @@
 {
-    "s2-0": "O(served_p1) & O(served_p0 & !(Y(O(served_p1))))",
-    "s3-0": "O(served_p1 & served_p2) & O(served_p0 & !(Y(O(served_p1 | served_p2)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p0))",
-    "s4-0": "O(served_p2 & served_p3) & O(served_p0 & served_p1 & !(Y(O(served_p2 | served_p3)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p3)) & !(O(boarded_p3 & boarded_p0))",
-    "s5-0": "O(served_p2 & served_p3 & served_p4) & O(served_p0 & served_p1 & !(Y(O(served_p2 | served_p3 | served_p4)))) & !(O(boarded_p0 & boarded_p1)) & !(O(boarded_p1 & boarded_p2)) & !(O(boarded_p2 & boarded_p3)) & !(O(boarded_p3 & boarded_p4)) & !(O(boarded_p4 & boarded_p0))",
-    "s6-0": "O(served_p3 & served_p4 & served_p5) & O(served_p0 & served_p1 & served_p2 & !(Y(O(served_p3 | served_p4 | served_p5)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p0))) & !(O(boarded_p5 & (boarded_p0 | boarded_p1)))",
-    "s7-0": "O(served_p3 & served_p4 & served_p5 & served_p6) & O(served_p0 & served_p1 & served_p2 & !(Y(O(served_p3 | served_p4 | served_p5 | served_p6)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6))) & !(O(boarded_p5 & (boarded_p6 | boarded_p0))) & !(O(boarded_p6 & (boarded_p0 | boarded_p1)))",
-    "s8-0": "O(served_p4 & served_p5 & served_p6 & served_p7) & O(served_p0 & served_p1 & served_p2 & served_p3 & !(Y(O(served_p4 | served_p5 | served_p6 | served_p7)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7))) & !(O(boarded_p6 & (boarded_p7 | boarded_p0))) & !(O(boarded_p7 & (boarded_p0 | boarded_p1)))",
-    "s9-0": "O(served_p4 & served_p5 & served_p6 & served_p7 & served_p8) & O(served_p0 & served_p1 & served_p2 & served_p3 & !(Y(O(served_p4 | served_p5 | served_p6 | served_p7 | served_p8)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p0))) & !(O(boarded_p7 & (boarded_p8 | boarded_p0 | boarded_p1))) & !(O(boarded_p8 & (boarded_p0 | boarded_p1 | boarded_p2)))",
-    "s10-0": "O(served_p5 & served_p6 & served_p7 & served_p8 & served_p9) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & !(Y(O(served_p5 | served_p6 | served_p7 | served_p8 | served_p9)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p0))) & !(O(boarded_p8 & (boarded_p9 | boarded_p0 | boarded_p1))) & !(O(boarded_p9 & (boarded_p0 | boarded_p1 | boarded_p2)))",
-    "s11-0": "O(served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & !(Y(O(served_p5 | served_p6 | served_p7 | served_p8 | served_p9 | served_p10)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p0))) & !(O(boarded_p9 & (boarded_p10 | boarded_p0 | boarded_p1))) & !(O(boarded_p10 & (boarded_p0 | boarded_p1 | boarded_p2)))",
-    "s12-0": "O(served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & !(Y(O(served_p6 | served_p7 | served_p8 | served_p9 | served_p10 | served_p11)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p0))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p0 | boarded_p1))) & !(O(boarded_p10 & (boarded_p11 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p11 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))",
-    "s13-0": "O(served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & !(Y(O(served_p6 | served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p0))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p0 | boarded_p1))) & !(O(boarded_p11 & (boarded_p12 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p12 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))",
-    "s14-0": "O(served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & !(Y(O(served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p0))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p0 | boarded_p1))) & !(O(boarded_p12 & (boarded_p13 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p13 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3)))",
-    "s15-0": "O(served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & !(Y(O(served_p7 | served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p0))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p0 | boarded_p1))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p13 & (boarded_p14 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p14 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))",
-    "s16-0": "O(served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & !(Y(O(served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p0))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p0 | boarded_p1))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p14 & (boarded_p15 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p15 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))",
-    "s17-0": "O(served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & !(Y(O(served_p8 | served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p0))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p0 | boarded_p1))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p15 & (boarded_p16 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p16 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4)))",
-    "s18-0": "O(served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & !(Y(O(served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p16 & (boarded_p17 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p17 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))",
-    "s19-0": "O(served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & !(Y(O(served_p9 | served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p17 & (boarded_p18 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p18 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))",
-    "s20-0": "O(served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & !(Y(O(served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p18 & (boarded_p19 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p19 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5)))",
-    "s21-0": "O(served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & !(Y(O(served_p10 | served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p19 & (boarded_p20 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p20 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))",
-    "s22-0": "O(served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & !(Y(O(served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p20 & (boarded_p21 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p21 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))",
-    "s23-0": "O(served_p11 & served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & !(Y(O(served_p11 | served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p21 & (boarded_p22 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p22 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6)))",
-    "s24-0": "O(served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & !(Y(O(served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p22 & (boarded_p23 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p23 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))",
-    "s25-0": "O(served_p12 & served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & !(Y(O(served_p12 | served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p23 & (boarded_p24 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p24 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))",
-    "s26-0": "O(served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & !(Y(O(served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p24 & (boarded_p25 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p25 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7)))",
-    "s27-0": "O(served_p13 & served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & !(Y(O(served_p13 | served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p25 & (boarded_p26 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p26 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))",
-    "s28-0": "O(served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & !(Y(O(served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p26 & (boarded_p27 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p27 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))",
-    "s29-0": "O(served_p14 & served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27 & served_p28) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & !(Y(O(served_p14 | served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27 | served_p28)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p26 & (boarded_p27 | boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p27 & (boarded_p28 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p28 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8)))",
-    "s30-0": "O(served_p15 & served_p16 & served_p17 & served_p18 & served_p19 & served_p20 & served_p21 & served_p22 & served_p23 & served_p24 & served_p25 & served_p26 & served_p27 & served_p28 & served_p29) & O(served_p0 & served_p1 & served_p2 & served_p3 & served_p4 & served_p5 & served_p6 & served_p7 & served_p8 & served_p9 & served_p10 & served_p11 & served_p12 & served_p13 & served_p14 & !(Y(O(served_p15 | served_p16 | served_p17 | served_p18 | served_p19 | served_p20 | served_p21 | served_p22 | served_p23 | served_p24 | served_p25 | served_p26 | served_p27 | served_p28 | served_p29)))) & !(O(boarded_p0 & (boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10))) & !(O(boarded_p1 & (boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11))) & !(O(boarded_p2 & (boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12))) & !(O(boarded_p3 & (boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13))) & !(O(boarded_p4 & (boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14))) & !(O(boarded_p5 & (boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15))) & !(O(boarded_p6 & (boarded_p7 | boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16))) & !(O(boarded_p7 & (boarded_p8 | boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17))) & !(O(boarded_p8 & (boarded_p9 | boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18))) & !(O(boarded_p9 & (boarded_p10 | boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19))) & !(O(boarded_p10 & (boarded_p11 | boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20))) & !(O(boarded_p11 & (boarded_p12 | boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21))) & !(O(boarded_p12 & (boarded_p13 | boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22))) & !(O(boarded_p13 & (boarded_p14 | boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23))) & !(O(boarded_p14 & (boarded_p15 | boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24))) & !(O(boarded_p15 & (boarded_p16 | boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25))) & !(O(boarded_p16 & (boarded_p17 | boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26))) & !(O(boarded_p17 & (boarded_p18 | boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27))) & !(O(boarded_p18 & (boarded_p19 | boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28))) & !(O(boarded_p19 & (boarded_p20 | boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29))) & !(O(boarded_p20 & (boarded_p21 | boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0))) & !(O(boarded_p21 & (boarded_p22 | boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1))) & !(O(boarded_p22 & (boarded_p23 | boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2))) & !(O(boarded_p23 & (boarded_p24 | boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3))) & !(O(boarded_p24 & (boarded_p25 | boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4))) & !(O(boarded_p25 & (boarded_p26 | boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5))) & !(O(boarded_p26 & (boarded_p27 | boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6))) & !(O(boarded_p27 & (boarded_p28 | boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7))) & !(O(boarded_p28 & (boarded_p29 | boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8))) & !(O(boarded_p29 & (boarded_p0 | boarded_p1 | boarded_p2 | boarded_p3 | boarded_p4 | boarded_p5 | boarded_p6 | boarded_p7 | boarded_p8 | boarded_p9)))"
+    "s2-0": "O(\"served p1\") & O(\"served p0\" & !(Y(O(\"served p1\"))))",
+    "s3-0": "O(\"served p1\" & \"served p2\") & O(\"served p0\" & !(Y(O(\"served p1\" | \"served p2\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p0\"))",
+    "s4-0": "O(\"served p2\" & \"served p3\") & O(\"served p0\" & \"served p1\" & !(Y(O(\"served p2\" | \"served p3\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p3\")) & !(O(\"boarded p3\" & \"boarded p0\"))",
+    "s5-0": "O(\"served p2\" & \"served p3\" & \"served p4\") & O(\"served p0\" & \"served p1\" & !(Y(O(\"served p2\" | \"served p3\" | \"served p4\")))) & !(O(\"boarded p0\" & \"boarded p1\")) & !(O(\"boarded p1\" & \"boarded p2\")) & !(O(\"boarded p2\" & \"boarded p3\")) & !(O(\"boarded p3\" & \"boarded p4\")) & !(O(\"boarded p4\" & \"boarded p0\"))",
+    "s6-0": "O(\"served p3\" & \"served p4\" & \"served p5\") & O(\"served p0\" & \"served p1\" & \"served p2\" & !(Y(O(\"served p3\" | \"served p4\" | \"served p5\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p0\"))) & !(O(\"boarded p5\" & (\"boarded p0\" | \"boarded p1\")))",
+    "s7-0": "O(\"served p3\" & \"served p4\" & \"served p5\" & \"served p6\") & O(\"served p0\" & \"served p1\" & \"served p2\" & !(Y(O(\"served p3\" | \"served p4\" | \"served p5\" | \"served p6\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p0\"))) & !(O(\"boarded p6\" & (\"boarded p0\" | \"boarded p1\")))",
+    "s8-0": "O(\"served p4\" & \"served p5\" & \"served p6\" & \"served p7\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & !(Y(O(\"served p4\" | \"served p5\" | \"served p6\" | \"served p7\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p0\"))) & !(O(\"boarded p7\" & (\"boarded p0\" | \"boarded p1\")))",
+    "s9-0": "O(\"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & !(Y(O(\"served p4\" | \"served p5\" | \"served p6\" | \"served p7\" | \"served p8\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p0\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p8\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))",
+    "s10-0": "O(\"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & !(Y(O(\"served p5\" | \"served p6\" | \"served p7\" | \"served p8\" | \"served p9\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p0\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p9\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))",
+    "s11-0": "O(\"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & !(Y(O(\"served p5\" | \"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p0\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p10\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\")))",
+    "s12-0": "O(\"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & !(Y(O(\"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p0\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p11\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))",
+    "s13-0": "O(\"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & !(Y(O(\"served p6\" | \"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p0\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p12\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))",
+    "s14-0": "O(\"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & !(Y(O(\"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p0\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p13\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\")))",
+    "s15-0": "O(\"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & !(Y(O(\"served p7\" | \"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p0\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p14\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))",
+    "s16-0": "O(\"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & !(Y(O(\"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p0\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p15\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))",
+    "s17-0": "O(\"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & !(Y(O(\"served p8\" | \"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p0\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p16\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\")))",
+    "s18-0": "O(\"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & !(Y(O(\"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p17\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))",
+    "s19-0": "O(\"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & !(Y(O(\"served p9\" | \"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p18\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))",
+    "s20-0": "O(\"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & !(Y(O(\"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p19\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\")))",
+    "s21-0": "O(\"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & !(Y(O(\"served p10\" | \"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p20\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))",
+    "s22-0": "O(\"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & !(Y(O(\"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p21\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))",
+    "s23-0": "O(\"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & !(Y(O(\"served p11\" | \"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p22\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\")))",
+    "s24-0": "O(\"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & !(Y(O(\"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p23\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))",
+    "s25-0": "O(\"served p12\" & \"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & !(Y(O(\"served p12\" | \"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p24\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))",
+    "s26-0": "O(\"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & !(Y(O(\"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p25\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\")))",
+    "s27-0": "O(\"served p13\" & \"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & !(Y(O(\"served p13\" | \"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p26\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))",
+    "s28-0": "O(\"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & !(Y(O(\"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p27\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))",
+    "s29-0": "O(\"served p14\" & \"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\" & \"served p28\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & !(Y(O(\"served p14\" | \"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\" | \"served p28\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p27\" & (\"boarded p28\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p28\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\")))",
+    "s30-0": "O(\"served p15\" & \"served p16\" & \"served p17\" & \"served p18\" & \"served p19\" & \"served p20\" & \"served p21\" & \"served p22\" & \"served p23\" & \"served p24\" & \"served p25\" & \"served p26\" & \"served p27\" & \"served p28\" & \"served p29\") & O(\"served p0\" & \"served p1\" & \"served p2\" & \"served p3\" & \"served p4\" & \"served p5\" & \"served p6\" & \"served p7\" & \"served p8\" & \"served p9\" & \"served p10\" & \"served p11\" & \"served p12\" & \"served p13\" & \"served p14\" & !(Y(O(\"served p15\" | \"served p16\" | \"served p17\" | \"served p18\" | \"served p19\" | \"served p20\" | \"served p21\" | \"served p22\" | \"served p23\" | \"served p24\" | \"served p25\" | \"served p26\" | \"served p27\" | \"served p28\" | \"served p29\")))) & !(O(\"boarded p0\" & (\"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\"))) & !(O(\"boarded p1\" & (\"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\"))) & !(O(\"boarded p2\" & (\"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\"))) & !(O(\"boarded p3\" & (\"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\"))) & !(O(\"boarded p4\" & (\"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\"))) & !(O(\"boarded p5\" & (\"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\"))) & !(O(\"boarded p6\" & (\"boarded p7\" | \"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\"))) & !(O(\"boarded p7\" & (\"boarded p8\" | \"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\"))) & !(O(\"boarded p8\" & (\"boarded p9\" | \"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\"))) & !(O(\"boarded p9\" & (\"boarded p10\" | \"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\"))) & !(O(\"boarded p10\" & (\"boarded p11\" | \"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\"))) & !(O(\"boarded p11\" & (\"boarded p12\" | \"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\"))) & !(O(\"boarded p12\" & (\"boarded p13\" | \"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\"))) & !(O(\"boarded p13\" & (\"boarded p14\" | \"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\"))) & !(O(\"boarded p14\" & (\"boarded p15\" | \"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\"))) & !(O(\"boarded p15\" & (\"boarded p16\" | \"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\"))) & !(O(\"boarded p16\" & (\"boarded p17\" | \"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\"))) & !(O(\"boarded p17\" & (\"boarded p18\" | \"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\"))) & !(O(\"boarded p18\" & (\"boarded p19\" | \"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\"))) & !(O(\"boarded p19\" & (\"boarded p20\" | \"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\"))) & !(O(\"boarded p20\" & (\"boarded p21\" | \"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\"))) & !(O(\"boarded p21\" & (\"boarded p22\" | \"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\"))) & !(O(\"boarded p22\" & (\"boarded p23\" | \"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\"))) & !(O(\"boarded p23\" & (\"boarded p24\" | \"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\"))) & !(O(\"boarded p24\" & (\"boarded p25\" | \"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\"))) & !(O(\"boarded p25\" & (\"boarded p26\" | \"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\"))) & !(O(\"boarded p26\" & (\"boarded p27\" | \"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\"))) & !(O(\"boarded p27\" & (\"boarded p28\" | \"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\"))) & !(O(\"boarded p28\" & (\"boarded p29\" | \"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\"))) & !(O(\"boarded p29\" & (\"boarded p0\" | \"boarded p1\" | \"boarded p2\" | \"boarded p3\" | \"boarded p4\" | \"boarded p5\" | \"boarded p6\" | \"boarded p7\" | \"boarded p8\" | \"boarded p9\")))"
 }
\ No newline at end of file
diff --git a/tests/helpers/planutils/downward.py b/tests/helpers/planutils/downward.py
index a6ce0172..6ef77122 100644
--- a/tests/helpers/planutils/downward.py
+++ b/tests/helpers/planutils/downward.py
@@ -68,7 +68,7 @@ def get_planner_cmd(
 
     def process_output(self, working_directory: Path, stdout: str) -> PlannerResult:
         """Process the output of the planner."""
-        logger.debug("Processing output of LAMA")
+        logger.debug("Processing output of Fast-Downward.")
 
         # the sas_plan file is in the /root directory
         sas_file = working_directory / "sas_plan"
diff --git a/tests/test_compiler/test_blocksworld_det.py b/tests/test_compiler/test_blocksworld_det.py
index 2e412a3c..cdfafe4b 100644
--- a/tests/test_compiler/test_blocksworld_det.py
+++ b/tests/test_compiler/test_blocksworld_det.py
@@ -35,8 +35,8 @@ class TestBlocksworldDetSimpleSequence(BaseCompilerTest):
 
     PATH_TO_DOMAINS_DIR = BLOCKSWORLD_DIR
     PATH_TO_INSTANCES_DIR = BLOCKSWORLD_DIR
-    MIN_INSTANCE_ID = 2
-    MAX_INSTANCE_ID = 10
+    MIN_INSTANCE_ID = 3
+    MAX_INSTANCE_ID = 3
 
     def make_formula(self, instance_id: int, domain: Path, problem: Path) -> str:
         """
@@ -50,7 +50,7 @@ def make_formula(self, instance_id: int, domain: Path, problem: Path) -> str:
         trailing_brackets = ""
         for i in range(1, instance_id):
             last = i == instance_id - 1
-            formula += f"O(on_b{i}_b{i + 1}" + (" & Y(" if not last else "")
+            formula += f'O("on b{i} b{i + 1}"' + (" & Y(" if not last else "")
             trailing_brackets += "))" if not last else ")"
         return formula + trailing_brackets
 
diff --git a/tests/test_compiler/test_readme_example.py b/tests/test_compiler/test_readme_example.py
index b2015447..383cf543 100644
--- a/tests/test_compiler/test_readme_example.py
+++ b/tests/test_compiler/test_readme_example.py
@@ -24,31 +24,18 @@
 
 from pathlib import Path
 
-import pytest
-from pddl.logic import Predicate, constants
 from pddl.parser.domain import DomainParser
 from pddl.parser.problem import ProblemParser
 from pylogics.parsers import parse_pltl
-from pylogics.syntax.pltl import Atomic as PLTLAtomic
 
 from plan4past.compiler import Compiler
 from tests.helpers.constants import EXAMPLES_DIR
 from tests.helpers.misc import check_compilation
 
 
-@pytest.mark.parametrize(
-    "from_atoms_to_fluent",
-    [
-        None,
-        {
-            PLTLAtomic("on_b_a"): Predicate("on", *constants("b a")),
-            PLTLAtomic("ontable_c"): Predicate("ontable", *constants("c")),
-        },
-    ],
-)
-def test_readme_example(val, default_planner, from_atoms_to_fluent) -> None:
+def test_readme_example(val, default_planner) -> None:
     """Test the example from the README."""
-    formula = "on_b_a & O(ontable_c)"
+    formula = '"on b a" & O("ontable c")'
     domain_parser = DomainParser()
     problem_parser = ProblemParser()
 
@@ -59,9 +46,7 @@ def test_readme_example(val, default_planner, from_atoms_to_fluent) -> None:
     problem = problem_parser(pddl_example_problem_path.read_text(encoding="utf-8"))
     goal = parse_pltl(formula)
 
-    compiler = Compiler(
-        domain, problem, goal, from_atoms_to_fluent=from_atoms_to_fluent
-    )
+    compiler = Compiler(domain, problem, goal)
     compiler.compile()
     compiled_domain, compiled_problem = compiler.result
 
diff --git a/tests/test_helpers/test_utils.py b/tests/test_helpers/test_utils.py
index 18237ef1..4620fbca 100644
--- a/tests/test_helpers/test_utils.py
+++ b/tests/test_helpers/test_utils.py
@@ -22,55 +22,33 @@
 
 """This module contains tests for the plan4past.helpers.utils module."""
 import pytest
-from pddl.logic import Predicate, constants
-from pylogics.syntax.pltl import Atomic as PLTLAtomic
-from pylogics.syntax.pltl import Before, Since
 
 from plan4past.helpers.utils import (
     add_val_prefix,
     check_,
-    default_mapping,
     remove_before_prefix,
     remove_val_prefix,
 )
 
 
-def test_default_mapping() -> None:
-    """Test the default mapping function."""
-    p_a_b = PLTLAtomic("p_a_b")
-    p_b_c = PLTLAtomic("p_b_c")
-    p_c_d = PLTLAtomic("p_c_d")
-    p2 = PLTLAtomic("p2")
-    before_p_a_b = Before(p_a_b)
-    p_b_c_since_p_c_d = Since(p_b_c, p_c_d)
-
-    result = default_mapping(before_p_a_b & p_b_c_since_p_c_d & p2)
-    assert result == {
-        p_a_b: Predicate("p", *constants("a b")),
-        p_b_c: Predicate("p", *constants("b c")),
-        p_c_d: Predicate("p", *constants("c d")),
-        p2: Predicate("p2"),
-    }
-
-
 def test_val_prefix() -> None:
     """Test the add_val_prefix function."""
-    assert add_val_prefix("Y-foo") == "val-Y-foo"
-    assert add_val_prefix("Yfoo") == "val-Yfoo"
-    assert add_val_prefix("foo") == "val-foo"
-    assert add_val_prefix("Y-foo-bar") == "val-Y-foo-bar"
+    assert add_val_prefix("Y-foo") == "VAL__Y-foo"
+    assert add_val_prefix("Yfoo") == "VAL__Yfoo"
+    assert add_val_prefix("foo") == "VAL__foo"
+    assert add_val_prefix("Y-foo-bar") == "VAL__Y-foo-bar"
 
 
 def test_remove_before_prefix() -> None:
     """Test the remove_before_prefix function."""
-    assert remove_before_prefix("Y-foo") == "foo"
-    assert remove_before_prefix("Yfoo") == "foo"
+    assert remove_before_prefix("Y__foo") == "foo"
+    assert remove_before_prefix("YLPAR__foo__RPAR") == "foo"
     assert remove_before_prefix("foo") == "foo"
 
 
 def test_remove_val_prefix() -> None:
     """Test the remove_val_prefix function."""
-    assert remove_val_prefix("val-foo") == "foo"
+    assert remove_val_prefix("VAL__foo") == "foo"
     assert remove_val_prefix("foo") == "foo"
 
 
diff --git a/tests/test_utils/test_derived_visitor.py b/tests/test_utils/test_derived_visitor.py
index aa299c92..7c54d5b2 100644
--- a/tests/test_utils/test_derived_visitor.py
+++ b/tests/test_utils/test_derived_visitor.py
@@ -24,7 +24,6 @@
 from typing import Set
 
 import pytest
-from pddl.logic import Constant
 from pddl.logic.base import And, Not, Or
 from pddl.logic.predicates import DerivedPredicate, Predicate
 from pylogics.syntax.pltl import Atomic as PLTLAtomic
@@ -62,7 +61,7 @@ def test_derived_predicates_visitor_not_implemented_fail():
     with pytest.raises(
         NotImplementedError, match="handler not implemented for object <class 'int'>"
     ):
-        derived_predicates(1, {})
+        derived_predicates(1)
 
 
 def test_derived_predicates_visitor_true():
@@ -70,7 +69,7 @@ def test_derived_predicates_visitor_true():
     val = Predicate(add_val_prefix("true"))
     expected = {DerivedPredicate(val, And())}
 
-    actual = derived_predicates(PropositionalTrue(), {})
+    actual = derived_predicates(PropositionalTrue())
     assert _eq(actual, expected)
 
 
@@ -79,7 +78,7 @@ def test_derived_predicates_visitor_false():
     val = Predicate(add_val_prefix("false"))
     expected = {DerivedPredicate(val, Or())}
 
-    actual = derived_predicates(PropositionalFalse(), {})
+    actual = derived_predicates(PropositionalFalse())
     assert _eq(actual, expected)
 
 
@@ -87,10 +86,10 @@ def test_derived_predicates_visitor_atomic():
     """Test the derived predicates visitor for the atomic formula."""
     a = PLTLAtomic("a")
     val = Predicate(add_val_prefix("a"))
-    condition = Predicate("p", Constant("a"))
+    condition = Predicate("a")
     expected = {DerivedPredicate(val, condition)}
 
-    actual = derived_predicates(a, {a: condition})
+    actual = derived_predicates(a)
     assert _eq(actual, expected)
 
 
@@ -99,10 +98,10 @@ def test_derived_predicates_visitor_and():
     a = PLTLAtomic("a")
     b = PLTLAtomic("b")
 
-    condition_a = Predicate("p", Constant("a"))
-    condition_b = Predicate("p", Constant("b"))
+    condition_a = Predicate("a")
+    condition_b = Predicate("b")
 
-    val = Predicate(add_val_prefix("a-and-b"))
+    val = Predicate(add_val_prefix("LPAR__a__RPAR-__AND__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
 
@@ -114,7 +113,7 @@ def test_derived_predicates_visitor_and():
         DerivedPredicate(val_b, condition_b),
     }
 
-    actual = derived_predicates(a & b, {a: condition_a, b: condition_b})
+    actual = derived_predicates(a & b)
     assert _eq(actual, expected)
 
 
@@ -123,10 +122,10 @@ def test_derived_predicates_visitor_or():
     a = PLTLAtomic("a")
     b = PLTLAtomic("b")
 
-    condition_a = Predicate("p", Constant("a"))
-    condition_b = Predicate("p", Constant("b"))
+    condition_a = Predicate("a")
+    condition_b = Predicate("b")
 
-    val = Predicate(add_val_prefix("a-or-b"))
+    val = Predicate(add_val_prefix("LPAR__a__RPAR-__OR__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
 
@@ -138,7 +137,7 @@ def test_derived_predicates_visitor_or():
         DerivedPredicate(val_b, condition_b),
     }
 
-    actual = derived_predicates(a | b, {a: condition_a, b: condition_b})
+    actual = derived_predicates(a | b)
     assert _eq(actual, expected)
 
 
@@ -146,16 +145,16 @@ def test_derived_predicates_visitor_not():
     """Test the derived predicates visitor for the not formula."""
     a = PLTLAtomic("a")
 
-    condition_a = Predicate("p", Constant("a"))
+    condition_a = Predicate("a")
 
-    val = Predicate(add_val_prefix("not-a"))
+    val = Predicate(add_val_prefix("NOT__LPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
 
     condition = Not(val_a)
 
     expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)}
 
-    actual = derived_predicates(~a, {a: condition_a})
+    actual = derived_predicates(~a)
     assert _eq(actual, expected)
 
 
@@ -164,16 +163,16 @@ def test_derived_predicates_visitor_before():
     a = PLTLAtomic("a")
     Ya = Before(a)
 
-    condition_a = Predicate("p", Constant("a"))
+    condition_a = Predicate("a")
 
-    val = Predicate(add_val_prefix("Ya"))
+    val = Predicate(add_val_prefix("YLPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
 
-    condition = Predicate("Ya")
+    condition = Predicate("YLPAR__a__RPAR")
 
     expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)}
 
-    actual = derived_predicates(Ya, {a: condition_a})
+    actual = derived_predicates(Ya)
     assert _eq(actual, expected)
 
 
@@ -187,14 +186,18 @@ def test_derived_predicates_visitor_since():
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
     val_c = Predicate(add_val_prefix("c"))
-    val_a_since_b_since_c = Predicate(add_val_prefix("a-S-b-S-c"))
-    val_b_since_c = Predicate(add_val_prefix("b-S-c"))
-    Y_a_since_b_since_c = Predicate("Y-a-S-b-S-c")
-    Y_b_since_c = Predicate("Y-b-S-c")
-
-    condition_a = Predicate("p", Constant("a"))
-    condition_b = Predicate("p", Constant("b"))
-    condition_c = Predicate("p", Constant("c"))
+    val_a_since_b_since_c = Predicate(
+        add_val_prefix("LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR")
+    )
+    val_b_since_c = Predicate(add_val_prefix("LPAR__b__RPAR-S-LPAR__c__RPAR"))
+    Y_a_since_b_since_c = Predicate(
+        "Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR"
+    )
+    Y_b_since_c = Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR")
+
+    condition_a = Predicate("a")
+    condition_b = Predicate("b")
+    condition_c = Predicate("c")
     condition_b_since_c = Or(val_c, And(val_b, Y_b_since_c))
     condition_a_since_b_since_c = Or(val_b_since_c, And(val_a, Y_a_since_b_since_c))
 
@@ -206,9 +209,7 @@ def test_derived_predicates_visitor_since():
         DerivedPredicate(val_c, condition_c),
     }
 
-    actual = derived_predicates(
-        a_since_b_since_c, {a: condition_a, b: condition_b, c: condition_c}
-    )
+    actual = derived_predicates(a_since_b_since_c)
     assert _eq(actual, expected)
 
 
@@ -218,10 +219,10 @@ def test_derived_predicates_visitor_once():
     once_a = Once(a)
 
     val_a = Predicate(add_val_prefix("a"))
-    val_once_a = Predicate(add_val_prefix("Oa"))
-    Y_once_a = Predicate("Y-Oa")
+    val_once_a = Predicate(add_val_prefix("OLPAR__a__RPAR"))
+    Y_once_a = Predicate("Y__OLPAR__a__RPAR")
 
-    condition_a = Predicate("p", Constant("a"))
+    condition_a = Predicate("a")
     condition_once_a = Or(val_a, Y_once_a)
 
     expected = {
@@ -229,5 +230,5 @@ def test_derived_predicates_visitor_once():
         DerivedPredicate(val_once_a, condition_once_a),
     }
 
-    actual = derived_predicates(once_a, {a: condition_a})
+    actual = derived_predicates(once_a)
     assert _eq(actual, expected)
diff --git a/tests/test_utils/test_mapping_parser.py b/tests/test_utils/test_mapping_parser.py
deleted file mode 100644
index a9944f7a..00000000
--- a/tests/test_utils/test_mapping_parser.py
+++ /dev/null
@@ -1,168 +0,0 @@
-# -*- coding: utf-8 -*-
-#
-# Copyright 2021 -- 2023 WhiteMech
-#
-# ------------------------------
-#
-# This file is part of Plan4Past.
-#
-# Plan4Past is free software: you can redistribute it and/or modify
-# it under the terms of the GNU Lesser General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# Plan4Past is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU Lesser General Public License for more details.
-#
-# You should have received a copy of the GNU Lesser General Public License
-# along with Plan4Past.  If not, see <https://www.gnu.org/licenses/>.
-#
-
-"""This module contains tests for the plan4past.utils.mapping_parser module."""
-from textwrap import dedent
-
-import pytest
-from pddl.logic import Constant, Predicate, constants
-from pylogics.syntax.pltl import Atomic as PLTLAtomic
-from pylogics.syntax.pltl import FalseFormula as PLTLFalse
-from pylogics.syntax.pltl import TrueFormula as PLTLTrue
-
-from plan4past.utils.mapping_parser import MappingParserError, mapping_parser
-from tests.helpers.constants import EXAMPLE_MAP_FILE
-
-_on_b_a = PLTLAtomic("on_b_a")
-_ontable_c = PLTLAtomic("ontable_c")
-
-_pddl_on_b_a = Predicate("on", *constants("b a"))
-_pddl_ontable_c = Predicate("ontable", Constant("c"))
-
-
-@pytest.mark.parametrize(
-    "formula,expected_mapping",
-    [
-        (PLTLTrue(), {}),
-        (PLTLFalse(), {}),
-        (_on_b_a, {_on_b_a: _pddl_on_b_a}),
-        (_ontable_c, {_ontable_c: _pddl_ontable_c}),
-        (_on_b_a & _ontable_c, {_on_b_a: _pddl_on_b_a, _ontable_c: _pddl_ontable_c}),
-    ],
-)
-def test_mapping_parser_successful_case(formula, expected_mapping):
-    """Test the mapping parser with the example map file."""
-    actual_mapping = mapping_parser(EXAMPLE_MAP_FILE.read_text(), formula)
-    assert actual_mapping == expected_mapping
-
-
-def test_mapping_parser_empty_file():
-    """Test the mapping parser when the file is empty."""
-    assert not mapping_parser("", PLTLTrue())
-
-
-def test_mapping_parser_empty_lines():
-    """Test the mapping parser with empty lines."""
-    assert not mapping_parser("\n\n", PLTLTrue())
-
-
-def test_mapping_parser_with_comments():
-    """Test the mapping parser with comments."""
-    assert mapping_parser(";;;;\n;\non_b_a,on b a", _on_b_a) == {_on_b_a: _pddl_on_b_a}
-
-
-def test_mapping_parser_when_row_has_no_comma():
-    """Test the mapping parser when a row is invalid (has no comma)."""
-    with pytest.raises(
-        MappingParserError,
-        match="invalid mapping at row 0: expected a mapping of the form '<symbol>,<predicate>'",
-    ):
-        mapping_parser(
-            "invalid_row\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_when_row_has_more_than_one_comma():
-    """Test the mapping parser when a row is invalid (has more than two commas)."""
-    with pytest.raises(
-        MappingParserError,
-        match="invalid mapping at row 0: expected a mapping of the form '<symbol>,<predicate>'",
-    ):
-        mapping_parser(
-            "invalid_row,invalid_row,\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_bad_symbol_format():
-    """Test the mapping parser when a row is invalid (bad symbol format)."""
-    with pytest.raises(
-        MappingParserError,
-        match="invalid mapping at row 0: symbol cannot be empty string and must match the regex ",
-    ):
-        mapping_parser(
-            "not a valid symbol,some_predicate\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_empty_predicate_name():
-    """Test the mapping parser when a row is invalid (empty predicate name)."""
-    with pytest.raises(
-        MappingParserError,
-        match="invalid mapping at row 0: predicate cannot be empty string",
-    ):
-        mapping_parser(
-            "some_symbol,\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_invalid_predicate_name():
-    """Test the mapping parser when a row is invalid (invalid predicate name)."""
-    with pytest.raises(
-        MappingParserError,
-        match=r"invalid mapping at row 0: got an invalid name for a predicate: 'not!'\. It must match the regex .*",
-    ):
-        mapping_parser(
-            "some_symbol,not! a valid predicate\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_invalid_constant_name():
-    """Test the mapping parser when a row is invalid (invalid constant name)."""
-    with pytest.raises(
-        MappingParserError,
-        match=r"invalid mapping at row 0: got an invalid constant: Value 'wrong-constant-name!' "
-        r"does not match the regular expression .*",
-    ):
-        mapping_parser(
-            "some_symbol,predicate wrong-constant-name!\n",
-            PLTLTrue(),
-        )
-
-
-def test_mapping_parser_in_case_of_unmapped_symbols():
-    """Test the mapping parser when a symbol is not mapped."""
-    with pytest.raises(
-        MappingParserError,
-        match=r"invalid mapping: the following symbols of the formula are not mapped: {'a|b', 'b|a'}",
-    ):
-        mapping_parser(
-            dedent(
-                """\
-                some_symbol,predicate some_constant
-                """
-            ),
-            PLTLAtomic("a") & PLTLAtomic("b") & PLTLTrue(),
-        )
-
-
-def test_mapping_parser_symbol_occurs_more_than_once():
-    """Test the mapping parser when a symbol occurs more than once."""
-    with pytest.raises(
-        MappingParserError,
-        match="invalid mapping at row 1: symbol 'on_b_a' is mapped multiple times",
-    ):
-        mapping_parser("on_b_a,on b a\non_b_a,on b a", _on_b_a)
diff --git a/tests/test_utils/test_predicates_visitor.py b/tests/test_utils/test_predicates_visitor.py
index b398570d..9f32884e 100644
--- a/tests/test_utils/test_predicates_visitor.py
+++ b/tests/test_utils/test_predicates_visitor.py
@@ -84,7 +84,7 @@ def test_predicates_visitor_before():
     """Test the predicates visitor for the before formula."""
     a = PLTLAtomic("a")
     Ya = Before(a)
-    assert predicates(Ya) == {Predicate("Ya")}
+    assert predicates(Ya) == {Predicate("YLPAR__a__RPAR")}
 
 
 def test_predicates_visitor_since():
@@ -94,8 +94,8 @@ def test_predicates_visitor_since():
     c = PLTLAtomic("c")
     a_since_b_since_c = Since(a, b, c)
     assert predicates(a_since_b_since_c) == {
-        Predicate("Y-b-S-c"),
-        Predicate("Y-a-S-b-S-c"),
+        Predicate("Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR"),
+        Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR"),
     }
 
 
@@ -103,4 +103,4 @@ def test_predicates_visitor_once():
     """Test the predicates visitor for the once formula."""
     a = PLTLAtomic("a")
     once_a = Once(a)
-    assert predicates(once_a) == {Predicate("Y-Oa")}
+    assert predicates(once_a) == {Predicate("Y__OLPAR__a__RPAR")}
diff --git a/tests/test_utils/test_rewrite_formula_visitor.py b/tests/test_utils/test_rewrite_formula_visitor.py
index 2bd8a6fc..7a5dbcbe 100644
--- a/tests/test_utils/test_rewrite_formula_visitor.py
+++ b/tests/test_utils/test_rewrite_formula_visitor.py
@@ -58,75 +58,75 @@ def test_rewrite_formula_visitor_false():
 
 def test_rewrite_formula_visitor_atomic():
     """Test the rewrite formula visitor for the atomic formula."""
-    a = PLTLAtomic("a")
+    a = PLTLAtomic('"a"')
     assert rewrite(a) == a
 
 
 def test_rewrite_formula_visitor_and():
     """Test the rewrite formula visitor for the and formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
-    c = PLTLAtomic("c")
-    d = PLTLAtomic("d")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
+    c = PLTLAtomic('"c"')
+    d = PLTLAtomic('"d"')
     assert rewrite(PLTLImplies(a, b) & PLTLImplies(c, d)) == (~a | b) & (~c | d)
 
 
 def test_rewrite_formula_visitor_or():
     """Test the rewrite formula visitor for the or formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
-    c = PLTLAtomic("c")
-    d = PLTLAtomic("d")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
+    c = PLTLAtomic('"c"')
+    d = PLTLAtomic('"d"')
     assert rewrite(PLTLImplies(a, b) | PLTLImplies(c, d)) == (~a | b) | (~c | d)
 
 
 def test_rewrite_formula_visitor_not():
     """Test the rewrite formula visitor for the not formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
     assert rewrite(~PLTLImplies(a, b)) == ~(~a | b)
 
 
 def test_rewrite_formula_visitor_implies():
     """Test the rewrite formula visitor for the implies formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
     assert rewrite(PLTLImplies(a, b)) == (~a | b)
 
 
 def test_rewrite_formula_visitor_equivalence():
     """Test the rewrite formula visitor for the equivalence formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
     assert rewrite(PLTLEquivalence(a, b)) == ((a & b) | (~a & ~b))
 
 
 def test_rewrite_formula_visitor_before():
     """Test the rewrite formula visitor for the before formula."""
-    a = PLTLAtomic("a")
+    a = PLTLAtomic('"a"')
     before_a = Before(a)
     assert rewrite(before_a) == before_a
 
 
 def test_rewrite_formula_visitor_since():
     """Test the rewrite formula visitor for the before formula."""
-    a = PLTLAtomic("a")
-    b = PLTLAtomic("b")
-    c = PLTLAtomic("c")
-    d = PLTLAtomic("d")
+    a = PLTLAtomic('"a"')
+    b = PLTLAtomic('"b"')
+    c = PLTLAtomic('"c"')
+    d = PLTLAtomic('"d"')
     a_since_b_since_c_implies_d = Since(a, b, PLTLImplies(c, d))
     assert rewrite(a_since_b_since_c_implies_d) == Since(a, Since(b, (~c | d)))
 
 
 def test_rewrite_formula_visitor_once():
     """Test the rewrite formula visitor for the once formula."""
-    a = PLTLAtomic("a")
+    a = PLTLAtomic('"a"')
     once_a = Once(a)
     assert rewrite(once_a) == once_a
 
 
 def test_rewrite_formula_visitor_historically():
     """Test the rewrite formula visitor for the historically formula."""
-    a = PLTLAtomic("a")
+    a = PLTLAtomic('"a"')
     historically_a = Historically(a)
     assert rewrite(historically_a) == ~Once(~a)
diff --git a/tests/test_utils/test_val_predicates_visitor.py b/tests/test_utils/test_val_predicates_visitor.py
index c28f460c..32440eff 100644
--- a/tests/test_utils/test_val_predicates_visitor.py
+++ b/tests/test_utils/test_val_predicates_visitor.py
@@ -66,7 +66,7 @@ def test_val_predicates_visitor_and():
     a = PLTLAtomic("a")
     b = PLTLAtomic("b")
 
-    val_a_and_b = Predicate(add_val_prefix("a-and-b"))
+    val_a_and_b = Predicate(add_val_prefix("LPAR__a__RPAR-__AND__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
     val_b = Predicate(add_val_prefix(b.name))
 
@@ -78,7 +78,7 @@ def test_val_predicates_visitor_or():
     a = PLTLAtomic("a")
     b = PLTLAtomic("b")
 
-    val_a_or_b = Predicate(add_val_prefix("a-or-b"))
+    val_a_or_b = Predicate(add_val_prefix("LPAR__a__RPAR-__OR__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
     val_b = Predicate(add_val_prefix(b.name))
 
@@ -89,7 +89,7 @@ def test_val_predicates_visitor_not():
     """Test the val predicates visitor for the not formula."""
     a = PLTLAtomic("a")
 
-    val_not_a = Predicate(add_val_prefix("not-a"))
+    val_not_a = Predicate(add_val_prefix("NOT__LPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
 
     assert val_predicates(~a) == {val_not_a, val_a}
@@ -100,7 +100,7 @@ def test_val_predicates_visitor_before():
     a = PLTLAtomic("a")
     before_a = Before(a)
 
-    val_before_a = Predicate(add_val_prefix("Ya"))
+    val_before_a = Predicate(add_val_prefix("YLPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
 
     assert val_predicates(before_a) == {val_before_a, val_a}
@@ -113,8 +113,10 @@ def test_val_predicates_visitor_since():
     c = PLTLAtomic("c")
     a_since_b_since_c = Since(a, b, c)
 
-    val_a_since_b_since_c = Predicate(add_val_prefix("a-S-b-S-c"))
-    val_b_since_c = Predicate(add_val_prefix("b-S-c"))
+    val_a_since_b_since_c = Predicate(
+        add_val_prefix("LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR")
+    )
+    val_b_since_c = Predicate(add_val_prefix("LPAR__b__RPAR-S-LPAR__c__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
     val_b = Predicate(add_val_prefix(b.name))
     val_c = Predicate(add_val_prefix(c.name))
@@ -133,7 +135,7 @@ def test_val_predicates_visitor_once():
     a = PLTLAtomic("a")
     once_a = Once(a)
 
-    val_once_a = Predicate(add_val_prefix("Oa"))
+    val_once_a = Predicate(add_val_prefix("OLPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix(a.name))
 
     assert val_predicates(once_a) == {val_once_a, val_a}