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

Execution Outputs of marcie for PermAdmissibility/01 (P/T)

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

execution on node 3: quadhexa-2.u-paris10.fr (runId=136959888200091_n_3)
=====================================================================
runnning marcie on PermAdmissibility-PT-01 (CTLFireability)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is PermAdmissibility-PT-01, examination is CTLFireability
=====================================================================

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

START 1369624572

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 168 NrTr: 592)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m51sec


-> reachability set: #nodes 66994 (6.7e+04) #states 52,537 (4)



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

checking: EF [[["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | [[["aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)]]]]]]] & [c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_7" \in [1, oo) | [[c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo) | c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_6" \in [1, oo)] | c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_7" \in [1, oo)]]]]
normalized: E [true U [["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | [[["aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)]]]]]]] & [c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_7" \in [1, oo) | [[c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo) | c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_6" \in [1, oo)] | c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_7" \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_1841_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_7" \in [1, oo) | [c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_7" \in [1, oo) | ["in4_6" \in [1, oo) && "in2_2" \in [1, oo) && c7 \in [1, oo) | "in4_6" \in [1, oo) && "in2_3" \in [1, oo) && c7 \in [1, oo)]]] | ["aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | [[[["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | [[[c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_0" \in [1, oo) | [c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux16_2" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | [[[[c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | [c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_6" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_7" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | [c19 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | [c19 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | [["aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | [[[[["aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]] | c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_6" \in [1, oo)] | c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_2" \in [1, oo)] | "aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux14_7" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]]] | c19 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_6" \in [1, oo)]]]]]]]]]]]]]]] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux16_2" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)]]]] | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo)] | c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_6" \in [1, oo)]]]]] | "aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]]]]
normalized: EG [[[["in2_3" \in [1, oo) && "in4_7" \in [1, oo) && c7 \in [1, oo) | [c7 \in [1, oo) && "in4_6" \in [1, oo) && "in2_2" \in [1, oo) | c7 \in [1, oo) && "in4_6" \in [1, oo) && "in2_3" \in [1, oo)]] | "in2_2" \in [1, oo) && "in4_7" \in [1, oo) && c7 \in [1, oo)] | ["aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | [[[["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | [[["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [[[["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | [["aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | [[[[["aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_7" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)]]]]]]]]]]]]]]] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)]]]] | "aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)]]]]] | "aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]]]]

..
EG iterations: 2
-> the formula is FALSE

FORMULA p_1842_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_2" \in [1, oo) | [c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_7" \in [1, oo) | [c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_6" \in [1, oo) | c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo)]]] & ~ [["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_2" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | [["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | [["aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo) | [c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | [[["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | [[["aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | [[[["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_6" \in [1, oo) | [c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_4" \in [1, oo) | [["aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_4" \in [1, oo) | [[[c19 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | [[["aux14_7" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | [[["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_2" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | [c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | [["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | "aux14_5" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]]]]] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)]]]]]] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)]] | c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_4" \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo)]]] | "aux14_1" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | c19 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_7" \in [1, oo)]]] | "aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo)]]] | "aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | c19 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo)]] | "aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)]]]]]]]]]]]]] | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo)]]]]]]]] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)]] | c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_7" \in [1, oo)]]]]]]]]]]]]
normalized: ~ [EG [~ [[~ [[[[[[[[[[c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_7" \in [1, oo) | [[c19 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_4" \in [1, oo) | [[[[[[[["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_6" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | [[[[[[[[[[[[[c19 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | [[c19 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | [c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_2" \in [1, oo) | [[["aux14_7" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | [[[c19 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [[[c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_7" \in [1, oo) | [c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_4" \in [1, oo) | [[c19 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_4" \in [1, oo) | [c19 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) | [[[[[["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | [["aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [[c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | "aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)]] | c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_6" \in [1, oo)]] | "aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo)]]] | "aux14_7" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]]] | "aux14_5" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)]]] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)]] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)] | "aux16_6" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo)]]]] | "aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]] | "aux16_6" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo)] | "aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]]] | "aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)]] | "aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)]] & [[[c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo) | c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_6" \in [1, oo)] | c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_7" \in [1, oo)] | c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_2" \in [1, oo)]]]]]

...
EG iterations: 3
-> the formula is TRUE

FORMULA p_1843_fireability_and_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_2" \in [1, oo) | [c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_3" \in [1, oo) | ["in2_2" \in [1, oo) && "in4_6" \in [1, oo) && c7 \in [1, oo) | c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo)]]] | ~ [["aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [[[c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_6" \in [1, oo) | [c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | [c19 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_4" \in [1, oo) | [c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_0" \in [1, oo) | [c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux16_2" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_7" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo) | [c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_1" \in [1, oo) | [c19 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | [[["aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux14_2" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | [[["aux14_7" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | [[[["aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_6" \in [1, oo) | [["aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | c19 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo)] | c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_4" \in [1, oo)]]]]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)]]]]]] | "aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_7" \in [1, oo)]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)]]]]]]]]]]]]] | "aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]] | c19 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[~ [[[["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | [[[[[[[[[[[[["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | [["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo) | [[[[[["aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | [[[["aux16_6" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]] | "aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)]]]] | "aux14_0" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux14_7" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]]] | "aux14_5" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)]] | "aux14_1" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c19 \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo)] | "aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]]] | "aux14_1" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_6" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]]] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)]] | [[[c7 \in [1, oo) && "in2_3" \in [1, oo) && "in4_6" \in [1, oo) | c7 \in [1, oo) && "in2_2" \in [1, oo) && "in4_6" \in [1, oo)] | c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_3" \in [1, oo)] | c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_2" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_1844_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 1m20sec

checking: AG [[[["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_7" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [[[[c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | [[[["aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | [[["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo) | [c19 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | [[["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_6" \in [1, oo) | [c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | [[["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | [c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_7" \in [1, oo) | [c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_4" \in [1, oo) | [c19 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_7" \in [1, oo) | [c19 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_0" \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | [c19 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | [[["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]] | c19 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]]]]]]]]]]]]]]] | "aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)]]]]]] | "aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)] | "aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)]]]]]]] | "aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]]]]] | c19 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_7" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux16_1" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)]]]]] | c19 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_7" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | c19 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_0" \in [1, oo)]]]]]]]]]]]]]] | "aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] & ~ [[c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_2" \in [1, oo) | [c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_3" \in [1, oo) | [c7 \in [1, oo) && "in4_6" \in [1, oo) && "in2_2" \in [1, oo) | c7 \in [1, oo) && "in4_6" \in [1, oo) && "in2_3" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[[["aux16_7" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_4" \in [1, oo) && c19 \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [[["aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | [[c19 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_6" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | [[[["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | [[[[["aux14_3" \in [1, oo) && c19 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | [[[[[[[["aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | [[["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_6" \in [1, oo) | [c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_4" \in [1, oo) | [["aux14_6" \in [1, oo) && c19 \in [1, oo) && "aux16_2" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c19 \in [1, oo) | [[["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux14_7" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_0" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo) | ["aux14_1" \in [1, oo) && c19 \in [1, oo) && "aux16_5" \in [1, oo) | [[["aux16_4" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo) | "aux14_5" \in [1, oo) && c19 \in [1, oo) && "aux16_3" \in [1, oo)]] | "aux16_6" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]]]]]]]]]]]]]]] | "aux14_1" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_5" \in [1, oo)]]] | "aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_7" \in [1, oo)]]] | "aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)]] | "aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux16_5" \in [1, oo) && c19 \in [1, oo) && "aux14_2" \in [1, oo)] | c19 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_7" \in [1, oo)] | c19 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux16_0" \in [1, oo) && c19 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c19 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c19 \in [1, oo)]]]] | "aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c19 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)]]]]] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c19 \in [1, oo)] | "aux14_0" \in [1, oo) && c19 \in [1, oo) && "aux16_1" \in [1, oo)]]] | "aux16_3" \in [1, oo) && c19 \in [1, oo) && "aux14_0" \in [1, oo)]] | c19 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux16_7" \in [1, oo) && c19 \in [1, oo) && "aux14_4" \in [1, oo)]]]]]]]] | "aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c19 \in [1, oo)] & ~ [[[c7 \in [1, oo) && "in4_7" \in [1, oo) && "in2_3" \in [1, oo) | ["in4_6" \in [1, oo) && "in2_2" \in [1, oo) && c7 \in [1, oo) | c7 \in [1, oo) && "in4_6" \in [1, oo) && "in2_3" \in [1, oo)]] | "in4_7" \in [1, oo) && "in2_2" \in [1, oo) && c7 \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_1845_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m23sec

checking: EG [[["aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_7" \in [1, oo) | [c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_6" \in [1, oo) | [[[c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_7" \in [1, oo) | [[[[[[[[[[[[[["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | [c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_1" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [["aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | [c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [[[["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | [c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo) | [c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_4" \in [1, oo) | [[["aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | [[["aux16_2" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [[[[[["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | [[["aux16_3" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux14_2" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo) | [[[["aux14_6" \in [1, oo) && c20 \in [1, oo) && "aux16_7" \in [1, oo) | [[["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | [c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_3" \in [1, oo) | "aux14_0" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)]]]]] | "aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)]] | "aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]]] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]]] | c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_4" \in [1, oo)] | "aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)]] | c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_7" \in [1, oo)]]]] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo)] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo)] | "aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)]]]]]] | "aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)]]]]] | c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_5" \in [1, oo)] | c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_4" \in [1, oo)] | c20 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_4" \in [1, oo)] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_7" \in [1, oo)] | "aux16_5" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_7" \in [1, oo)]] | "aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo)] | c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_4" \in [1, oo)]]]] & [[[[["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [[c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_5" \in [1, oo) | [[c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_2" \in [1, oo) | [[[[["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [[c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_7" \in [1, oo) | [[[c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_4" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [[[[[[c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_4" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux11_3" \in [1, oo) && c13 \in [1, oo) && "aux9_7" \in [1, oo) | [["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_5" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_6" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_7" \in [1, oo) | [["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[[[["aux11_7" \in [1, oo) && c13 \in [1, oo) && "aux9_3" \in [1, oo) | [[c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_5" \in [1, oo) | [[c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_6" \in [1, oo) | [[["aux11_5" \in [1, oo) && c13 \in [1, oo) && "aux9_1" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_1" \in [1, oo) | ["aux9_4" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_1" \in [1, oo) | [["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | "aux11_5" \in [1, oo) && c13 \in [1, oo) && "aux9_7" \in [1, oo)] | "aux9_6" \in [1, oo) && "aux11_2" \in [1, oo) && c13 \in [1, oo)]]]]]]]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_1" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_6" \in [1, oo)]] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_2" \in [1, oo)]] | "aux11_4" \in [1, oo) && c13 \in [1, oo) && "aux9_0" \in [1, oo)] | "aux11_0" \in [1, oo) && c13 \in [1, oo) && "aux9_5" \in [1, oo)] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_7" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_3" \in [1, oo)]]]]]]] | "aux11_6" \in [1, oo) && c13 \in [1, oo) && "aux9_4" \in [1, oo)]]]] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_6" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_4" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_0" \in [1, oo)] | "aux11_1" \in [1, oo) && c13 \in [1, oo) && "aux9_2" \in [1, oo)]]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)]] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_1" \in [1, oo)]] | "aux11_0" \in [1, oo) && c13 \in [1, oo) && "aux9_6" \in [1, oo)] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_4" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_1" \in [1, oo)]] | c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_5" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_0" \in [1, oo)]] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_4" \in [1, oo)] | "aux11_3" \in [1, oo) && c13 \in [1, oo) && "aux9_2" \in [1, oo)] | c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_0" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]]]
normalized: EG [[[[[[["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [[[[["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | [[["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [[[[[["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux9_7" \in [1, oo) && "aux11_3" \in [1, oo) && c13 \in [1, oo) | [["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | ["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[[[["aux9_3" \in [1, oo) && "aux11_7" \in [1, oo) && c13 \in [1, oo) | [["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [[["aux9_1" \in [1, oo) && "aux11_5" \in [1, oo) && c13 \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_4" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo) | ["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | [["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | "aux9_7" \in [1, oo) && "aux11_5" \in [1, oo) && c13 \in [1, oo)] | "aux9_6" \in [1, oo) && "aux11_2" \in [1, oo) && c13 \in [1, oo)]]]]]]]] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)]]] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]] | "aux9_0" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo)] | "aux9_5" \in [1, oo) && "aux11_0" \in [1, oo) && c13 \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)]]]]]]] | "aux9_4" \in [1, oo) && "aux11_6" \in [1, oo) && c13 \in [1, oo)]]]] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_2" \in [1, oo) && "aux11_1" \in [1, oo) && c13 \in [1, oo)]]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)]] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)]] | "aux9_6" \in [1, oo) && "aux11_0" \in [1, oo) && c13 \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)]] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_2" \in [1, oo) && "aux11_3" \in [1, oo) && c13 \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] & [[[["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | [c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_5" \in [1, oo) | [[[[["aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | [[[[[["aux16_6" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | [[[["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | [[c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [[["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [[["aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_6" \in [1, oo) && c20 \in [1, oo) | [[["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | ["aux14_3" \in [1, oo) && c20 \in [1, oo) && "aux16_3" \in [1, oo) | "aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c20 \in [1, oo)]]]]] | "aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo)]]]]] | "aux16_4" \in [1, oo) && "aux14_2" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_7" \in [1, oo)]]] | "aux14_0" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]]]]]] | c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_5" \in [1, oo)]]] | "aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)]]] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)]]]] | "aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)]] | c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_2" \in [1, oo) && c20 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)]]]]]]]]]]]]]] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)]]] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1886_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m4sec

checking: AF [[["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_5" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux14_1" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | [c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_7" \in [1, oo) | ["aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | [c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | [c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_5" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | ["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_7" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_7" \in [1, oo) | [[[["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [["aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo) | [c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_2" \in [1, oo) | [[[[[["aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_2" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | [c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux14_2" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo) | ["aux14_6" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo) | [c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_0" \in [1, oo) | [c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | ["aux16_3" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | [c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux14_0" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo) | "aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_7" \in [1, oo)] | c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_4" \in [1, oo)] | "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_6" \in [1, oo)]]] | "aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)]] | "aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_7" \in [1, oo)] | c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_7" \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]] | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_1" \in [1, oo) | ["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_4" \in [1, oo) | ["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_5" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_5" \in [1, oo) | ["aux11_5" \in [1, oo) && c13 \in [1, oo) && "aux9_2" \in [1, oo) | ["aux11_4" \in [1, oo) && c13 \in [1, oo) && "aux9_1" \in [1, oo) | ["aux11_1" \in [1, oo) && c13 \in [1, oo) && "aux9_5" \in [1, oo) | ["aux11_7" \in [1, oo) && c13 \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_6" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_3" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_0" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_0" \in [1, oo) | ["aux11_4" \in [1, oo) && c13 \in [1, oo) && "aux9_3" \in [1, oo) | ["aux11_4" \in [1, oo) && c13 \in [1, oo) && "aux9_6" \in [1, oo) | ["aux11_0" \in [1, oo) && c13 \in [1, oo) && "aux9_2" \in [1, oo) | ["aux11_1" \in [1, oo) && c13 \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_5" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_6" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_5" \in [1, oo) | [[[c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_0" \in [1, oo) | [[[["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | [[c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_6" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_6" \in [1, oo) | [["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [[[[c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_4" \in [1, oo) | [[c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_6" \in [1, oo) | ["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_7" \in [1, oo)]] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_1" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_3" \in [1, oo)] | c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_3" \in [1, oo)] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_5" \in [1, oo)]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_1" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_0" \in [1, oo)]] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_5" \in [1, oo)] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_2" \in [1, oo)] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_3" \in [1, oo)]] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_5" \in [1, oo)] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_7" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_3" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [EG [~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | [["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [[["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | [["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)]] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)]]]] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]]] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)]] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_4" \in [1, oo) && "aux11_1" \in [1, oo) && c13 \in [1, oo)] | "aux9_2" \in [1, oo) && "aux11_0" \in [1, oo) && c13 \in [1, oo)] | "aux9_6" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo)] | "aux9_3" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_4" \in [1, oo) && "aux11_7" \in [1, oo) && c13 \in [1, oo)] | "aux9_5" \in [1, oo) && "aux11_1" \in [1, oo) && c13 \in [1, oo)] | "aux9_1" \in [1, oo) && "aux11_4" \in [1, oo) && c13 \in [1, oo)] | "aux9_2" \in [1, oo) && "aux11_5" \in [1, oo) && c13 \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[[[[[[["aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [["aux16_6" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [[["aux14_6" \in [1, oo) && c20 \in [1, oo) && "aux16_3" \in [1, oo) | [c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[["aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | "aux16_6" \in [1, oo) && "aux14_0" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo)] | c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_6" \in [1, oo) && c20 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux14_0" \in [1, oo) && c20 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux16_6" \in [1, oo) && "aux14_6" \in [1, oo) && c20 \in [1, oo)] | "aux16_6" \in [1, oo) && "aux14_2" \in [1, oo) && c20 \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo)] | c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_5" \in [1, oo)] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)]]]]]] | "aux14_2" \in [1, oo) && c20 \in [1, oo) && "aux16_0" \in [1, oo)] | "aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)]] | "aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)]]]] | "aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux14_7" \in [1, oo) && "aux16_1" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_0" \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_1" \in [1, oo) && c20 \in [1, oo) && "aux16_1" \in [1, oo)] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo)] | c20 \in [1, oo) && "aux14_5" \in [1, oo) && "aux16_5" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux14_1" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)] | "aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux16_4" \in [1, oo) && "aux14_1" \in [1, oo) && c20 \in [1, oo)] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)]]]]]

.........
EG iterations: 9
-> the formula is TRUE

FORMULA p_1887_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m15sec

checking: AG [[["aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_5" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [[c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_4" \in [1, oo) | [[[c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_7" \in [1, oo) | [[["aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_5" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [["aux16_0" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_6" \in [1, oo) | [[[c20 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_4" \in [1, oo) | [c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_4" \in [1, oo) | ["aux16_0" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [[[c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_2" \in [1, oo) | [["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | [[["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | ["aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo) | [[[["aux16_3" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_4" \in [1, oo) | [[[[[[[["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | [c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_4" \in [1, oo) | [c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_4" \in [1, oo) | [[[[[[[[c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_6" \in [1, oo) | ["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | [["aux16_1" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | [[["aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | ["aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_6" \in [1, oo)]]]] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)]] | c20 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_7" \in [1, oo)]]]] | c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_4" \in [1, oo)] | "aux16_3" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo)] | c20 \in [1, oo) && "aux14_6" \in [1, oo) && "aux16_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_6" \in [1, oo)]]]] | "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux16_2" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo)] | c20 \in [1, oo) && "aux14_1" \in [1, oo) && "aux16_6" \in [1, oo)] | "aux16_5" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_6" \in [1, oo)] | c20 \in [1, oo) && "aux14_0" \in [1, oo) && "aux16_7" \in [1, oo)]]] | "aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo)] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo)]]]]] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux14_5" \in [1, oo) && c20 \in [1, oo) && "aux16_7" \in [1, oo)]] | "aux16_1" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)]] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux16_3" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo)]]]] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | "aux16_1" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)]]] | c20 \in [1, oo) && "aux14_2" \in [1, oo) && "aux16_7" \in [1, oo)]]] | "aux16_0" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)] | "aux16_2" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]] | c20 \in [1, oo) && "aux14_4" \in [1, oo) && "aux16_7" \in [1, oo)] | "aux14_7" \in [1, oo) && c20 \in [1, oo) && "aux16_4" \in [1, oo)]] | c20 \in [1, oo) && "aux14_3" \in [1, oo) && "aux16_6" \in [1, oo)]]] & [[c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_0" \in [1, oo) | [[[[[["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_5" \in [1, oo) | [[c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_1" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_6" \in [1, oo) | [[[[c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_3" \in [1, oo) | [[c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_7" \in [1, oo) | [[c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_4" \in [1, oo) | [[[c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_3" \in [1, oo) | [[[[[[c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_3" \in [1, oo) | [[[c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_2" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_7" \in [1, oo) | [c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_3" \in [1, oo) | [[[c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_7" \in [1, oo) | [[c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_0" \in [1, oo) | [c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_2" \in [1, oo) | [[["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_6" \in [1, oo) | [["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_5" \in [1, oo) | [c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_3" \in [1, oo) | [c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_3" \in [1, oo) | ["aux11_1" \in [1, oo) && c13 \in [1, oo) && "aux9_1" \in [1, oo) | [c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_4" \in [1, oo) | [c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_1" \in [1, oo) | ["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux11_6" \in [1, oo) && c13 \in [1, oo) && "aux9_0" \in [1, oo) | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]]]]]]]]]] | c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_6" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_6" \in [1, oo)] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_5" \in [1, oo)]]]] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_5" \in [1, oo)]] | c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_5" \in [1, oo)] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_6" \in [1, oo)]]]]] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_6" \in [1, oo)] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_5" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_7" \in [1, oo)] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_3" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_2" \in [1, oo)] | c13 \in [1, oo) && "aux11_4" \in [1, oo) && "aux9_6" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_4" \in [1, oo)] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_7" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_1" \in [1, oo) && "aux9_2" \in [1, oo)]] | c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_2" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_1" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux11_2" \in [1, oo) && c13 \in [1, oo) && "aux9_7" \in [1, oo)]]]]] | c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_2" \in [1, oo)]]] | c13 \in [1, oo) && "aux11_7" \in [1, oo) && "aux9_2" \in [1, oo)] | c13 \in [1, oo) && "aux11_2" \in [1, oo) && "aux9_0" \in [1, oo)] | c13 \in [1, oo) && "aux11_5" \in [1, oo) && "aux9_4" \in [1, oo)] | c13 \in [1, oo) && "aux11_0" \in [1, oo) && "aux9_4" \in [1, oo)] | c13 \in [1, oo) && "aux11_3" \in [1, oo) && "aux9_2" \in [1, oo)]] | c13 \in [1, oo) && "aux11_6" \in [1, oo) && "aux9_1" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | [["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | ["aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [[["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [[[[["aux9_7" \in [1, oo) && "aux11_2" \in [1, oo) && c13 \in [1, oo) | ["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [[["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo) | [["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [[["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo) | ["aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | ["aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | ["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | [[["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | ["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | [[[[["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo) | ["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | [["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo) | [[[["aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo) | ["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo) | [[["aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo) | [[[[[[[[[["aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo) | "aux9_0" \in [1, oo) && "aux11_6" \in [1, oo) && c13 \in [1, oo)] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_1" \in [1, oo) && "aux11_1" \in [1, oo) && c13 \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)]] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)]]] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)]]] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_3" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_2" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]]] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]]]]]] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)]]] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)]] | "aux9_7" \in [1, oo) && c13 \in [1, oo) && "aux11_6" \in [1, oo)]] | "aux9_3" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)]]]] | "aux9_6" \in [1, oo) && c13 \in [1, oo) && "aux11_0" \in [1, oo)] | "aux9_4" \in [1, oo) && c13 \in [1, oo) && "aux11_7" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_1" \in [1, oo)] | "aux9_1" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)]] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_4" \in [1, oo)] | "aux9_5" \in [1, oo) && c13 \in [1, oo) && "aux11_2" \in [1, oo)]]]]]] | "aux9_0" \in [1, oo) && c13 \in [1, oo) && "aux11_5" \in [1, oo)]] & [[["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo) | [["aux16_4" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo) | ["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo) | [["aux14_6" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | [[["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [[["aux14_1" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [[[["aux14_2" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [[c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_7" \in [1, oo) | [["aux16_7" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_3" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | [[[[["aux16_4" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_2" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo) | [[["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | ["aux16_6" \in [1, oo) && "aux14_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo) | [c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_5" \in [1, oo) | [c20 \in [1, oo) && "aux16_2" \in [1, oo) && "aux14_7" \in [1, oo) | [[[["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | ["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | ["aux14_0" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo) | ["aux14_6" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo) | ["aux14_1" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_7" \in [1, oo) | ["aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_2" \in [1, oo) | [[[["aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo) | [["aux14_1" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo) | ["aux14_4" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo) | [[[["aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo) | "aux14_3" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_0" \in [1, oo) && c20 \in [1, oo)] | "aux14_4" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)]]] | c20 \in [1, oo) && "aux16_1" \in [1, oo) && "aux14_5" \in [1, oo)]] | "aux14_4" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)] | "aux14_0" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux14_6" \in [1, oo) && c20 \in [1, oo) && "aux16_1" \in [1, oo)]]]]]]]] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_0" \in [1, oo)] | "aux14_4" \in [1, oo) && c20 \in [1, oo) && "aux16_3" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)]]]]]]]] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)] | c20 \in [1, oo) && "aux16_3" \in [1, oo) && "aux14_5" \in [1, oo)]]]] | "aux16_6" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_5" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && "aux14_7" \in [1, oo) && c20 \in [1, oo)] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_3" \in [1, oo)]]] | "aux14_1" \in [1, oo) && "aux16_3" \in [1, oo) && c20 \in [1, oo)]] | "aux14_2" \in [1, oo) && c20 \in [1, oo) && "aux16_1" \in [1, oo)]]] | c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_5" \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_6" \in [1, oo)]]] | "aux16_6" \in [1, oo) && c20 \in [1, oo) && "aux14_4" \in [1, oo)] | c20 \in [1, oo) && "aux16_0" \in [1, oo) && "aux14_7" \in [1, oo)]] | c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_5" \in [1, oo)] | "aux14_2" \in [1, oo) && "aux16_2" \in [1, oo) && c20 \in [1, oo)]]] | "aux16_7" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)]]] | "aux16_4" \in [1, oo) && c20 \in [1, oo) && "aux14_1" \in [1, oo)]] | c20 \in [1, oo) && "aux16_5" \in [1, oo) && "aux14_7" \in [1, oo)] | "aux14_3" \in [1, oo) && "aux16_1" \in [1, oo) && c20 \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_1888_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m14sec


total processing time: 3m52sec

STOP 1369624805

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

1291 1594 1676 1980 2045 2212 2283 2396 2427 2752 2823 3015 3075 3237 3308 3443 3451 3648 3719 3848 3938 4042 4090 4097 4378 4404 4563 4626 4644 4839 4860 5015 5070 5150 5215 5220 5370 5449 5505 5544 5592 5715 5761 5818 5863 5929 5970 6032 6157 6170 6179 6320 6320 6315 6482 6467 6471 6659 6658 6655 6775 6771 6764 6867 6858 6848 6964 6945 6929 7004 7015 7063 7106 7134 7129 7171 7223 7262 7311 7370 7383 7392 7441 7479 7505 7492 7536 7586 7623 7662 7730 7744 7737 7741 7771 7781 7808 7840 7864 7846 7955 8001 8033 8075 8098 8131 8152 8199 8239 8250 8294 8407 8411 8399 8461 8506 8549 8590 8596 8607 8653 8660 8767 8772 8755 8793 8804 8845 8855 8887 8898 8933 9005 9011 9014 9042 9069 9083 9093 9088 9115 9128 9157 9907 10817 11422 11914 12251 12538 12794 13196 13421 13610 13742 13965 14151 14317 14609 14958 15323 15621 15817 15870 15980 16095 16147 16232 16385 16421 16475 16636 16782 16938 17027 17072 17285 17476 17561 17836 17956 18159 18202 18214 18351 18398 18709 18842 18990 19067 19182 19196 19237 19326 19365 19624 19632 19844 19991 20062 20206 20296 20345 20359 20491 20590 20744 20837 20896 21002 21067 21160 21306 21492 21542 21569 21572 21702 21848 21910 21963 22005 22013 22136 22195 22257 22292 22302 22414 22439 22444 22443 22525 22634 22665 22679 22721 22796 22808 23006 23109 23157 23214 23323 23486 23607 23716 23766 23798 23877 24013 24107 24161 24209 24362 24524 24556 24641 24703 24769 24834 24909 25247 25388 25537 25570 25620 25657 25800 25877 25927 25969 26014 26084 26124 26145 26173 26220 26351 26481 26626 26694 26694 26718 26851 26910 26932 27077 27147 27241 27248 27241 27274 27332 27383 27521 27550 27588 27611 27614 27657 27676 27740 27770 27785 27784 27958 28006 28047 28114 28116 28166 28195 28252 28281 28334 28334 28514 28588 28655 28688 28831 28870 28875 28895 28943 28995 29037 29071 29127 29162 29169 29174 29263 29386 29433 29490 29500 29528 29602 29675 29724 29756 29767 29764 29901 29983 30091 30118 30148 30159 30159 30164 30177 30218 30246 30291 30301 30312 30310 30313 30454 30552 30646 30733 30771 30813 30860 30969 31014 31059 31115 31195 31229 31291 31331 31370 31494 31611 31715 31818 31886 31946 32002 32022 32075 32145 32245 32320 32349 32384 32465 32485 32517 32620 32668 32689 32732 32742 32799 32840 32851 32861 32892 32912 33095 33136 33200 33314 33351 33376 33400 33424 33463 33523 33595 33632 33670 33704 33707 33732 33725 33872 33973 34042 34082 34127 34168 34181 34247 34300 34374 34435 34476 34493 34533 34569 34609 34730 34771 34809 34854 34864 34872 34908 34927 34935 34968 34988 35133 35217 35283 35319 35348 35373 35415 35516 35537 35585 35622 35624 35639 35666 35714 35744 35795 35991 36061 36079 36096 36133 36142 36152 36194 36248 36296 36304 36320 36355 36350 36391 36391 36465 36489 36500 36517 36530 36536 36552 36574 36565 36564 36577 36688 36767 36788 36814 36865 36948 36985 37008 37073 37119 37127 37168 37211 37273 37334 37357 37402 37544 37609 37635 37661 37704 37778 37801 37836 37866 37908 37913 37912 37945 37996 38029 38064 38180 38209 38260 38284 38307 38316 38350 38377 38376 38418 38433 38509 38551 38570 38578 38603 38632 38665 38667 38664 38679 38714 38723 42336 43193 44896 45444 45487 47666 48286 48752 49470 49760 50514 51161 51476 51691 51971 52951 53416 53493 54161 54324 55953 58654 60302 61778 62412 62719 63594 63955 64113 64597 64846 65188 65491 65733 65903 66033 66176 66251 66400 66496 66561 66679 66817 66938
iterations count:592874 (1001), effective:3245 (5)

initing FirstDep: 0m0sec

13639 13786 13996 14031 14072 14189 14232 14626 14806 14970 15067 15169 15201 15118 15589 15685 15830 15869 15690 16641 16810 16738 16735 17325 17338 17321 17400 18626 18799 18963 19107 19251 19291 19487 19693 19788 19888 19969 19797 19641 20198 20377 20406 20203 20544 20511 20423 20570 20571 20602 20501 21396 21579 21629 21732 21873 22483 22505 22569 22547 22694 22930 23004 23041 22945 23127 23061 23068 23033 22917 22885 23692 23785 23886 24077 24123 24535 24659 24689 24719 24909 24872 24809 25087 24913 24843 24799 24558 25341 25447 25837 25937 26087 26024 26092 26151 26073 25998 25950 25874 26117 26232 26352 26779 26933 26843 26914 26759 26720 26751 27087 27488 27560 27774 27786 27013 28349 27689 28108 28489 28567 28743 28878 29025 29073 29176 29219 29351 29436 29462 29502 29729 30014 30110 30244 30301 30385 30511 30498 30516 30582 30625 30680 30847 31004 31136 31175 31192 31279 31299 31368 31407 31508 31567 31598 31584 31647 31690 31657 31905 32014 32041 32122 32175 32232 32264 32364 32446 32495 32576 32666 32700 32708 32755 32794 32806 32866 32873 32888 32888 32894 32871 32932 32998 33013 33085 33138 33185 33357 33411 33450 33447 33428 33470 33504 33684 33704 33743 33722 33769 33775 33762 33850 33924 33963 34058 34136 34212 34249 34258 34267 34304 34342 34408 34452 34506 34483 34516 34551 34591 34637 34646 34649 34658 34745 34833 34886 34928 34939 34988 35020 35094 35145 35195 35225 35240 35277 35375 35411 35422 35536 35575 35734 35823 35863 35942 35992 36055 36098 36176 36249 36314 36321 36332 36392 36451 36502 36500 36511 36567 36613 36617 36689 36761 36793 36804 36894 36913 36972 37045 37029 37066 37122 37176 37227 37203 37269 37321 37303 37338 37341 37381 37458 37465 37447 37478 37468 37475 37514 37541 37575 37574 37575 37670 37720 37760 37810 37864 37913 37932 37921 37966 38010 38052 38082 38052 38289 38353 38380 38502 38591 38725 38723
iterations count:313361 (529), effective:2116 (3)
58090 59276 61786 62175 63007 64293 64111 65272 65026 66239 66107 66721 66996 67127 67057
iterations count:15627 (26), effective:41 (0)

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

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