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=GlobalRessAlloc-PT-03
export BK_EXAMINATION=ReachabilityMix
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1658
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/GlobalRessAlloc-PT-03
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is GlobalRessAlloc-PT-03, examination is ReachabilityMix'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for GlobalRessAlloc/03 (P/T)

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

execution on node 2: quadhexa-2.u-paris10.fr (runId=136952151800062_n_2)
=====================================================================
runnning marcie on GlobalRessAlloc-PT-03 (ReachabilityMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is GlobalRessAlloc-PT-03, examination is ReachabilityMix
=====================================================================

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

START 1369528471

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=ReachabilityMix.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 33 NrTr: 4791)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m6sec


RS generation: 0m37sec


-> reachability set: #nodes 3060 (3.1e+03) #states 6,320 (3)



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

checking: AG [[[pr_released_3!=Processes_3 & [pr_released_2!=Processes_2 & [pr_released_1!=Processes_1 & true]]] & ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | [[["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo)]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[true & pr_released_1!=Processes_1] & pr_released_2!=Processes_2] & pr_released_3!=Processes_3] & ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | [["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | [[["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | [[[[["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | [["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | [[[[[[[["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | [["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | [[["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | [[[["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [2, oo) | [[[[[[[[["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | [["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)]]]]]]]] | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo)]] | "pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo)]]] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo)]]]]]]] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo)] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo)] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo)] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_37_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m5sec

checking: AG [[[pr_released_3!=Processes_3 & [pr_released_2!=Processes_2 & [pr_released_1!=Processes_1 & true]]] | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["in_critical_s_2_4" \in [2, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[pr_released_3!=Processes_3 & [pr_released_2!=Processes_2 & [pr_released_1!=Processes_1 & true]]] | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | [[["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | [["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_4" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | [["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | [[[[["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | [[["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | [[["in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | [[["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | [["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)]]]]]]]]]]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)]]] | "pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo)]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)]]]]]]]]]]]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]]]]]] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)]]]]]]]]]

-> the formula is FALSE

FORMULA p_38_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m3sec

checking: AG [[~ [[pr_released_3!=Processes_3 & [pr_released_2!=Processes_2 & [pr_released_1!=Processes_1 & true]]]] & ~ [["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[~ [[[[true & pr_released_1!=Processes_1] & pr_released_2!=Processes_2] & pr_released_3!=Processes_3]] & ~ [["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | "pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_39_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["in_critical_s_2_3" \in [2, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | "pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_4" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_2" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_4" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_1" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_2" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_5" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)]] | ~ [[[[true & pr_released_1!=Processes_1] & pr_released_2!=Processes_2] & pr_released_3!=Processes_3]]]]
normalized: ~ [E [true U ~ [[~ [[[[[[[[[[[[[[[[[[[[[[["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo) | [[["in_critical_s_3_2" \in [2, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_4" \in [2, oo) && "pr_in_2" \in [2, oo) | [[[[[[[["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | [[[["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | [[["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | [[["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | [[[["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | [["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [2, oo) | [[["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | [[[["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | [[["in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [2, oo) | [["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)]]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)]]] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)]]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)]]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)]]]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_1" \in [2, oo)]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)]]]] | "pr_in_3" \in [2, oo) && "in_critical_s_3_1" \in [2, oo)] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [2, oo)]]]] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo)]]] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo)]]]]]] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_3_4" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_2" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)]]]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)]]] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_1" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_2" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_5" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)]] | ~ [[[[true & pr_released_1!=Processes_1] & pr_released_2!=Processes_2] & pr_released_3!=Processes_3]]]]]]

-> the formula is TRUE

FORMULA p_40_mix_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[pr_released_3!=Processes_3 & [pr_released_2!=Processes_2 & [pr_released_1!=Processes_1 & true]]] & ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo) | ["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | [[[[[[[[[[[[[[[[["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_5" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]]] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_1" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_6" \in [2, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_3" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_1" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_3" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_6" \in [2, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_5" \in [2, oo) && "pr_in_2" \in [2, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[true & pr_released_1!=Processes_1] & pr_released_2!=Processes_2] & pr_released_3!=Processes_3] & ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["pr_in_1" \in [2, oo) && "in_critical_s_1_5" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | [[[["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | [[["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo) | ["pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [2, oo) | ["in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | [["in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | [["pr_in_2" \in [2, oo) && "in_critical_s_2_4" \in [2, oo) | [[[[["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | [[["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_2" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo) | [["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | [[["pr_in_1" \in [2, oo) && "in_critical_s_1_3" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_5" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_6" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_3" \in [2, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_1" \in [2, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_6" \in [2, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_1" \in [2, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_4" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_1_3" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_2_3" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | ["in_critical_s_3_6" \in [2, oo) && "pr_in_3" \in [2, oo) | [["in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo) | ["in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo) | [[[[[[[[[[[["in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo) | ["in_critical_s_3_3" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo) | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_5" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_1_1" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_5" \in [2, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_3_1" \in [1, oo) && "in_critical_s_3_6" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_6" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_3_4" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_2_1" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_6" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)] | "in_critical_s_1_2" \in [1, oo) && "in_critical_s_1_4" \in [1, oo) && "pr_in_1" \in [2, oo)]]]]] | "pr_in_3" \in [2, oo) && "in_critical_s_3_2" \in [1, oo) && "in_critical_s_3_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_4" \in [2, oo)]]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_1" \in [1, oo) && "pr_in_3" \in [2, oo)]] | "in_critical_s_1_6" \in [1, oo) && "in_critical_s_1_2" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_2_2" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_3" \in [2, oo) && "in_critical_s_3_4" \in [2, oo)]]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_2" \in [1, oo) && "pr_in_3" \in [2, oo)] | "pr_in_2" \in [2, oo) && "in_critical_s_2_2" \in [2, oo)] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_3" \in [1, oo) && "pr_in_2" \in [2, oo)] | "in_critical_s_2_6" \in [1, oo) && "in_critical_s_2_5" \in [1, oo) && "pr_in_2" \in [2, oo)]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_3" \in [1, oo) && "pr_in_3" \in [2, oo)]]]] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)]]]]]] | "in_critical_s_1_5" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)]]]] | "in_critical_s_3_6" \in [1, oo) && "in_critical_s_3_5" \in [1, oo) && "pr_in_3" \in [2, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_1" \in [2, oo)]]] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_1" \in [1, oo) && "pr_in_1" \in [2, oo)]] | "in_critical_s_3_5" \in [1, oo) && "in_critical_s_3_4" \in [1, oo) && "pr_in_3" \in [2, oo)]]]] | "in_critical_s_1_4" \in [1, oo) && "in_critical_s_1_3" \in [1, oo) && "pr_in_1" \in [2, oo)] | "in_critical_s_2_4" \in [1, oo) && "in_critical_s_2_1" \in [1, oo) && "pr_in_2" \in [2, oo)] | "pr_in_1" \in [2, oo) && "in_critical_s_1_2" \in [2, oo)]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_41_mix_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[pr_in_1!=Processes_1 & [pr_in_2!=Processes_2 & [pr_in_3!=Processes_3 & true]]] & ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_2" \in [1, oo) && "Resources_1" \in [2, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_3" \in [2, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_4" \in [2, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_1" \in [2, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_1" \in [1, oo) | "Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[true & pr_in_3!=Processes_3] & pr_in_2!=Processes_2] & pr_in_1!=Processes_1] & ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | [["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Resources_2" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo) | [["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Processes_3" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [["Processes_2" \in [1, oo) && "Resources_1" \in [2, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | [["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_6" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_3" \in [2, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_4" \in [2, oo) | [["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | [["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | [[["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | [[["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | "Resources_1" \in [2, oo) && "Processes_1" \in [1, oo)]]]]] | "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_5" \in [2, oo) && "Processes_1" \in [1, oo)]] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)]]]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)]]]]]] | "Processes_3" \in [1, oo) && "Resources_1" \in [2, oo)]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo)]]]] | "Resources_6" \in [2, oo) && "Processes_3" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)]]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo)]]]]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)]]] | "Resources_4" \in [2, oo) && "Processes_1" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)]]]]]]]]]] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo)]]]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]]]] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)]] | "Resources_2" \in [2, oo) && "Processes_3" \in [1, oo)]]] | "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]]]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]]]]] | "Resources_6" \in [2, oo) && "Processes_2" \in [1, oo)]]]]]]]]] | "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_42_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[pr_in_1!=Processes_1 & [pr_in_2!=Processes_2 & [pr_in_3!=Processes_3 & true]]] | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_2" \in [2, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_1" \in [1, oo) | ["Processes_2" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_4" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_5" \in [2, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_1" \in [1, oo) | "Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[true & pr_in_3!=Processes_3] & pr_in_2!=Processes_2] & pr_in_1!=Processes_1] | ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [[[["Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | [[["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | [[[[["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | [[[["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [[[[[[["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | [["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo) | [[[["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | [[[["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo) | [[[["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Processes_2" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_4" \in [2, oo) && "Processes_3" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_5" \in [2, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_1" \in [2, oo) && "Processes_1" \in [1, oo) | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)]]]]]]]]]]]]]]]]]]]]] | "Resources_6" \in [2, oo) && "Processes_1" \in [1, oo)] | "Resources_6" \in [2, oo) && "Processes_3" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)]]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_4" \in [2, oo) && "Processes_1" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)]]] | "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_1" \in [2, oo) && "Processes_2" \in [1, oo)] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo)]]]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)]] | "Processes_3" \in [1, oo) && "Resources_2" \in [2, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)]]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo)]]]] | "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo)] | "Resources_6" \in [2, oo) && "Processes_2" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [2, oo)]] | "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]]]]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo)]]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo)]]] | "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_43_mix_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m4sec

checking: AG [[[pr_in_1!=Processes_1 & [pr_in_2!=Processes_2 & [pr_in_3!=Processes_3 & true]]] & ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_3" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [2, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_2" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_3" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_6" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) | ["Resources_4" \in [1, oo) && "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) | ["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) | ["Resources_1" \in [2, oo) && "Processes_1" \in [1, oo) | "Resources_4" \in [1, oo) && "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | [[["Resources_5" \in [2, oo) && "Processes_3" \in [1, oo) | [["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [2, oo) && "Processes_1" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_2" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo) | [[[["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_2" \in [2, oo) && "Processes_3" \in [1, oo) | [[[[[[[[[["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | ["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_1" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | [["Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [[["Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_1" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo) | [[[["Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | [["Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo) | [["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo) | [["Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_6" \in [2, oo) && "Processes_3" \in [1, oo) | [["Resources_3" \in [2, oo) && "Processes_2" \in [1, oo) | ["Resources_4" \in [2, oo) && "Processes_3" \in [1, oo) | [[[["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo) | [[[[["Resources_5" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo) | ["Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo) | [[["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | ["Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo) | [[[[["Resources_5" \in [2, oo) && "Processes_2" \in [1, oo) | [["Resources_1" \in [2, oo) && "Processes_1" \in [1, oo) | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_2" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_5" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_5" \in [2, oo) && "Processes_1" \in [1, oo)]]] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)]]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)]]] | "Resources_1" \in [2, oo) && "Processes_3" \in [1, oo)] | "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo)]]] | "Resources_6" \in [2, oo) && "Processes_1" \in [1, oo)]]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_4" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo)]]] | "Resources_2" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_1" \in [1, oo)]] | "Resources_4" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_5" \in [1, oo)]]] | "Resources_4" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)]]] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)]]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)] | "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_2" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo)] | "Processes_3" \in [1, oo) && "Resources_3" \in [2, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_4" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)] | "Resources_4" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_1" \in [1, oo)]] | "Processes_3" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_5" \in [1, oo)]] | "Resources_3" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_2" \in [1, oo)] | "Resources_2" \in [2, oo) && "Processes_2" \in [1, oo)]]]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)]]]]]]] | "Resources_3" \in [2, oo) && "Processes_1" \in [1, oo)] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)]]]]] | "Resources_1" \in [1, oo) && "Processes_1" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_3" \in [1, oo) && "Resources_2" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)] | "Processes_1" \in [1, oo) && "Resources_3" \in [1, oo) && "Resources_4" \in [1, oo)]]] | "Resources_5" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_1" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_6" \in [1, oo)]] | "Resources_2" \in [1, oo) && "Processes_2" \in [1, oo) && "Resources_5" \in [1, oo)] & [[[true & pr_in_3!=Processes_3] & pr_in_2!=Processes_2] & pr_in_1!=Processes_1]]]]]

-> the formula is FALSE

FORMULA p_44_mix_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m24sec

STOP 1369528556

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

133 170 176 207 233 240 247 259 269 274 281 287 291 295 300 318 318 328 328 336 338 351 346 346 354 354 385 390 386 389 388 385 405 403 399 403 410 409 408 409 410 411 408 407 405 403 400 407 414 420 427 445 444 445 447 448 457 458 460 460 464 467 467 467 474 475 485 485 493 493 497 500 501 510 508 508 518 518 522 524 523 522 526 525 529 532 532 540 539 552 552 567 565 577 570 578 578 584 591 591 602 606 612 614 615 616 621 620 625 635 635 640 641 641 649 662 657 657 669 662 664 665 670 672 673 673 679 689 685 685 688 690 691 691 696 697 697 707 707 721 717 717 728 720 724 727 727 733 737 737 746 746 757 752 752 760 760 773 773 766 766 773 789 785 779 779 788 788 803 803 800 797 797 801 801 801 805 805 808 808 814 814 814 818 818 818 818 857 857 857 890 890 896 896 899 899 901 908 903 903 903 942 940 940 938 936 936 934 940 940 946 946 951 954 954 962 962 967 965 965 967 967 976 976 971 975 975 973 973 981 981 981 981 1020 1017 1014 1011 1011 1016 1021 1021 1023 1029 1023 1025 1025 1030 1027 1033 1027 1041 1030 1030 1035 1032 1032 1035 1035 1035 1079 1072 1063 1063 1065 1069 1069 1071 1071 1071 1081 1071 1078 1074 1072 1072 1077 1072 1078 1074 1082 1080 1080 1080 1324 1316 1304 1299 1284 1280 1276 1272 1271 1268 1257 1252 1248 1248 1244 1240 1240 1236 1240 1240 1244 1244 1250 1253 1248 1252 1252 1266 1259 1259 1264 1268 1262 1268 1266 1266 1269 1271 1271 1275 1275 1273 1278 1276 1276 1279 1282 1282 1289 1286 1294 1286 1302 1291 1291 1298 1293 1297 1294 1294 1296 1298 1298 1304 1301 1306 1303 1303 1309 1326 1319 1319 1312 1312 1314 1314 1314 1315 1315 1315 1319 1321 1321 1323 1323 1324 1324 1324 1474 1470 1467 1463 1454 1452 1450 1448 1446 1461 1468 1464 1464 1464 1463 1462 1453 1449 1449 1448 1444 1434 1433 1404 1394 1396 1390 1392 1385 1387 1382 1384 1376 1376 1370 1370 1374 1374 1378 1384 1387 1381 1391 1385 1392 1385 1385 1397 1399 1388 1395 1394 1388 1400 1395 1397 1398 1386 1386 1390 1391 1386 1386 1395 1389 1390 1390 1390 1390 1394 1388 1388 1386 1386 1388 1388 1390 1390 1396 1388 1388 1394 1388 1389 1389 1401 1389 1389 1399 1397 1389 1389 1394 1395 1390 1389 1389 1398 1386 1395 1389 1390 1381 1384 1385 1380 1380 1379 1390 1387 1375 1376 1376 1386 1386 1375 1377 1377 1388 1388 1378 1378 1377 1394 1389 1385 1372 1372 1372 1370 1370 1371 1371 1373 1373 1377 1377 1383 1379 1379 1382 1382 1384 1384 1397 1397 1390 1390 1395 1391 1391 1392 1392 1394 1394 1401 1397 1397 1394 1394 1394 1381 1381 1381 1427 1423 1423 1419 1416 1413 1410 1410 1410 1414 1418 1418 1425 1421 1421 1423 1423 1422 1445 1433 1426 1432 1427 1427 1433 1427 1430 1430 1429 1429 1429 1429 1661 1654 1652 1645 1642 1636 1630 1622 1617 1613 1609 1608 1606 1606 1601 1593 1588 1585 1585 1582 1584 1579 1576 1576 1573 1573 1573 1573 1573 1577 1574 1574 1571 1571 1576 1570 1570 1574 1571 1571 1576 1573 1573 1573 1570 1570 1573 1576 1570 1574 1571 1571 1575 1584 1584 1576 1576 1576 1576 1577 1577 1582 1582 1579 1579 1586 1578 1594 1584 1577 1577 1580 1580 1577 1577 1583 1580 1580 1580 1579 1578 1578 1581 1581 1577 1580 1576 1576 1576 1579 1588 1588 1580 1580 1580 1585 1587 1587 1587 1587 1587 1587 1587 1588 1588 1588 1627 1626 1625 1624 1625 1622 1623 1620 1620 1621 1618 1619 1616 1616 1618 1618 1621 1621 1626 1623 1623 1631 1627 1633 1625 1643 1634 1634 1628 1631 1631 1628 1628 1634 1627 1631 1624 1631 1628 1628 1628 1666 1664 1664 1662 1665 1660 1658 1658 1658 1660 1660 1662 1663 1663 1662 1662 1662 1693 1693 1693 1693 1724 1724 1724 1730 1733 1733 1736 1736 1740 1740 1740 1785 1775 1774 1774 1773 1773 1772 1771 1771 1777 1783 1783 1788 1788 1792 1792 1800 1800 1805 1804 1804 1807 1807 1818 1818 1815 1815 1821 1823 1820 1827 1826 1826 1826 1873 1868 1863 1861 1857 1857 1862 1862 1867 1867 1870 1872 1872 1876 1876 1881 1879 1879 1881 1881 1890 1887 1887 1892 1890 1890 1893 1893 1893 2047 2044 2040 2038 2031 2028 2025 2022 2025 2021 2017 2014 2012 2012 2010 2008 2008 2006 2006 2009 2011 2011 2015 2013 2013 2015 2015 2028 2024 2020 2029 2025 2023 2023 2028 2026 2030 2030 2032 2032 2036 2036 2034 2034 2040 2038 2038 2043 2052 2052 2045 2045 2047 2047 2047 2052 2052 2054 2061 2056 2064 2059 2059 2059 2099 2096 2097 2094 2096 2092 2092 2093 2090 2092 2088 2088 2089 2086 2086 2090 2090 2094 2099 2099 2096 2096 2104 2099 2107 2101 2125 2119 2113 2108 2108 2114 2116 2111 2118 2118 2112 2118 2113 2113 2117 2117 2117 2117 2154 2150 2148 2148 2146 2146 2144 2144 2148 2148 2151 2151 2154 2154 2156 2156 2156 2178 2178 2178 2225 2201 2201 2201 2204 2203 2203 2210 2203 2205 2205 2205 2205 2246 2244 2239 2241 2237 2232 2232 2228 2228 2231 2235 2235 2238 2238 2239 2257 2240 2240 2244 2239 2239 2246 2238 2255 2245 2246 2239 2245 2245 2241 2241 2248 2243 2243 2243 2287 2284 2281 2279 2267 2267 2270 2270 2274 2282 2277 2276 2276 2283 2277 2282 2276 2276 2277 2277 2291 2285 2279 2283 2284 2278 2282 2276 2276 2276 2421 2422 2411 2412 2402 2394 2390 2385 2385 2378 2375 2368 2364 2364 2359 2360 2355 2351 2351 2350 2350 2348 2351 2351 2346 2346 2344 2344 2354 2348 2343 2348 2346 2348 2342 2345 2341 2341 2342 2351 2341 2350 2345 2347 2342 2348 2344 2344 2346 2346 2355 2345 2345 2345 2344 2344 2344 2347 2347 2345 2351 2345 2345 2348 2348 2348 2390 2387 2386 2385 2384 2385 2382 2385 2377 2377 2378 2375 2375 2372 2372 2372 2375 2375 2380 2380 2383 2378 2378 2386 2380 2380 2383 2383 2405 2391 2391 2386 2386 2392 2394 2389 2394 2394 2387 2391 2385 2392 2387 2387 2387 2423 2425 2421 2416 2416 2414 2414 2409 2409 2409 2412 2422 2414 2423 2416 2424 2417 2417 2417 2443 2443 2443 2483 2476 2469 2469 2473 2482 2474 2479 2474 2474 2474 2474 2474 2520 2515 2510 2511 2508 2509 2506 2503 2503 2500 2500 2502 2506 2506 2509 2515 2509 2509 2520 2510 2515 2515 2511 2516 2509 2509 2519 2512 2512 2507 2512 2511 2512 2507 2507 2514 2510 2510 2510 2547 2544 2544 2541 2542 2539 2539 2536 2536 2536 2538 2540 2540 2548 2541 2547 2540 2540 2540 2563 2563 2563 2600 2593 2586 2586 2590 2590 2591 2591 2598 2591 2595 2590 2590 2590 2633 2628 2626 2621 2621 2622 2619 2616 2616 2613 2613 2615 2619 2619 2623 2623 2622 2622 2633 2624 2628 2628 2625 2625 2630 2623 2633 2632 2625 2620 2620 2623 2623 2624 2619 2626 2622 2622 2622 2655 2656 2653 2653 2650 2651 2648 2648 2645 2645 2645 2647 2651 2651 2659 2652 2652 2649 2649 2649 2669 2669 2669 2669 2707 2700 2690 2690 2693 2693 2695 2695 2700 2695 2695 2694 2694 2694 2744 2736 2729 2731 2727 2727 2728 2722 2719 2719 2715 2715 2718 2722 2722 2725 2725 2732 2726 2743 2736 2729 2735 2735 2731 2731 2736 2730 2730 2742 2740 2734 2729 2729 2733 2733 2734 2728 2735 2730 2730 2730 2765 2766 2763 2763 2760 2760 2761 2755 2750 2750 2750 2753 2753 2755 2755 2763 2757 2757 2758 2758 2758 2782 2782 2782 2782 2820 2813 2813 2806 2806 2808 2808 2807 2812 2812 2808 2808 2811 2811 2811 2811 2831 2831 2831 2868 2868 2861 2861 2851 2851 2854 2854 2855 2863 2861 2863 2857 2864 2859 2859 2859 2879 2879 2879 2879 2915 2908 2908 2901 2901 2903 2903 2901 2901 2905 2901 2901 2908 2904 2904 2904 2925 2925 2925 2974 2963 2963 2956 2956 2948 2948 2950 2950 2948 2948 2952 2952 2953 2948 2955 2951 2951 2951 2951 2975 2975 2975 2975 2998 2998 2998 2998 3020 3020 3020 3020 3041 3041 3041 3041 3041 3060 3060 3060 3060 3060
iterations count:1481071 (309), effective:2245 (0)

initing FirstDep: 0m0sec

3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)
649 739 882 882 953 953 1003 1024 1024 1034 1181 1181 1215 1215 1239 1237 1237 1312 1326 1326 1326 1326 1358 1359 1359 1357 1357 1659 1659 1659 1659 1813 1813 1813 1915 1915 1915 1981 1981 1981 2005 2005 2005 2355 2355 2355 2355 2452 2452 2452 2517 2517 2517 2543 2543 2543 2804 2804 2804 2856 2856 2856 2856 2879 2879 2879 3008 3008 3008 3032 3032 3032 3060 3060 3060 3060
iterations count:76932 (16), effective:35 (0)
3179 3179 3115 3115 3060 3060 3060 3060 3060
iterations count:9196 (1), effective:23 (0)
3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)
3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)
3843 3842 3842 3810 3727 3727 3729 3727 3727 3727 3728 3727 3729 3727 3727 3727 3728 3698 3475 3475 3068 3079 3078 3077 3069 3069 3069 3060 3060 3060 3060
iterations count:31098 (6), effective:116 (0)
3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)

--------------------
content from /tmp/BenchKit_head_log_file.1658: