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

Execution Outputs of marcie for SharedMemory/000010 (P/T)

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

execution on node 4: quadhexa-2.u-paris10.fr (runId=136983895000056_n_4)
=====================================================================
runnning marcie on SharedMemory-PT-000010 (ReachabilityFireability)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is SharedMemory-PT-000010, examination is ReachabilityFireability
=====================================================================

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

START 1369845781

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 131 NrTr: 210)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m6sec


RS generation: 0m0sec


-> reachability set: #nodes 2681 (2.7e+03) #states 1,830,519 (6)



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

checking: AG [[[["Ext_Mem_Acc_8_1" \in [1, oo) | [[["Ext_Mem_Acc_6_3" \in [1, oo) | [[[[["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | [["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | [["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | [["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | [["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | [[["Ext_Mem_Acc_4_10" \in [1, oo) | [[[["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | [[["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | ["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | [["Ext_Mem_Acc_4_3" \in [1, oo) | [["Ext_Mem_Acc_7_3" \in [1, oo) | [["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | [[["Ext_Mem_Acc_3_1" \in [1, oo) | [[[["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | ["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)]] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)]]] | "Ext_Mem_Acc_5_2" \in [1, oo)]] | "Ext_Mem_Acc_2_9" \in [1, oo)]] | "Ext_Mem_Acc_10_7" \in [1, oo)]]]]] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)]]] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)]] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)]]]] | "Ext_Mem_Acc_9_7" \in [1, oo)]]]]]] | "Ext_Mem_Acc_9_10" \in [1, oo)]]]]] | "Ext_Mem_Acc_2_7" \in [1, oo)]]] | "Ext_Mem_Acc_6_7" \in [1, oo)]]]]]] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)]] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)]] | "Ext_Mem_Acc_10_8" \in [1, oo)] & ["Active_3" \in [1, oo) | ["Active_8" \in [1, oo) | ["Active_4" \in [1, oo) | ["Active_2" \in [1, oo) | ["Active_6" \in [1, oo) | [["Active_10" \in [1, oo) | ["Active_5" \in [1, oo) | ["Active_7" \in [1, oo) | "Active_9" \in [1, oo)]]] | "Active_1" \in [1, oo)]]]]]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | [["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | [[[["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | [["Ext_Mem_Acc_2_9" \in [1, oo) | ["Ext_Mem_Acc_7_3" \in [1, oo) | ["Ext_Mem_Acc_5_2" \in [1, oo) | [[["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | [["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | [[[[[[["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | ["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)]]]] | "Ext_Mem_Acc_3_1" \in [1, oo)]]] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)]]]] | "Ext_Mem_Acc_4_3" \in [1, oo)]]] | "Ext_Mem_Acc_5_1" \in [1, oo)] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)]]]] | "Ext_Mem_Acc_7_5" \in [1, oo)]]]] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)] & ["Active_3" \in [1, oo) | ["Active_8" \in [1, oo) | ["Active_4" \in [1, oo) | ["Active_2" \in [1, oo) | ["Active_6" \in [1, oo) | [["Active_10" \in [1, oo) | ["Active_5" \in [1, oo) | ["Active_7" \in [1, oo) | "Active_9" \in [1, oo)]]] | "Active_1" \in [1, oo)]]]]]]]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | ["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | [["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | [["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | [[[[[[[[[["Ext_Mem_Acc_7_3" \in [1, oo) | [[[[[[["Ext_Mem_Acc_2_8" \in [1, oo) | [[["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | [[[[[["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | [["Ext_Mem_Acc_3_4" \in [1, oo) | [["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | [[[[["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | [[[["Ext_Mem_Acc_4_2" \in [1, oo) | [["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | [["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)]] | "Ext_Mem_Acc_9_3" \in [1, oo)]]] | "Ext_Mem_Acc_4_8" \in [1, oo)]] | "Ext_Mem_Acc_10_6" \in [1, oo)] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)]]] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)] | "Ext_Mem_Acc_10_3" \in [1, oo)]]] | "Ext_Mem_Acc_4_1" \in [1, oo)]] | "Ext_Mem_Acc_2_3" \in [1, oo)]]] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)]]] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)]] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)]] | "Ext_Mem_Acc_2_9" \in [1, oo)] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)] | "Ext_Mem_Acc_5_1" \in [1, oo)] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)]]] | "Ext_Mem_Acc_8_4" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_9_7" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ["Active_3" \in [1, oo) | ["Active_8" \in [1, oo) | ["Active_4" \in [1, oo) | [["Active_6" \in [1, oo) | ["Active_1" \in [1, oo) | [[["Active_9" \in [1, oo) | "Active_7" \in [1, oo)] | "Active_5" \in [1, oo)] | "Active_10" \in [1, oo)]]] | "Active_2" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[[[[["Active_2" \in [1, oo) | [[["Active_10" \in [1, oo) | ["Active_5" \in [1, oo) | ["Active_7" \in [1, oo) | "Active_9" \in [1, oo)]]] | "Active_1" \in [1, oo)] | "Active_6" \in [1, oo)]] | "Active_4" \in [1, oo)] | "Active_8" \in [1, oo)] | "Active_3" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_9_7" \in [1, oo) | [[[[[[[[["Ext_Mem_Acc_8_4" \in [1, oo) | [[["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | ["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | ["Ext_Mem_Acc_2_9" \in [1, oo) | [["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | [["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | [[["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | [[["Ext_Mem_Acc_2_3" \in [1, oo) | [["Ext_Mem_Acc_4_1" \in [1, oo) | [[["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | [[["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | [["Ext_Mem_Acc_4_8" \in [1, oo) | [[["Ext_Mem_Acc_9_3" \in [1, oo) | [["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)]] | "Ext_Mem_Acc_3_8" \in [1, oo)] | "Ext_Mem_Acc_9_4" \in [1, oo)]] | "Ext_Mem_Acc_4_2" \in [1, oo)]]]] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)]]]]] | "Ext_Mem_Acc_9_6" \in [1, oo)] | "Ext_Mem_Acc_1_10" \in [1, oo)]] | "Ext_Mem_Acc_3_4" \in [1, oo)]] | "Ext_Mem_Acc_5_4" \in [1, oo)] | "Ext_Mem_Acc_8_3" \in [1, oo)]]]]]] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)]]] | "Ext_Mem_Acc_2_8" \in [1, oo)]]]]]]] | "Ext_Mem_Acc_7_3" \in [1, oo)]]]]]]]]]] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)]] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)]] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[[[["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | [[["Ext_Mem_Acc_7_10" \in [1, oo) | [[[[["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | [[[[[["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | [[[[[["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | [[[[[["Ext_Mem_Acc_8_5" \in [1, oo) | [["Ext_Mem_Acc_4_5" \in [1, oo) | [["Ext_Mem_Acc_1_2" \in [1, oo) | [[[[[[["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | [[[["Ext_Mem_Acc_8_2" \in [1, oo) | [[["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | [[["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | [["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_1_10" \in [1, oo)]]] | "Ext_Mem_Acc_2_3" \in [1, oo)] | "Ext_Mem_Acc_5_4" \in [1, oo)]]]] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)]] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)] | "Ext_Mem_Acc_5_6" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_7_3" \in [1, oo)] | "Ext_Mem_Acc_2_9" \in [1, oo)] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)] | "Ext_Mem_Acc_5_1" \in [1, oo)]] | "Ext_Mem_Acc_1_4" \in [1, oo)]] | "Ext_Mem_Acc_2_10" \in [1, oo)]] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)]]]]]] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)]]]] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)]]]] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)]] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)]]] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)]] & ~ [["Active_3" \in [1, oo) | ["Active_8" \in [1, oo) | ["Active_4" \in [1, oo) | ["Active_2" \in [1, oo) | ["Active_6" \in [1, oo) | ["Active_1" \in [1, oo) | ["Active_10" \in [1, oo) | [["Active_9" \in [1, oo) | "Active_7" \in [1, oo)] | "Active_5" \in [1, oo)]]]]]]]]]]]
normalized: ~ [E [true U ~ [[~ [[[[[[["Active_1" \in [1, oo) | [["Active_5" \in [1, oo) | ["Active_9" \in [1, oo) | "Active_7" \in [1, oo)]] | "Active_10" \in [1, oo)]] | "Active_6" \in [1, oo)] | "Active_2" \in [1, oo)] | "Active_4" \in [1, oo)] | "Active_8" \in [1, oo)] | "Active_3" \in [1, oo)]] & ~ [["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | [[["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | [["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | [[[["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | [[[["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | [[[[[["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | [["Ext_Mem_Acc_2_10" \in [1, oo) | [["Ext_Mem_Acc_1_4" \in [1, oo) | [["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | ["Ext_Mem_Acc_2_9" \in [1, oo) | ["Ext_Mem_Acc_7_3" \in [1, oo) | [[[[[[[[["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | [["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | [[[["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | [[["Ext_Mem_Acc_1_10" \in [1, oo) | [[[[[[[[[[[[[[[[["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)] | "Ext_Mem_Acc_9_3" \in [1, oo)] | "Ext_Mem_Acc_3_8" \in [1, oo)] | "Ext_Mem_Acc_9_4" \in [1, oo)] | "Ext_Mem_Acc_4_8" \in [1, oo)] | "Ext_Mem_Acc_4_2" \in [1, oo)] | "Ext_Mem_Acc_10_6" \in [1, oo)] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)] | "Ext_Mem_Acc_10_3" \in [1, oo)] | "Ext_Mem_Acc_9_6" \in [1, oo)]] | "Ext_Mem_Acc_4_1" \in [1, oo)] | "Ext_Mem_Acc_3_4" \in [1, oo)]]] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)]]] | "Ext_Mem_Acc_8_2" \in [1, oo)]]]] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)]]]]]]] | "Ext_Mem_Acc_1_2" \in [1, oo)]] | "Ext_Mem_Acc_4_5" \in [1, oo)]] | "Ext_Mem_Acc_8_5" \in [1, oo)]]]]]] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)]]]]]] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)]]]]]] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)]]]]] | "Ext_Mem_Acc_7_10" \in [1, oo)]]] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)]]]]]]]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [["Active_3" \in [1, oo) | ["Active_8" \in [1, oo) | ["Active_4" \in [1, oo) | ["Active_2" \in [1, oo) | [[[[["Active_9" \in [1, oo) | "Active_7" \in [1, oo)] | "Active_5" \in [1, oo)] | "Active_10" \in [1, oo)] | "Active_1" \in [1, oo)] | "Active_6" \in [1, oo)]]]]]] | ~ [[[[[[[[[["Ext_Mem_Acc_7_10" \in [1, oo) | [["Ext_Mem_Acc_6_2" \in [1, oo) | [[[["Ext_Mem_Acc_6_7" \in [1, oo) | [[[["Ext_Mem_Acc_7_9" \in [1, oo) | [[[[[["Ext_Mem_Acc_1_9" \in [1, oo) | [["Ext_Mem_Acc_9_1" \in [1, oo) | [[[["Ext_Mem_Acc_5_10" \in [1, oo) | [["Ext_Mem_Acc_4_6" \in [1, oo) | [["Ext_Mem_Acc_4_10" \in [1, oo) | [["Ext_Mem_Acc_7_1" \in [1, oo) | [[[["Ext_Mem_Acc_2_10" \in [1, oo) | [[[["Ext_Mem_Acc_5_1" \in [1, oo) | [[[["Ext_Mem_Acc_2_9" \in [1, oo) | [[[["Ext_Mem_Acc_6_8" \in [1, oo) | [["Ext_Mem_Acc_6_1" \in [1, oo) | [["Ext_Mem_Acc_2_8" \in [1, oo) | [["Ext_Mem_Acc_5_6" \in [1, oo) | [[[["Ext_Mem_Acc_10_5" \in [1, oo) | [[[[[[[[[[["Ext_Mem_Acc_10_3" \in [1, oo) | [[[[[["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | [[[[["Ext_Mem_Acc_3_8" \in [1, oo) | [[["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)] | "Ext_Mem_Acc_9_3" \in [1, oo)]] | "Ext_Mem_Acc_9_4" \in [1, oo)] | "Ext_Mem_Acc_4_8" \in [1, oo)] | "Ext_Mem_Acc_4_2" \in [1, oo)] | "Ext_Mem_Acc_10_6" \in [1, oo)]]] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)]] | "Ext_Mem_Acc_9_6" \in [1, oo)] | "Ext_Mem_Acc_1_10" \in [1, oo)] | "Ext_Mem_Acc_4_1" \in [1, oo)] | "Ext_Mem_Acc_3_4" \in [1, oo)] | "Ext_Mem_Acc_2_3" \in [1, oo)] | "Ext_Mem_Acc_5_4" \in [1, oo)] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)]] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)]] | "Ext_Mem_Acc_2_5" \in [1, oo)]] | "Ext_Mem_Acc_3_1" \in [1, oo)]] | "Ext_Mem_Acc_4_9" \in [1, oo)]] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)] | "Ext_Mem_Acc_7_3" \in [1, oo)]] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)]] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)]] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)]] | "Ext_Mem_Acc_9_2" \in [1, oo)]] | "Ext_Mem_Acc_6_10" \in [1, oo)]] | "Ext_Mem_Acc_9_8" \in [1, oo)]] | "Ext_Mem_Acc_10_9" \in [1, oo)] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)]] | "Ext_Mem_Acc_2_6" \in [1, oo)]] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)]] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)]] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)]] | "Ext_Mem_Acc_7_8" \in [1, oo)]] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[~ [["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | [["Ext_Mem_Acc_7_8" \in [1, oo) | [["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | [["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | [["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | [["Ext_Mem_Acc_2_6" \in [1, oo) | [["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | ["Ext_Mem_Acc_10_9" \in [1, oo) | [["Ext_Mem_Acc_9_8" \in [1, oo) | [["Ext_Mem_Acc_6_10" \in [1, oo) | [["Ext_Mem_Acc_9_2" \in [1, oo) | [["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | [["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | [["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | [["Ext_Mem_Acc_7_3" \in [1, oo) | ["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | [["Ext_Mem_Acc_4_9" \in [1, oo) | [["Ext_Mem_Acc_3_1" \in [1, oo) | [["Ext_Mem_Acc_2_5" \in [1, oo) | [["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | [["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | ["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | [["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | [[["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | [["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]] | "Ext_Mem_Acc_3_8" \in [1, oo)]]]]] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)]]]]]] | "Ext_Mem_Acc_10_3" \in [1, oo)]]]]]]]]]]] | "Ext_Mem_Acc_10_5" \in [1, oo)]]]] | "Ext_Mem_Acc_5_6" \in [1, oo)]] | "Ext_Mem_Acc_2_8" \in [1, oo)]] | "Ext_Mem_Acc_6_1" \in [1, oo)]] | "Ext_Mem_Acc_6_8" \in [1, oo)]]]] | "Ext_Mem_Acc_2_9" \in [1, oo)]]]] | "Ext_Mem_Acc_5_1" \in [1, oo)]]]] | "Ext_Mem_Acc_2_10" \in [1, oo)]]]] | "Ext_Mem_Acc_7_1" \in [1, oo)]] | "Ext_Mem_Acc_4_10" \in [1, oo)]] | "Ext_Mem_Acc_4_6" \in [1, oo)]] | "Ext_Mem_Acc_5_10" \in [1, oo)]]]] | "Ext_Mem_Acc_9_1" \in [1, oo)]] | "Ext_Mem_Acc_1_9" \in [1, oo)]]]]]] | "Ext_Mem_Acc_7_9" \in [1, oo)]]]] | "Ext_Mem_Acc_6_7" \in [1, oo)]]]] | "Ext_Mem_Acc_6_2" \in [1, oo)]] | "Ext_Mem_Acc_7_10" \in [1, oo)]]]]]]]]]] | ~ [[[[[["Active_6" \in [1, oo) | ["Active_1" \in [1, oo) | ["Active_10" \in [1, oo) | ["Active_5" \in [1, oo) | ["Active_7" \in [1, oo) | "Active_9" \in [1, oo)]]]]] | "Active_2" \in [1, oo)] | "Active_4" \in [1, oo)] | "Active_8" \in [1, oo)] | "Active_3" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[[[[[[[[[[["Ext_Mem_Acc_7_8" \in [1, oo) | [["Ext_Mem_Acc_1_5" \in [1, oo) | [[[[[[[[["Ext_Mem_Acc_1_8" \in [1, oo) | [[[[[[[[["Ext_Mem_Acc_10_9" \in [1, oo) | [[[[[[[[[[[[[[["Ext_Mem_Acc_5_1" \in [1, oo) | [["Ext_Mem_Acc_10_7" \in [1, oo) | [["Ext_Mem_Acc_2_9" \in [1, oo) | [["Ext_Mem_Acc_5_2" \in [1, oo) | [[[[[[[[[[[[[[[[["Ext_Mem_Acc_5_4" \in [1, oo) | [["Ext_Mem_Acc_3_4" \in [1, oo) | [["Ext_Mem_Acc_1_10" \in [1, oo) | [["Ext_Mem_Acc_10_3" \in [1, oo) | [["Ext_Mem_Acc_9_5" \in [1, oo) | [["Ext_Mem_Acc_6_4" \in [1, oo) | [["Ext_Mem_Acc_3_7" \in [1, oo) | [["Ext_Mem_Acc_10_6" \in [1, oo) | [["Ext_Mem_Acc_4_8" \in [1, oo) | [["Ext_Mem_Acc_3_8" \in [1, oo) | [[["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)] | "Ext_Mem_Acc_9_3" \in [1, oo)]] | "Ext_Mem_Acc_9_4" \in [1, oo)]] | "Ext_Mem_Acc_4_2" \in [1, oo)]] | "Ext_Mem_Acc_10_2" \in [1, oo)]] | "Ext_Mem_Acc_7_6" \in [1, oo)]] | "Ext_Mem_Acc_4_7" \in [1, oo)]] | "Ext_Mem_Acc_6_9" \in [1, oo)]] | "Ext_Mem_Acc_9_6" \in [1, oo)]] | "Ext_Mem_Acc_4_1" \in [1, oo)]] | "Ext_Mem_Acc_2_3" \in [1, oo)]] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)]] | "Ext_Mem_Acc_7_3" \in [1, oo)]] | "Ext_Mem_Acc_4_3" \in [1, oo)]] | "Ext_Mem_Acc_8_10" \in [1, oo)]] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)]] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)]] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)]] | "Ext_Mem_Acc_6_2" \in [1, oo)]] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)] xor ["Active_3" \in [1, oo) | [["Active_4" \in [1, oo) | [["Active_6" \in [1, oo) | [["Active_10" \in [1, oo) | [["Active_7" \in [1, oo) | "Active_9" \in [1, oo)] | "Active_5" \in [1, oo)]] | "Active_1" \in [1, oo)]] | "Active_2" \in [1, oo)]] | "Active_8" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[[[["Active_8" \in [1, oo) | [["Active_2" \in [1, oo) | [["Active_1" \in [1, oo) | [["Active_5" \in [1, oo) | ["Active_9" \in [1, oo) | "Active_7" \in [1, oo)]] | "Active_10" \in [1, oo)]] | "Active_6" \in [1, oo)]] | "Active_4" \in [1, oo)]] | "Active_3" \in [1, oo)] & ~ [["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | [["Ext_Mem_Acc_6_2" \in [1, oo) | [["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | [["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | [["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | [["Ext_Mem_Acc_8_10" \in [1, oo) | [["Ext_Mem_Acc_4_3" \in [1, oo) | [["Ext_Mem_Acc_7_3" \in [1, oo) | [["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | [["Ext_Mem_Acc_2_3" \in [1, oo) | [["Ext_Mem_Acc_4_1" \in [1, oo) | [["Ext_Mem_Acc_9_6" \in [1, oo) | [["Ext_Mem_Acc_6_9" \in [1, oo) | [["Ext_Mem_Acc_4_7" \in [1, oo) | [["Ext_Mem_Acc_7_6" \in [1, oo) | [["Ext_Mem_Acc_10_2" \in [1, oo) | [["Ext_Mem_Acc_4_2" \in [1, oo) | [["Ext_Mem_Acc_9_4" \in [1, oo) | [["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]] | "Ext_Mem_Acc_3_8" \in [1, oo)]] | "Ext_Mem_Acc_4_8" \in [1, oo)]] | "Ext_Mem_Acc_10_6" \in [1, oo)]] | "Ext_Mem_Acc_3_7" \in [1, oo)]] | "Ext_Mem_Acc_6_4" \in [1, oo)]] | "Ext_Mem_Acc_9_5" \in [1, oo)]] | "Ext_Mem_Acc_10_3" \in [1, oo)]] | "Ext_Mem_Acc_1_10" \in [1, oo)]] | "Ext_Mem_Acc_3_4" \in [1, oo)]] | "Ext_Mem_Acc_5_4" \in [1, oo)]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_5_2" \in [1, oo)]] | "Ext_Mem_Acc_2_9" \in [1, oo)]] | "Ext_Mem_Acc_10_7" \in [1, oo)]] | "Ext_Mem_Acc_5_1" \in [1, oo)]]]]]]]]]]]]]]] | "Ext_Mem_Acc_10_9" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_1_8" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_1_5" \in [1, oo)]] | "Ext_Mem_Acc_7_8" \in [1, oo)]]]]]]]]]]]] | [["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | [["Ext_Mem_Acc_6_2" \in [1, oo) | [["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | [["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | [["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | [["Ext_Mem_Acc_8_10" \in [1, oo) | [["Ext_Mem_Acc_4_3" \in [1, oo) | [["Ext_Mem_Acc_7_3" \in [1, oo) | [["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | [["Ext_Mem_Acc_2_3" \in [1, oo) | [["Ext_Mem_Acc_4_1" \in [1, oo) | [["Ext_Mem_Acc_9_6" \in [1, oo) | [["Ext_Mem_Acc_6_9" \in [1, oo) | [["Ext_Mem_Acc_4_7" \in [1, oo) | [["Ext_Mem_Acc_7_6" \in [1, oo) | [["Ext_Mem_Acc_10_2" \in [1, oo) | [["Ext_Mem_Acc_4_2" \in [1, oo) | [["Ext_Mem_Acc_9_4" \in [1, oo) | [["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]] | "Ext_Mem_Acc_3_8" \in [1, oo)]] | "Ext_Mem_Acc_4_8" \in [1, oo)]] | "Ext_Mem_Acc_10_6" \in [1, oo)]] | "Ext_Mem_Acc_3_7" \in [1, oo)]] | "Ext_Mem_Acc_6_4" \in [1, oo)]] | "Ext_Mem_Acc_9_5" \in [1, oo)]] | "Ext_Mem_Acc_10_3" \in [1, oo)]] | "Ext_Mem_Acc_1_10" \in [1, oo)]] | "Ext_Mem_Acc_3_4" \in [1, oo)]] | "Ext_Mem_Acc_5_4" \in [1, oo)]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_5_2" \in [1, oo)]] | "Ext_Mem_Acc_2_9" \in [1, oo)]] | "Ext_Mem_Acc_10_7" \in [1, oo)]] | "Ext_Mem_Acc_5_1" \in [1, oo)]]]]]]]]]]]]]]] | "Ext_Mem_Acc_10_9" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_1_8" \in [1, oo)]]]]]]]]] | "Ext_Mem_Acc_1_5" \in [1, oo)]] | "Ext_Mem_Acc_7_8" \in [1, oo)]]]]]]]]]] & ~ [[["Active_8" \in [1, oo) | [["Active_2" \in [1, oo) | [["Active_1" \in [1, oo) | [["Active_5" \in [1, oo) | ["Active_9" \in [1, oo) | "Active_7" \in [1, oo)]] | "Active_10" \in [1, oo)]] | "Active_6" \in [1, oo)]] | "Active_4" \in [1, oo)]] | "Active_3" \in [1, oo)]]]]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_1_3" \in [1, oo) | [[[["Ext_Mem_Acc_2_3" \in [1, oo) | [[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)]] | "Ext_Mem_Acc_9_3" \in [1, oo)] | "Ext_Mem_Acc_3_8" \in [1, oo)] | "Ext_Mem_Acc_9_4" \in [1, oo)] | "Ext_Mem_Acc_4_8" \in [1, oo)] | "Ext_Mem_Acc_4_2" \in [1, oo)] | "Ext_Mem_Acc_10_6" \in [1, oo)] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)] | "Ext_Mem_Acc_10_3" \in [1, oo)] | "Ext_Mem_Acc_9_6" \in [1, oo)] | "Ext_Mem_Acc_1_10" \in [1, oo)] | "Ext_Mem_Acc_4_1" \in [1, oo)] | "Ext_Mem_Acc_3_4" \in [1, oo)]] | "Ext_Mem_Acc_5_4" \in [1, oo)] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)]] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)] | "Ext_Mem_Acc_7_3" \in [1, oo)] | "Ext_Mem_Acc_2_9" \in [1, oo)] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)] | "Ext_Mem_Acc_5_1" \in [1, oo)] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_4" \in [1, oo) | ["Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_5" \in [1, oo) | ["Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_9" \in [1, oo) | [[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_7" \in [1, oo) | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_4" \in [1, oo)]]] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_3" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_9" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)]]] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_1" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_2" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_2" \in [1, oo)]]]]
normalized: ~ [E [true U [["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Memory_9" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_2" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_8" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | [[["Memory_9" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Memory_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_2" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | [[["Memory_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | "Memory_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo)]]]]]]]]]]]]]]]] | "Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Memory_7" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo)] | "Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | ["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | ["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | ["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | ["Ext_Mem_Acc_2_9" \in [1, oo) | ["Ext_Mem_Acc_7_3" \in [1, oo) | ["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | [["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | [["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | [["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)]]]]]]]]]]]]]]]]]]] | "Ext_Mem_Acc_2_3" \in [1, oo)]]]] | "Ext_Mem_Acc_1_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_48_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)] | "Ext_Mem_Acc_9_3" \in [1, oo)] | "Ext_Mem_Acc_3_8" \in [1, oo)] | "Ext_Mem_Acc_9_4" \in [1, oo)] | "Ext_Mem_Acc_4_8" \in [1, oo)] | "Ext_Mem_Acc_4_2" \in [1, oo)] | "Ext_Mem_Acc_10_6" \in [1, oo)] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)] | "Ext_Mem_Acc_10_3" \in [1, oo)] | "Ext_Mem_Acc_9_6" \in [1, oo)] | "Ext_Mem_Acc_1_10" \in [1, oo)] | "Ext_Mem_Acc_4_1" \in [1, oo)] | "Ext_Mem_Acc_3_4" \in [1, oo)] | "Ext_Mem_Acc_2_3" \in [1, oo)] | "Ext_Mem_Acc_5_4" \in [1, oo)] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)] | "Ext_Mem_Acc_7_3" \in [1, oo)] | "Ext_Mem_Acc_2_9" \in [1, oo)] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)] | "Ext_Mem_Acc_5_1" \in [1, oo)] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_7" \in [1, oo) | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_3" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_9" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_1" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_2" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_2" \in [1, oo)]]]]
normalized: ~ [E [true U [["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Memory_9" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_2" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_8" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_7" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_9" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Memory_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_2" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | "Memory_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | ["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | ["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | ["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | ["Ext_Mem_Acc_2_9" \in [1, oo) | ["Ext_Mem_Acc_7_3" \in [1, oo) | ["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | ["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_49_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_5" \in [1, oo) | ["Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_1" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_7" \in [1, oo) | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_3" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)]]] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_10" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_9" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_1" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_10" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_5" \in [1, oo)] | "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_4" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) && "Queue_1" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) && "Queue_2" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) && "Queue_3" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) && "Queue_6" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) && "Queue_9" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_2" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) && "Queue_5" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) && "Queue_9" \in [1, oo)] | "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo)] | "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) && "Queue_2" \in [1, oo)] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Ext_Mem_Acc_5_3" \in [1, oo) | "Ext_Mem_Acc_3_2" \in [1, oo)] | "Ext_Mem_Acc_10_1" \in [1, oo)] | "Ext_Mem_Acc_9_3" \in [1, oo)] | "Ext_Mem_Acc_3_8" \in [1, oo)] | "Ext_Mem_Acc_9_4" \in [1, oo)] | "Ext_Mem_Acc_4_8" \in [1, oo)] | "Ext_Mem_Acc_4_2" \in [1, oo)] | "Ext_Mem_Acc_10_6" \in [1, oo)] | "Ext_Mem_Acc_10_2" \in [1, oo)] | "Ext_Mem_Acc_3_7" \in [1, oo)] | "Ext_Mem_Acc_7_6" \in [1, oo)] | "Ext_Mem_Acc_6_4" \in [1, oo)] | "Ext_Mem_Acc_4_7" \in [1, oo)] | "Ext_Mem_Acc_9_5" \in [1, oo)] | "Ext_Mem_Acc_6_9" \in [1, oo)] | "Ext_Mem_Acc_10_3" \in [1, oo)] | "Ext_Mem_Acc_9_6" \in [1, oo)] | "Ext_Mem_Acc_1_10" \in [1, oo)] | "Ext_Mem_Acc_4_1" \in [1, oo)] | "Ext_Mem_Acc_3_4" \in [1, oo)] | "Ext_Mem_Acc_2_3" \in [1, oo)] | "Ext_Mem_Acc_5_4" \in [1, oo)] | "Ext_Mem_Acc_8_3" \in [1, oo)] | "Ext_Mem_Acc_5_9" \in [1, oo)] | "Ext_Mem_Acc_1_3" \in [1, oo)] | "Ext_Mem_Acc_2_1" \in [1, oo)] | "Ext_Mem_Acc_10_5" \in [1, oo)] | "Ext_Mem_Acc_8_2" \in [1, oo)] | "Ext_Mem_Acc_3_10" \in [1, oo)] | "Ext_Mem_Acc_7_2" \in [1, oo)] | "Ext_Mem_Acc_5_6" \in [1, oo)] | "Ext_Mem_Acc_2_5" \in [1, oo)] | "Ext_Mem_Acc_2_8" \in [1, oo)] | "Ext_Mem_Acc_3_1" \in [1, oo)] | "Ext_Mem_Acc_6_1" \in [1, oo)] | "Ext_Mem_Acc_4_9" \in [1, oo)] | "Ext_Mem_Acc_6_8" \in [1, oo)] | "Ext_Mem_Acc_1_7" \in [1, oo)] | "Ext_Mem_Acc_5_2" \in [1, oo)] | "Ext_Mem_Acc_7_3" \in [1, oo)] | "Ext_Mem_Acc_2_9" \in [1, oo)] | "Ext_Mem_Acc_4_3" \in [1, oo)] | "Ext_Mem_Acc_10_7" \in [1, oo)] | "Ext_Mem_Acc_8_10" \in [1, oo)] | "Ext_Mem_Acc_5_1" \in [1, oo)] | "Ext_Mem_Acc_1_2" \in [1, oo)] | "Ext_Mem_Acc_1_4" \in [1, oo)] | "Ext_Mem_Acc_4_5" \in [1, oo)] | "Ext_Mem_Acc_2_10" \in [1, oo)] | "Ext_Mem_Acc_8_5" \in [1, oo)] | "Ext_Mem_Acc_7_5" \in [1, oo)] | "Ext_Mem_Acc_8_4" \in [1, oo)] | "Ext_Mem_Acc_7_1" \in [1, oo)] | "Ext_Mem_Acc_9_2" \in [1, oo)] | "Ext_Mem_Acc_4_10" \in [1, oo)] | "Ext_Mem_Acc_6_10" \in [1, oo)] | "Ext_Mem_Acc_4_6" \in [1, oo)] | "Ext_Mem_Acc_9_8" \in [1, oo)] | "Ext_Mem_Acc_5_10" \in [1, oo)] | "Ext_Mem_Acc_10_9" \in [1, oo)] | "Ext_Mem_Acc_9_7" \in [1, oo)] | "Ext_Mem_Acc_10_4" \in [1, oo)] | "Ext_Mem_Acc_9_1" \in [1, oo)] | "Ext_Mem_Acc_2_6" \in [1, oo)] | "Ext_Mem_Acc_1_9" \in [1, oo)] | "Ext_Mem_Acc_8_9" \in [1, oo)] | "Ext_Mem_Acc_9_10" \in [1, oo)] | "Ext_Mem_Acc_8_7" \in [1, oo)] | "Ext_Mem_Acc_1_8" \in [1, oo)] | "Ext_Mem_Acc_2_4" \in [1, oo)] | "Ext_Mem_Acc_7_9" \in [1, oo)] | "Ext_Mem_Acc_2_7" \in [1, oo)] | "Ext_Mem_Acc_7_4" \in [1, oo)] | "Ext_Mem_Acc_5_7" \in [1, oo)] | "Ext_Mem_Acc_6_7" \in [1, oo)] | "Ext_Mem_Acc_3_6" \in [1, oo)] | "Ext_Mem_Acc_1_6" \in [1, oo)] | "Ext_Mem_Acc_1_5" \in [1, oo)] | "Ext_Mem_Acc_6_2" \in [1, oo)] | "Ext_Mem_Acc_7_8" \in [1, oo)] | "Ext_Mem_Acc_7_10" \in [1, oo)] | "Ext_Mem_Acc_5_8" \in [1, oo)] | "Ext_Mem_Acc_6_5" \in [1, oo)] | "Ext_Mem_Acc_3_9" \in [1, oo)] | "Ext_Mem_Acc_6_3" \in [1, oo)] | "Ext_Mem_Acc_8_6" \in [1, oo)] | "Ext_Mem_Acc_3_5" \in [1, oo)] | "Ext_Mem_Acc_8_1" \in [1, oo)] | "Ext_Mem_Acc_10_8" \in [1, oo)]]]]
normalized: ~ [E [true U [["Ext_Mem_Acc_10_8" \in [1, oo) | ["Ext_Mem_Acc_8_1" \in [1, oo) | ["Ext_Mem_Acc_3_5" \in [1, oo) | ["Ext_Mem_Acc_8_6" \in [1, oo) | ["Ext_Mem_Acc_6_3" \in [1, oo) | ["Ext_Mem_Acc_3_9" \in [1, oo) | ["Ext_Mem_Acc_6_5" \in [1, oo) | ["Ext_Mem_Acc_5_8" \in [1, oo) | ["Ext_Mem_Acc_7_10" \in [1, oo) | ["Ext_Mem_Acc_7_8" \in [1, oo) | ["Ext_Mem_Acc_6_2" \in [1, oo) | ["Ext_Mem_Acc_1_5" \in [1, oo) | ["Ext_Mem_Acc_1_6" \in [1, oo) | ["Ext_Mem_Acc_3_6" \in [1, oo) | ["Ext_Mem_Acc_6_7" \in [1, oo) | ["Ext_Mem_Acc_5_7" \in [1, oo) | ["Ext_Mem_Acc_7_4" \in [1, oo) | ["Ext_Mem_Acc_2_7" \in [1, oo) | ["Ext_Mem_Acc_7_9" \in [1, oo) | ["Ext_Mem_Acc_2_4" \in [1, oo) | ["Ext_Mem_Acc_1_8" \in [1, oo) | ["Ext_Mem_Acc_8_7" \in [1, oo) | ["Ext_Mem_Acc_9_10" \in [1, oo) | ["Ext_Mem_Acc_8_9" \in [1, oo) | ["Ext_Mem_Acc_1_9" \in [1, oo) | ["Ext_Mem_Acc_2_6" \in [1, oo) | ["Ext_Mem_Acc_9_1" \in [1, oo) | ["Ext_Mem_Acc_10_4" \in [1, oo) | ["Ext_Mem_Acc_9_7" \in [1, oo) | ["Ext_Mem_Acc_10_9" \in [1, oo) | ["Ext_Mem_Acc_5_10" \in [1, oo) | ["Ext_Mem_Acc_9_8" \in [1, oo) | ["Ext_Mem_Acc_4_6" \in [1, oo) | ["Ext_Mem_Acc_6_10" \in [1, oo) | ["Ext_Mem_Acc_4_10" \in [1, oo) | ["Ext_Mem_Acc_9_2" \in [1, oo) | ["Ext_Mem_Acc_7_1" \in [1, oo) | ["Ext_Mem_Acc_8_4" \in [1, oo) | ["Ext_Mem_Acc_7_5" \in [1, oo) | ["Ext_Mem_Acc_8_5" \in [1, oo) | ["Ext_Mem_Acc_2_10" \in [1, oo) | ["Ext_Mem_Acc_4_5" \in [1, oo) | ["Ext_Mem_Acc_1_4" \in [1, oo) | ["Ext_Mem_Acc_1_2" \in [1, oo) | ["Ext_Mem_Acc_5_1" \in [1, oo) | ["Ext_Mem_Acc_8_10" \in [1, oo) | ["Ext_Mem_Acc_10_7" \in [1, oo) | ["Ext_Mem_Acc_4_3" \in [1, oo) | ["Ext_Mem_Acc_2_9" \in [1, oo) | ["Ext_Mem_Acc_7_3" \in [1, oo) | ["Ext_Mem_Acc_5_2" \in [1, oo) | ["Ext_Mem_Acc_1_7" \in [1, oo) | ["Ext_Mem_Acc_6_8" \in [1, oo) | ["Ext_Mem_Acc_4_9" \in [1, oo) | ["Ext_Mem_Acc_6_1" \in [1, oo) | ["Ext_Mem_Acc_3_1" \in [1, oo) | ["Ext_Mem_Acc_2_8" \in [1, oo) | ["Ext_Mem_Acc_2_5" \in [1, oo) | ["Ext_Mem_Acc_5_6" \in [1, oo) | ["Ext_Mem_Acc_7_2" \in [1, oo) | ["Ext_Mem_Acc_3_10" \in [1, oo) | ["Ext_Mem_Acc_8_2" \in [1, oo) | ["Ext_Mem_Acc_10_5" \in [1, oo) | ["Ext_Mem_Acc_2_1" \in [1, oo) | ["Ext_Mem_Acc_1_3" \in [1, oo) | ["Ext_Mem_Acc_5_9" \in [1, oo) | ["Ext_Mem_Acc_8_3" \in [1, oo) | ["Ext_Mem_Acc_5_4" \in [1, oo) | ["Ext_Mem_Acc_2_3" \in [1, oo) | ["Ext_Mem_Acc_3_4" \in [1, oo) | ["Ext_Mem_Acc_4_1" \in [1, oo) | ["Ext_Mem_Acc_1_10" \in [1, oo) | ["Ext_Mem_Acc_9_6" \in [1, oo) | ["Ext_Mem_Acc_10_3" \in [1, oo) | ["Ext_Mem_Acc_6_9" \in [1, oo) | ["Ext_Mem_Acc_9_5" \in [1, oo) | ["Ext_Mem_Acc_4_7" \in [1, oo) | ["Ext_Mem_Acc_6_4" \in [1, oo) | ["Ext_Mem_Acc_7_6" \in [1, oo) | ["Ext_Mem_Acc_3_7" \in [1, oo) | ["Ext_Mem_Acc_10_2" \in [1, oo) | ["Ext_Mem_Acc_10_6" \in [1, oo) | ["Ext_Mem_Acc_4_2" \in [1, oo) | ["Ext_Mem_Acc_4_8" \in [1, oo) | ["Ext_Mem_Acc_9_4" \in [1, oo) | ["Ext_Mem_Acc_3_8" \in [1, oo) | ["Ext_Mem_Acc_9_3" \in [1, oo) | ["Ext_Mem_Acc_10_1" \in [1, oo) | ["Ext_Mem_Acc_3_2" \in [1, oo) | "Ext_Mem_Acc_5_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Memory_9" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_2" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_8" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_8" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_4" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_7" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_9" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Memory_6" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | [[["Memory_2" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_5" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_6" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Memory_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_8" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_2" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_4" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Memory_3" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Memory_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_9" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo) | ["Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_10" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_10" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_4" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | ["Memory_1" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_8" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Memory_10" \in [1, oo) && "Queue_7" \in [1, oo) && "Ext_Bus" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_2" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_3" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_1" \in [1, oo) | ["Queue_3" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_5" \in [1, oo) | ["Queue_9" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_7" \in [1, oo) | "Memory_7" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Queue_1" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Memory_6" \in [1, oo)] | "Memory_5" \in [1, oo) && "Ext_Bus" \in [1, oo) && "Queue_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_50_fireability_and_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m11sec

STOP 1369845793

--------------------
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

825 1016 1265 1409 1853 2064 2261 2392 2626 2681
iterations count:10105 (48), effective:110 (0)

initing FirstDep: 0m0sec

2716 2748 2686 2669 2674
iterations count:5174 (24), effective:75 (0)
862 1191 1375 1649 1880 2065 2318 2618 2645
iterations count:9695 (46), effective:100 (0)

iterations count:226 (1), effective:3 (0)
4643 4187 4250 4087 3689 3500 3130 3145 3016 2880
iterations count:10973 (52), effective:130 (0)
4359 4191 4127 3975 3505 3322 3092 3085 2964 2825
iterations count:10421 (49), effective:106 (0)

iterations count:216 (1), effective:3 (0)

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