From bac485a1e21b02b7c836e3d175c81b66834a477c Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 9 Jul 2023 21:28:30 +0200 Subject: [PATCH] fix: use simplified mapping After this commit, there is no need to provide an explicit mapping, since it is assumed that the propositions *are* the ground fluents. E.g. if previously the formula was specified as follows: formula = "on_b_a & O(ontable_c)" Now we require that the propositions can be interpreted as PDDL predicates, i.e.: formula = '"on b a" & O("ontable c")' Pylogics does not allow spaces in the proposition name; therefore, the double quotes are always required. Only exception is when the predicate is unary: formula = 'Y(O(made-p4)))' (as in openstacks). --- README.md | 2 +- plan4past/__main__.py | 22 +-- plan4past/compiler.py | 38 +--- plan4past/helpers/utils.py | 52 +++-- plan4past/utils/derived_visitor.py | 62 ++---- plan4past/utils/mapping_parser.py | 186 ------------------ plan4past/utils/rewrite_formula_visitor.py | 4 + plan4past/utils/val_predicates_visitor.py | 2 +- .../BF/elevators_ppltl/elevators_teg.json | 58 +++--- tests/test_compiler/test_blocksworld_det.py | 2 +- tests/test_compiler/test_readme_example.py | 21 +- tests/test_helpers/test_utils.py | 22 --- tests/test_utils/test_derived_visitor.py | 60 +++--- tests/test_utils/test_mapping_parser.py | 168 ---------------- .../test_rewrite_formula_visitor.py | 44 ++--- 15 files changed, 152 insertions(+), 591 deletions(-) delete mode 100644 plan4past/utils/mapping_parser.py delete mode 100644 tests/test_utils/test_mapping_parser.py 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..cb9478ba 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) diff --git a/plan4past/helpers/utils.py b/plan4past/helpers/utils.py index a1b47738..3175f59f 100644 --- a/plan4past/helpers/utils.py +++ b/plan4past/helpers/utils.py @@ -21,13 +21,14 @@ # """Miscellanea utilities.""" -from typing import Dict +import re 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})" +) def add_val_prefix(name: str): @@ -65,19 +66,6 @@ def replace_symbols(name: str): ) -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: """ User-defined assert. @@ -88,3 +76,33 @@ def check_(condition: bool, message: str = "") -> None: """ if not condition: raise AssertionError(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 validate(symbol: str) -> None: + """ + Validate a symbol. + + :param symbol: the symbol + """ + # 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..e0be5143 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,39 @@ ) from pylogics.utils.to_string import to_string -from plan4past.helpers.utils import add_val_prefix, replace_symbols +from plan4past.helpers.utils import 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 +80,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,45 +94,39 @@ 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])))) @@ -153,14 +135,12 @@ def derived_predicates_since( Predicate(f"Y-{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))) @@ -168,5 +148,5 @@ def derived_predicates_once( Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))), Predicate(f"Y-{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 . -# - -"""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 ','", 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/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/test_compiler/test_blocksworld_det.py b/tests/test_compiler/test_blocksworld_det.py index 2e412a3c..a99bb5a9 100644 --- a/tests/test_compiler/test_blocksworld_det.py +++ b/tests/test_compiler/test_blocksworld_det.py @@ -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..755f1735 100644 --- a/tests/test_helpers/test_utils.py +++ b/tests/test_helpers/test_utils.py @@ -22,37 +22,15 @@ """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" diff --git a/tests/test_utils/test_derived_visitor.py b/tests/test_utils/test_derived_visitor.py index aa299c92..3035bb27 100644 --- a/tests/test_utils/test_derived_visitor.py +++ b/tests/test_utils/test_derived_visitor.py @@ -62,7 +62,7 @@ def test_derived_predicates_visitor_not_implemented_fail(): with pytest.raises( NotImplementedError, match="handler not implemented for object " ): - derived_predicates(1, {}) + derived_predicates(1) def test_derived_predicates_visitor_true(): @@ -70,7 +70,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,32 +79,32 @@ 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) def test_derived_predicates_visitor_atomic(): """Test the derived predicates visitor for the atomic formula.""" - a = PLTLAtomic("a") - val = Predicate(add_val_prefix("a")) + a = PLTLAtomic('"a"') + val = Predicate(add_val_prefix('"a"')) condition = Predicate("p", Constant("a")) expected = {DerivedPredicate(val, condition)} - actual = derived_predicates(a, {a: condition}) + actual = derived_predicates(a) assert _eq(actual, expected) def test_derived_predicates_visitor_and(): """Test the derived predicates visitor for the and formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') condition_a = Predicate("p", Constant("a")) condition_b = Predicate("p", Constant("b")) val = Predicate(add_val_prefix("a-and-b")) - val_a = Predicate(add_val_prefix("a")) - val_b = Predicate(add_val_prefix("b")) + val_a = Predicate(add_val_prefix('"a"')) + val_b = Predicate(add_val_prefix('"b"')) condition = And(val_a, val_b) @@ -114,21 +114,21 @@ 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) def test_derived_predicates_visitor_or(): """Test the derived predicates visitor for the or formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') condition_a = Predicate("p", Constant("a")) condition_b = Predicate("p", Constant("b")) val = Predicate(add_val_prefix("a-or-b")) - val_a = Predicate(add_val_prefix("a")) - val_b = Predicate(add_val_prefix("b")) + val_a = Predicate(add_val_prefix('"a"')) + val_b = Predicate(add_val_prefix('"b"')) condition = Or(val_a, val_b) @@ -138,30 +138,30 @@ 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) def test_derived_predicates_visitor_not(): """Test the derived predicates visitor for the not formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') condition_a = Predicate("p", Constant("a")) val = Predicate(add_val_prefix("not-a")) - val_a = Predicate(add_val_prefix("a")) + 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) def test_derived_predicates_visitor_before(): """Test the derived predicates visitor for the before formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"p a"') Ya = Before(a) condition_a = Predicate("p", Constant("a")) @@ -173,19 +173,19 @@ def test_derived_predicates_visitor_before(): expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)} - actual = derived_predicates(Ya, {a: condition_a}) + actual = derived_predicates(Ya) assert _eq(actual, expected) def test_derived_predicates_visitor_since(): """Test the derived predicates visitor for the since formula.""" - a = PLTLAtomic("a") - b = PLTLAtomic("b") + a = PLTLAtomic('"a"') + b = PLTLAtomic('"b"') c = PLTLAtomic("c") a_since_b_since_c = Since(a, b, c) - val_a = Predicate(add_val_prefix("a")) - val_b = Predicate(add_val_prefix("b")) + 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")) @@ -206,18 +206,16 @@ 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) def test_derived_predicates_visitor_once(): """Test the derived predicates visitor for the once formula.""" - a = PLTLAtomic("a") + a = PLTLAtomic('"a"') once_a = Once(a) - val_a = Predicate(add_val_prefix("a")) + val_a = Predicate(add_val_prefix('"a"')) val_once_a = Predicate(add_val_prefix("Oa")) Y_once_a = Predicate("Y-Oa") @@ -229,5 +227,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 . -# - -"""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 ','", - ): - 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 ','", - ): - 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_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)