Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=DrinkVendingMachine-PT-10
export BK_EXAMINATION=CTLMix
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1657
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/DrinkVendingMachine-PT-10
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is DrinkVendingMachine-PT-10, examination is CTLMix'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for DrinkVendingMachine/10 (P/T)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

execution on node 35: cluster1u37.lip6.fr (runId=136937309400912_n_35)
=====================================================================
runnning marcie on DrinkVendingMachine-PT-10 (CTLMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is DrinkVendingMachine-PT-10, examination is CTLMix
=====================================================================

--------------------
content from stdout:

START 1369387566

Marcie rev. 1103M (build: rohrch on 2013-02-17)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4 --mcc-file=CTLMix.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 120 NrTr: 111160)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:1m5sec

init dd package: 0m1sec


RS generation: 0m10sec


-> reachability set: #nodes 273 (2.7e+02) #states 1,152,921,504,606,846,976 (18)



starting CTL model checker
--------------------------

checking: AG [[["wait_9" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_4" \in [1, oo) | ["theProducts_8" \in [1, oo) && "wait_1" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_3" \in [1, oo) | ["theProducts_9" \in [1, oo) && "wait_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_5" \in [1, oo) | "wait_2" \in [1, oo) && "theProducts_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [productSlots_5=theProducts_5 & [productSlots_1=theProducts_1 & [productSlots_2=theProducts_2 & [productSlots_7=theProducts_7 & [productSlots_6=theProducts_6 & [productSlots_4=theProducts_4 & [productSlots_3=theProducts_3 & [productSlots_9=theProducts_9 & [productSlots_8=theProducts_8 & [productSlots_10=theProducts_10 & true]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[productSlots_5=theProducts_5 & [productSlots_1=theProducts_1 & [productSlots_2=theProducts_2 & [productSlots_7=theProducts_7 & [productSlots_6=theProducts_6 & [productSlots_4=theProducts_4 & [productSlots_3=theProducts_3 & [productSlots_9=theProducts_9 & [productSlots_8=theProducts_8 & [productSlots_10=theProducts_10 & true]]]]]]]]]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["wait_2" \in [1, oo) && "theProducts_5" \in [1, oo) | "wait_1" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_7" \in [1, oo)] | "theProducts_9" \in [1, oo) && "wait_1" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_6" \in [1, oo)] | "theProducts_8" \in [1, oo) && "wait_1" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_4" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_10" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_1876_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m2sec

checking: AF [[["wait_9" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_4" \in [1, oo) | ["theProducts_8" \in [1, oo) && "wait_1" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_4" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_5" \in [1, oo) && "theProducts_3" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_5" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_6" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_3" \in [1, oo) | ["theProducts_9" \in [1, oo) && "wait_1" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_10" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_2" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_8" \in [1, oo) | ["wait_2" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_9" \in [1, oo) && "theProducts_7" \in [1, oo) | ["wait_10" \in [1, oo) && "theProducts_9" \in [1, oo) | ["wait_1" \in [1, oo) && "theProducts_5" \in [1, oo) | "wait_2" \in [1, oo) && "theProducts_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [productSlots_5=theProducts_5 & [productSlots_1=theProducts_1 & [productSlots_2=theProducts_2 & [productSlots_7=theProducts_7 & [productSlots_6=theProducts_6 & [productSlots_4=theProducts_4 & [productSlots_3=theProducts_3 & [productSlots_9=theProducts_9 & [productSlots_8=theProducts_8 & [productSlots_10=theProducts_10 & true]]]]]]]]]]]]
normalized: ~ [EG [~ [[[productSlots_5=theProducts_5 & [productSlots_1=theProducts_1 & [productSlots_2=theProducts_2 & [productSlots_7=theProducts_7 & [productSlots_6=theProducts_6 & [productSlots_4=theProducts_4 & [productSlots_3=theProducts_3 & [productSlots_9=theProducts_9 & [productSlots_8=theProducts_8 & [productSlots_10=theProducts_10 & true]]]]]]]]]] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["wait_2" \in [1, oo) && "theProducts_5" \in [1, oo) | "wait_1" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_1" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_10" \in [1, oo) && "theProducts_7" \in [1, oo)] | "theProducts_9" \in [1, oo) && "wait_1" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_9" \in [1, oo) && "theProducts_9" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_10" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_5" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_8" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_7" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_6" \in [1, oo)] | "wait_2" \in [1, oo) && "theProducts_3" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_7" \in [1, oo)] | "