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=TokenRing-PT-005
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/TokenRing-PT-005
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is TokenRing-PT-005, examination is ReachabilityFireability'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for TokenRing/005 (P/T)

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

execution on node 38: cluster1u40.lip6.fr (runId=136989898301257_n_38)
=====================================================================
runnning marcie on TokenRing-PT-005 (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 TokenRing-PT-005, examination is ReachabilityFireability
=====================================================================

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

START 1369913242

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: 36 NrTr: 156)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m0sec


-> reachability set: #nodes 652 (6.5e+02) #states 166



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

checking: AG [[["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | [["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | [[["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | [[[["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | [[["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | [[[["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_0" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | [[["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | [[["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | [[["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | [[["State_4_4" \in [1, oo) && "State_5_1" \in [1, oo) | [[[[["State_4_3" \in [1, oo) && "State_3_2" \in [1, oo) | [[["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | [["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_0" \in [1, oo) | [["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | [[[["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_5" \in [1, oo) | [[[["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | [[[["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | [[[[[[["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | [[["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_0" \in [1, oo) | [[[[["State_3_4" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | [["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | [["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_0" \in [1, oo)]] | "State_2_4" \in [1, oo) && "State_1_1" \in [1, oo)]]] | "State_2_5" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)]]] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_1" \in [1, oo)]] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_0" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_5" \in [1, oo) && "State_4_1" \in [1, oo)]]] | "State_1_3" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)]]] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_0" \in [1, oo)]]]]]]]]]]]] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)]] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)]]] | "State_3_5" \in [1, oo) && "State_2_1" \in [1, oo)]]] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)]] | "State_1_4" \in [1, oo) && "State_2_0" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)]] | "State_3_5" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)]]]]]]]] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)]]] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_5" \in [1, oo) && "State_1_2" \in [1, oo)]]] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)]]]]]]]] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)]] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)]] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)]]] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)]] & [["State_5_3" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | [["State_5_4" \in [1, oo) && "State_0_4" \in [1, oo) | "State_5_1" \in [1, oo) && "State_0_1" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_0_2" \in [1, oo)]]] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[[["State_5_3" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | [["State_5_4" \in [1, oo) && "State_0_4" \in [1, oo) | "State_5_1" \in [1, oo) && "State_0_1" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_0_2" \in [1, oo)]]] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)] & [["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | [[["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | [["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | [["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | [[[[[[[["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | [[["State_2_5" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | [[["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | [[[[[[[["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_5" \in [1, oo) && "State_2_2" \in [1, oo) | [["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_0" \in [1, oo) | [["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | [[["State_3_5" \in [1, oo) && "State_2_1" \in [1, oo) | [[["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | [["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | [[[[[[[[[[[["State_1_4" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | [[["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_2" \in [1, oo) | [["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_5_5" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_0" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | [["State_0_3" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | [[["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_5" \in [1, oo) && "State_1_3" \in [1, oo) | [[["State_2_4" \in [1, oo) && "State_1_1" \in [1, oo) | [["State_0_4" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)]] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)]] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_3" \in [1, oo)]]]]] | "State_3_3" \in [1, oo) && "State_4_0" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)]]] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)]]]]]]]] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)]]]] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)]]]] | "State_3_3" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)]]]] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)]] | "State_2_4" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)]] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)]]] | "State_4_3" \in [1, oo) && "State_3_2" \in [1, oo)]]]]] | "State_4_4" \in [1, oo) && "State_5_1" \in [1, oo)]]] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)]]] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)]]] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)]]] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_0" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)]]]] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)]]] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)]]]] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)]]] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)]] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | [[[[[[["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | [[[[[[[[[[["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | [[[[[["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_1" \in [1, oo) | [[[[["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | [[["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_5" \in [1, oo) && "State_2_0" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | [[["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | [[[["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_0" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | [[[["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | [["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | [[["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)]]]] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)]]]] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)]]]]]]]]]]]]]]]]] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)]]]] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)]]]]]]]]]]]]]]] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)]]]]] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)]]] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)]]] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)]]] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)]]] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)]]] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)] | [["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | [["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)]] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)]] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | [["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | [["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)]] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)]] | ["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | [[["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | [[["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | [[["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | [[["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | [[["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | [[[[["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | [[[[[[[[[[[[[[["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | [[[["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | [[[[[[[[[[[[[[[[["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | [[[["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | [[[["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)]]] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)]] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)]]]] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_0" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)]]]] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)]]] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_5" \in [1, oo) && "State_2_0" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)]]] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)]]]]] | "State_1_4" \in [1, oo) && "State_0_1" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)]]]]]] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)]]]]]]]]]]] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)]]]]]]] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_3_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)]]] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)] & [[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | [["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)]] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)]]] & ["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | [[["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)]]] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)] | [[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]] | ["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | [[["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_5_fireability_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)] <-> [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[[~ [["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]]]] | [["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]] & ["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)]]]]
normalized: ~ [E [true U [["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]]]]]

-> the formula is TRUE

FORMULA p_28_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)]]]]
normalized: ~ [E [true U [["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]]]]]

-> the formula is FALSE

FORMULA p_29_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[~ [[[[[["State_0_1" \in [1, oo) && "State_5_1" \in [1, oo) | "State_0_4" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_0_0" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_0_5" \in [1, oo) && "State_5_5" \in [1, oo)]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["State_4_2" \in [1, oo) && "State_5_5" \in [1, oo) | "State_3_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_1" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_1_4" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_3_4" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_4" \in [1, oo)] | "State_0_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_5" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_5_3" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_1" \in [1, oo)] | "State_4_3" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_0_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_1" \in [1, oo)] | "State_1_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_1_1" \in [1, oo) && "State_0_2" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_2" \in [1, oo)] | "State_5_2" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_1_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_2_3" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_0" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_5" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_3" \in [1, oo)] | "State_4_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_0_1" \in [1, oo) && "State_1_0" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_5_3" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_3" \in [1, oo) && "State_2_4" \in [1, oo)] | "State_1_3" \in [1, oo) && "State_0_5" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_1_3" \in [1, oo)] | "State_0_4" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_2" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_3_4" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_5_4" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_2" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_3" \in [1, oo)] | "State_5_1" \in [1, oo) && "State_4_2" \in [1, oo)] | "State_3_1" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_4_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_2" \in [1, oo)] | "State_5_0" \in [1, oo) && "State_4_4" \in [1, oo)] | "State_0_2" \in [1, oo) && "State_1_5" \in [1, oo)] | "State_3_2" \in [1, oo) && "State_4_5" \in [1, oo)] | "State_2_4" \in [1, oo) && "State_3_5" \in [1, oo)] | "State_3_0" \in [1, oo) && "State_2_2" \in [1, oo)] | "State_2_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_4_1" \in [1, oo) && "State_3_3" \in [1, oo)] | "State_4_0" \in [1, oo) && "State_3_1" \in [1, oo)] | "State_2_1" \in [1, oo) && "State_1_3" \in [1, oo)]]]]
normalized: ~ [E [true U [["State_2_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_2_4" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_0" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_1" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_5_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_3_3" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_5_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_2" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_4_4" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_2" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_4_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_0_5" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_5_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_5" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_5_2" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_2" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_1_2" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_0_0" \in [1, oo) && "State_1_1" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_1" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_4_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_2" \in [1, oo) && "State_1_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_2" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_4_1" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_2_0" \in [1, oo) && "State_3_2" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_4_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_0_3" \in [1, oo) | ["State_2_1" \in [1, oo) && "State_1_4" \in [1, oo) | ["State_3_1" \in [1, oo) && "State_4_4" \in [1, oo) | ["State_4_0" \in [1, oo) && "State_3_3" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_3" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_2" \in [1, oo) | ["State_4_5" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_1_3" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_2_3" \in [1, oo) && "State_3_4" \in [1, oo) | ["State_1_4" \in [1, oo) && "State_2_5" \in [1, oo) | ["State_1_1" \in [1, oo) && "State_2_4" \in [1, oo) | ["State_0_1" \in [1, oo) && "State_1_5" \in [1, oo) | ["State_1_0" \in [1, oo) && "State_0_4" \in [1, oo) | ["State_3_0" \in [1, oo) && "State_2_5" \in [1, oo) | "State_4_2" \in [1, oo) && "State_5_5" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [["State_0_5" \in [1, oo) && "State_5_5" \in [1, oo) | ["State_0_3" \in [1, oo) && "State_5_3" \in [1, oo) | ["State_5_0" \in [1, oo) && "State_0_0" \in [1, oo) | ["State_0_2" \in [1, oo) && "State_5_2" \in [1, oo) | ["State_0_4" \in [1, oo) && "State_5_4" \in [1, oo) | "State_0_1" \in [1, oo) && "State_5_1" \in [1, oo)]]]]]]]]]

-> the formula is FALSE

FORMULA p_30_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m2sec

STOP 1369913244

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

290 361 551
iterations count:3699 (23), effective:60 (0)

initing FirstDep: 0m0sec


iterations count:156 (1), effective:0 (0)

iterations count:156 (1), effective:0 (0)

iterations count:156 (1), effective:0 (0)

iterations count:156 (1), effective:0 (0)

iterations count:475 (3), effective:6 (0)

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