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

Execution Outputs of marcie for Philosophers/000050 (P/T)

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

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

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

START 1369688320

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 250 NrTr: 250)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


-> reachability set: #nodes 1280 (1.3e+03) #states 717,897,987,691,852,588,770,249 (23)



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

checking: AG [[["Eat_13" \in [1, oo) | ["Eat_3" \in [1, oo) | ["Eat_50" \in [1, oo) | ["Eat_12" \in [1, oo) | ["Eat_25" \in [1, oo) | ["Eat_9" \in [1, oo) | ["Eat_28" \in [1, oo) | ["Eat_2" \in [1, oo) | ["Eat_8" \in [1, oo) | ["Eat_48" \in [1, oo) | ["Eat_34" \in [1, oo) | ["Eat_27" \in [1, oo) | ["Eat_10" \in [1, oo) | ["Eat_20" \in [1, oo) | ["Eat_37" \in [1, oo) | ["Eat_18" \in [1, oo) | ["Eat_16" \in [1, oo) | ["Eat_23" \in [1, oo) | ["Eat_32" \in [1, oo) | [["Eat_22" \in [1, oo) | ["Eat_29" \in [1, oo) | ["Eat_44" \in [1, oo) | ["Eat_19" \in [1, oo) | ["Eat_26" \in [1, oo) | ["Eat_36" \in [1, oo) | [[["Eat_45" \in [1, oo) | [[[["Eat_24" \in [1, oo) | [[[[[[[["Eat_31" \in [1, oo) | ["Eat_40" \in [1, oo) | ["Eat_47" \in [1, oo) | ["Eat_14" \in [1, oo) | ["Eat_33" \in [1, oo) | ["Eat_42" \in [1, oo) | ["Eat_38" \in [1, oo) | ["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]]]]]]]]] | "Eat_5" \in [1, oo)] | "Eat_39" \in [1, oo)] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)] | "Eat_30" \in [1, oo)] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)]] | "Eat_7" \in [1, oo)] | "Eat_17" \in [1, oo)] | "Eat_49" \in [1, oo)]] | "Eat_11" \in [1, oo)] | "Eat_35" \in [1, oo)]]]]]]] | "Eat_21" \in [1, oo)]]]]]]]]]]]]]]]]]]]] & ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_26" \in [1, oo) | [[["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [[["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_42" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[[["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [[[[["Think_14" \in [1, oo) && "Fork_14" \in [1, oo) | [[[["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | [[["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | [["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)]]] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)]] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]]] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]]]] | "Think_36" \in [1, oo) && "Fork_36" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_43" \in [1, oo)]]]] | "Think_41" \in [1, oo) && "Fork_41" \in [1, oo)]]]]]]]]]]
normalized: ~ [E [true U ~ [[["Eat_13" \in [1, oo) | ["Eat_3" \in [1, oo) | ["Eat_50" \in [1, oo) | ["Eat_12" \in [1, oo) | ["Eat_25" \in [1, oo) | ["Eat_9" \in [1, oo) | ["Eat_28" \in [1, oo) | ["Eat_2" \in [1, oo) | ["Eat_8" \in [1, oo) | ["Eat_48" \in [1, oo) | ["Eat_34" \in [1, oo) | ["Eat_27" \in [1, oo) | ["Eat_10" \in [1, oo) | ["Eat_20" \in [1, oo) | ["Eat_37" \in [1, oo) | ["Eat_18" \in [1, oo) | ["Eat_16" \in [1, oo) | ["Eat_23" \in [1, oo) | ["Eat_32" \in [1, oo) | [["Eat_22" \in [1, oo) | ["Eat_29" \in [1, oo) | ["Eat_44" \in [1, oo) | ["Eat_19" \in [1, oo) | ["Eat_26" \in [1, oo) | ["Eat_36" \in [1, oo) | [[["Eat_45" \in [1, oo) | [[[["Eat_24" \in [1, oo) | [[[[[[[["Eat_31" \in [1, oo) | ["Eat_40" \in [1, oo) | ["Eat_47" \in [1, oo) | ["Eat_14" \in [1, oo) | ["Eat_33" \in [1, oo) | ["Eat_42" \in [1, oo) | ["Eat_38" \in [1, oo) | ["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]]]]]]]]] | "Eat_5" \in [1, oo)] | "Eat_39" \in [1, oo)] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)] | "Eat_30" \in [1, oo)] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)]] | "Eat_7" \in [1, oo)] | "Eat_17" \in [1, oo)] | "Eat_49" \in [1, oo)]] | "Eat_11" \in [1, oo)] | "Eat_35" \in [1, oo)]]]]]]] | "Eat_21" \in [1, oo)]]]]]]]]]]]]]]]]]]]] & ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_26" \in [1, oo) | [[["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [[["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_42" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[[["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [[[[["Think_14" \in [1, oo) && "Fork_14" \in [1, oo) | [[[["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | [[["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | [["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)]]] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)]] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]]] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]]]] | "Think_36" \in [1, oo) && "Fork_36" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_43" \in [1, oo)]]]] | "Think_41" \in [1, oo) && "Fork_41" \in [1, oo)]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m14sec

checking: AG [[["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | [[["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | [[["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | [["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | [["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [[["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Think_1" \in [1, oo) && "Fork_1" \in [1, oo)]]]]]]]]]]]]]]]]] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_18" \in [1, oo)]]]] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)]]]]]]]]]]]]]] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)]]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)]]] | [[["Eat_50" \in [1, oo) | [[["Eat_9" \in [1, oo) | [[["Eat_8" \in [1, oo) | [[["Eat_27" \in [1, oo) | [[[[[["Eat_23" \in [1, oo) | [["Eat_21" \in [1, oo) | ["Eat_22" \in [1, oo) | [[["Eat_19" \in [1, oo) | [[["Eat_35" \in [1, oo) | ["Eat_11" \in [1, oo) | [[["Eat_17" \in [1, oo) | ["Eat_7" \in [1, oo) | [[[["Eat_30" \in [1, oo) | [[["Eat_39" \in [1, oo) | [["Eat_31" \in [1, oo) | [[[["Eat_33" \in [1, oo) | [[["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]] | "Eat_38" \in [1, oo)] | "Eat_42" \in [1, oo)]] | "Eat_14" \in [1, oo)] | "Eat_47" \in [1, oo)] | "Eat_40" \in [1, oo)]] | "Eat_5" \in [1, oo)]] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)]] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)] | "Eat_24" \in [1, oo)]]] | "Eat_49" \in [1, oo)] | "Eat_45" \in [1, oo)]]] | "Eat_36" \in [1, oo)] | "Eat_26" \in [1, oo)]] | "Eat_44" \in [1, oo)] | "Eat_29" \in [1, oo)]]] | "Eat_32" \in [1, oo)]] | "Eat_16" \in [1, oo)] | "Eat_18" \in [1, oo)] | "Eat_37" \in [1, oo)] | "Eat_20" \in [1, oo)] | "Eat_10" \in [1, oo)]] | "Eat_34" \in [1, oo)] | "Eat_48" \in [1, oo)]] | "Eat_2" \in [1, oo)] | "Eat_28" \in [1, oo)]] | "Eat_25" \in [1, oo)] | "Eat_12" \in [1, oo)]] | "Eat_3" \in [1, oo)] | "Eat_13" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[[[["Eat_50" \in [1, oo) | [[["Eat_9" \in [1, oo) | [[["Eat_8" \in [1, oo) | [[["Eat_27" \in [1, oo) | [[[[[["Eat_23" \in [1, oo) | [["Eat_21" \in [1, oo) | ["Eat_22" \in [1, oo) | [[["Eat_19" \in [1, oo) | [[["Eat_35" \in [1, oo) | ["Eat_11" \in [1, oo) | [[["Eat_17" \in [1, oo) | ["Eat_7" \in [1, oo) | [[[["Eat_30" \in [1, oo) | [[["Eat_39" \in [1, oo) | [["Eat_31" \in [1, oo) | [[[["Eat_33" \in [1, oo) | [[["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]] | "Eat_38" \in [1, oo)] | "Eat_42" \in [1, oo)]] | "Eat_14" \in [1, oo)] | "Eat_47" \in [1, oo)] | "Eat_40" \in [1, oo)]] | "Eat_5" \in [1, oo)]] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)]] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)] | "Eat_24" \in [1, oo)]]] | "Eat_49" \in [1, oo)] | "Eat_45" \in [1, oo)]]] | "Eat_36" \in [1, oo)] | "Eat_26" \in [1, oo)]] | "Eat_44" \in [1, oo)] | "Eat_29" \in [1, oo)]]] | "Eat_32" \in [1, oo)]] | "Eat_16" \in [1, oo)] | "Eat_18" \in [1, oo)] | "Eat_37" \in [1, oo)] | "Eat_20" \in [1, oo)] | "Eat_10" \in [1, oo)]] | "Eat_34" \in [1, oo)] | "Eat_48" \in [1, oo)]] | "Eat_2" \in [1, oo)] | "Eat_28" \in [1, oo)]] | "Eat_25" \in [1, oo)] | "Eat_12" \in [1, oo)]] | "Eat_3" \in [1, oo)] | "Eat_13" \in [1, oo)] | [[["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | [[["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | [[[[[[[[[[[[[["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | [[[["Think_18" \in [1, oo) && "Fork_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | [["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Think_1" \in [1, oo) && "Fork_1" \in [1, oo)]]]]]]] | "Think_48" \in [1, oo) && "Fork_48" \in [1, oo)]]]]]]]]]]] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)]] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_34" \in [1, oo) && "Fork_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)]]] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)]]] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m6sec

checking: AG [[~ [[[[["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | [[[["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | [["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [[[[[["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | [[["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | [[["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Think_42" \in [1, oo) && "Fork_42" \in [1, oo)]] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)]] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]]]] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)]]]]] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)]] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]] & [[[[[["Eat_9" \in [1, oo) | [[[[[[[["Eat_20" \in [1, oo) | [[[[[["Eat_21" \in [1, oo) | [[[[[[[[[[[["Eat_7" \in [1, oo) | [[[[[[[[[["Eat_40" \in [1, oo) | [[[["Eat_42" \in [1, oo) | [[["Eat_6" \in [1, oo) | "Eat_43" \in [1, oo)] | "Eat_1" \in [1, oo)] | "Eat_38" \in [1, oo)]] | "Eat_33" \in [1, oo)] | "Eat_14" \in [1, oo)] | "Eat_47" \in [1, oo)]] | "Eat_31" \in [1, oo)] | "Eat_5" \in [1, oo)] | "Eat_39" \in [1, oo)] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)] | "Eat_30" \in [1, oo)] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)] | "Eat_24" \in [1, oo)]] | "Eat_17" \in [1, oo)] | "Eat_49" \in [1, oo)] | "Eat_45" \in [1, oo)] | "Eat_11" \in [1, oo)] | "Eat_35" \in [1, oo)] | "Eat_36" \in [1, oo)] | "Eat_26" \in [1, oo)] | "Eat_19" \in [1, oo)] | "Eat_44" \in [1, oo)] | "Eat_29" \in [1, oo)] | "Eat_22" \in [1, oo)]] | "Eat_32" \in [1, oo)] | "Eat_23" \in [1, oo)] | "Eat_16" \in [1, oo)] | "Eat_18" \in [1, oo)] | "Eat_37" \in [1, oo)]] | "Eat_10" \in [1, oo)] | "Eat_27" \in [1, oo)] | "Eat_34" \in [1, oo)] | "Eat_48" \in [1, oo)] | "Eat_8" \in [1, oo)] | "Eat_2" \in [1, oo)] | "Eat_28" \in [1, oo)]] | "Eat_25" \in [1, oo)] | "Eat_12" \in [1, oo)] | "Eat_50" \in [1, oo)] | "Eat_3" \in [1, oo)] | "Eat_13" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["Eat_13" \in [1, oo) | ["Eat_3" \in [1, oo) | ["Eat_50" \in [1, oo) | ["Eat_12" \in [1, oo) | ["Eat_25" \in [1, oo) | [["Eat_28" \in [1, oo) | ["Eat_2" \in [1, oo) | ["Eat_8" \in [1, oo) | ["Eat_48" \in [1, oo) | ["Eat_34" \in [1, oo) | ["Eat_27" \in [1, oo) | ["Eat_10" \in [1, oo) | [["Eat_37" \in [1, oo) | ["Eat_18" \in [1, oo) | ["Eat_16" \in [1, oo) | ["Eat_23" \in [1, oo) | ["Eat_32" \in [1, oo) | [["Eat_22" \in [1, oo) | ["Eat_29" \in [1, oo) | ["Eat_44" \in [1, oo) | ["Eat_19" \in [1, oo) | ["Eat_26" \in [1, oo) | ["Eat_36" \in [1, oo) | ["Eat_35" \in [1, oo) | ["Eat_11" \in [1, oo) | ["Eat_45" \in [1, oo) | ["Eat_49" \in [1, oo) | ["Eat_17" \in [1, oo) | [["Eat_24" \in [1, oo) | ["Eat_46" \in [1, oo) | ["Eat_15" \in [1, oo) | ["Eat_30" \in [1, oo) | ["Eat_4" \in [1, oo) | ["Eat_41" \in [1, oo) | ["Eat_39" \in [1, oo) | ["Eat_5" \in [1, oo) | ["Eat_31" \in [1, oo) | [["Eat_47" \in [1, oo) | ["Eat_14" \in [1, oo) | ["Eat_33" \in [1, oo) | [["Eat_38" \in [1, oo) | ["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]]] | "Eat_42" \in [1, oo)]]]] | "Eat_40" \in [1, oo)]]]]]]]]]] | "Eat_7" \in [1, oo)]]]]]]]]]]]] | "Eat_21" \in [1, oo)]]]]]] | "Eat_20" \in [1, oo)]]]]]]]] | "Eat_9" \in [1, oo)]]]]]] & ~ [["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [[[[["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | [[[["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | [["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | [["Think_42" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Think_12" \in [1, oo) && "Fork_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]]] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)]]]]]] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)]] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)]]]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)]]]]]]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[[[[[[[[[[[["Eat_34" \in [1, oo) | ["Eat_27" \in [1, oo) | [[[[[[[[[[[[[[[[[[["Eat_17" \in [1, oo) | [[[[["Eat_30" \in [1, oo) | [[[["Eat_5" \in [1, oo) | [[[[[[["Eat_38" \in [1, oo) | [["Eat_6" \in [1, oo) | "Eat_43" \in [1, oo)] | "Eat_1" \in [1, oo)]] | "Eat_42" \in [1, oo)] | "Eat_33" \in [1, oo)] | "Eat_14" \in [1, oo)] | "Eat_47" \in [1, oo)] | "Eat_40" \in [1, oo)] | "Eat_31" \in [1, oo)]] | "Eat_39" \in [1, oo)] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)]] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)] | "Eat_24" \in [1, oo)] | "Eat_7" \in [1, oo)]] | "Eat_49" \in [1, oo)] | "Eat_45" \in [1, oo)] | "Eat_11" \in [1, oo)] | "Eat_35" \in [1, oo)] | "Eat_36" \in [1, oo)] | "Eat_26" \in [1, oo)] | "Eat_19" \in [1, oo)] | "Eat_44" \in [1, oo)] | "Eat_29" \in [1, oo)] | "Eat_22" \in [1, oo)] | "Eat_21" \in [1, oo)] | "Eat_32" \in [1, oo)] | "Eat_23" \in [1, oo)] | "Eat_16" \in [1, oo)] | "Eat_18" \in [1, oo)] | "Eat_37" \in [1, oo)] | "Eat_20" \in [1, oo)] | "Eat_10" \in [1, oo)]]] | "Eat_48" \in [1, oo)] | "Eat_8" \in [1, oo)] | "Eat_2" \in [1, oo)] | "Eat_28" \in [1, oo)] | "Eat_9" \in [1, oo)] | "Eat_25" \in [1, oo)] | "Eat_12" \in [1, oo)] | "Eat_50" \in [1, oo)] | "Eat_3" \in [1, oo)] | "Eat_13" \in [1, oo)] | ~ [["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | [[["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | [["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [[[["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | [[[[[["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | [["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | [[[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | [["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_20" \in [1, oo) | [["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | [[[["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | [["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [[[["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)]] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)]]]]] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)]]]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)]]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)]] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)]]]]]]] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)]] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)]]] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)]] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)]]]]]
normalized: ~ [E [true U ~ [[~ [[["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | [["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | [[[[[[["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | [["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [[[["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | [[[[["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | [["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | [[["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]]] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)]]]] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)]] | "Think_20" \in [1, oo) && "Fork_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)]]]]]] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)]]]] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)]]] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]] | ["Eat_13" \in [1, oo) | ["Eat_3" \in [1, oo) | ["Eat_50" \in [1, oo) | ["Eat_12" \in [1, oo) | ["Eat_25" \in [1, oo) | ["Eat_9" \in [1, oo) | ["Eat_28" \in [1, oo) | ["Eat_2" \in [1, oo) | ["Eat_8" \in [1, oo) | ["Eat_48" \in [1, oo) | [[["Eat_10" \in [1, oo) | ["Eat_20" \in [1, oo) | ["Eat_37" \in [1, oo) | ["Eat_18" \in [1, oo) | ["Eat_16" \in [1, oo) | ["Eat_23" \in [1, oo) | ["Eat_32" \in [1, oo) | ["Eat_21" \in [1, oo) | ["Eat_22" \in [1, oo) | ["Eat_29" \in [1, oo) | ["Eat_44" \in [1, oo) | ["Eat_19" \in [1, oo) | ["Eat_26" \in [1, oo) | ["Eat_36" \in [1, oo) | ["Eat_35" \in [1, oo) | ["Eat_11" \in [1, oo) | ["Eat_45" \in [1, oo) | ["Eat_49" \in [1, oo) | [["Eat_7" \in [1, oo) | ["Eat_24" \in [1, oo) | ["Eat_46" \in [1, oo) | ["Eat_15" \in [1, oo) | [["Eat_4" \in [1, oo) | ["Eat_41" \in [1, oo) | ["Eat_39" \in [1, oo) | [["Eat_31" \in [1, oo) | ["Eat_40" \in [1, oo) | ["Eat_47" \in [1, oo) | ["Eat_14" \in [1, oo) | ["Eat_33" \in [1, oo) | ["Eat_42" \in [1, oo) | [["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]] | "Eat_38" \in [1, oo)]]]]]]] | "Eat_5" \in [1, oo)]]]] | "Eat_30" \in [1, oo)]]]]] | "Eat_17" \in [1, oo)]]]]]]]]]]]]]]]]]]] | "Eat_27" \in [1, oo)] | "Eat_34" \in [1, oo)]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["Fork_16" \in [1, oo) && "Think_16" \in [1, oo) | [["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | [[[[[["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | [[[["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Think_6" \in [1, oo) && "Fork_6" \in [1, oo) | [[["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | [["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | [[[["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | [[[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | [["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | [[[[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)]]] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)]]]]]]]]] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)]] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)]]] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)]]] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)]] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)]] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)]] -> [[[[[[["Eat_28" \in [1, oo) | [[["Eat_48" \in [1, oo) | [[[[[[[[[[[[[[[[["Eat_35" \in [1, oo) | [[[[[[[[[[[[[[[[["Eat_14" \in [1, oo) | [[[[["Eat_6" \in [1, oo) | "Eat_43" \in [1, oo)] | "Eat_1" \in [1, oo)] | "Eat_38" \in [1, oo)] | "Eat_42" \in [1, oo)] | "Eat_33" \in [1, oo)]] | "Eat_47" \in [1, oo)] | "Eat_40" \in [1, oo)] | "Eat_31" \in [1, oo)] | "Eat_5" \in [1, oo)] | "Eat_39" \in [1, oo)] | "Eat_41" \in [1, oo)] | "Eat_4" \in [1, oo)] | "Eat_30" \in [1, oo)] | "Eat_15" \in [1, oo)] | "Eat_46" \in [1, oo)] | "Eat_24" \in [1, oo)] | "Eat_7" \in [1, oo)] | "Eat_17" \in [1, oo)] | "Eat_49" \in [1, oo)] | "Eat_45" \in [1, oo)] | "Eat_11" \in [1, oo)]] | "Eat_36" \in [1, oo)] | "Eat_26" \in [1, oo)] | "Eat_19" \in [1, oo)] | "Eat_44" \in [1, oo)] | "Eat_29" \in [1, oo)] | "Eat_22" \in [1, oo)] | "Eat_21" \in [1, oo)] | "Eat_32" \in [1, oo)] | "Eat_23" \in [1, oo)] | "Eat_16" \in [1, oo)] | "Eat_18" \in [1, oo)] | "Eat_37" \in [1, oo)] | "Eat_20" \in [1, oo)] | "Eat_10" \in [1, oo)] | "Eat_27" \in [1, oo)] | "Eat_34" \in [1, oo)]] | "Eat_8" \in [1, oo)] | "Eat_2" \in [1, oo)]] | "Eat_9" \in [1, oo)] | "Eat_25" \in [1, oo)] | "Eat_12" \in [1, oo)] | "Eat_50" \in [1, oo)] | "Eat_3" \in [1, oo)] | "Eat_13" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["Eat_13" \in [1, oo) | ["Eat_3" \in [1, oo) | ["Eat_50" \in [1, oo) | ["Eat_12" \in [1, oo) | ["Eat_25" \in [1, oo) | ["Eat_9" \in [1, oo) | [["Eat_2" \in [1, oo) | ["Eat_8" \in [1, oo) | [["Eat_34" \in [1, oo) | ["Eat_27" \in [1, oo) | ["Eat_10" \in [1, oo) | ["Eat_20" \in [1, oo) | ["Eat_37" \in [1, oo) | ["Eat_18" \in [1, oo) | ["Eat_16" \in [1, oo) | ["Eat_23" \in [1, oo) | ["Eat_32" \in [1, oo) | ["Eat_21" \in [1, oo) | ["Eat_22" \in [1, oo) | ["Eat_29" \in [1, oo) | ["Eat_44" \in [1, oo) | ["Eat_19" \in [1, oo) | ["Eat_26" \in [1, oo) | ["Eat_36" \in [1, oo) | [["Eat_11" \in [1, oo) | ["Eat_45" \in [1, oo) | ["Eat_49" \in [1, oo) | ["Eat_17" \in [1, oo) | ["Eat_7" \in [1, oo) | ["Eat_24" \in [1, oo) | ["Eat_46" \in [1, oo) | ["Eat_15" \in [1, oo) | ["Eat_30" \in [1, oo) | ["Eat_4" \in [1, oo) | ["Eat_41" \in [1, oo) | ["Eat_39" \in [1, oo) | ["Eat_5" \in [1, oo) | ["Eat_31" \in [1, oo) | ["Eat_40" \in [1, oo) | ["Eat_47" \in [1, oo) | [["Eat_33" \in [1, oo) | ["Eat_42" \in [1, oo) | ["Eat_38" \in [1, oo) | ["Eat_1" \in [1, oo) | ["Eat_43" \in [1, oo) | "Eat_6" \in [1, oo)]]]]] | "Eat_14" \in [1, oo)]]]]]]]]]]]]]]]]] | "Eat_35" \in [1, oo)]]]]]]]]]]]]]]]]] | "Eat_48" \in [1, oo)]]] | "Eat_28" \in [1, oo)]]]]]]] | ~ [[["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | [["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | [[["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | [[["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | [["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | [["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | [[[[[[[[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | [[["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | [["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)]]]]] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)]]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)]] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]]]] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)]]] | "Think_6" \in [1, oo) && "Fork_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)]]]] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)]]]]]] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)]] | "Fork_16" \in [1, oo) && "Think_16" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [[[[[[[[[[["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [[[[[[[[["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | [[[[[[[["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | [[[[[[[["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[[[[[["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)]]] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)]]] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)]] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)]]] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_16" \in [1, oo) && "Think_17" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)]]] & [[[[[[[[[[["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | [[[["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [[["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [[[[[[[[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | [[[[["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | [[[[[[[[["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | [[[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)]]] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]]] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)]] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]]]]
normalized: ~ [E [true U [["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | [["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | [["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | [[["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [[["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | [[["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | [["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)]]]] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)]]]]]]]]] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]]]]] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]]]]]]] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)]]] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)]]]] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)]]]]]]]]]]] & [[["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | [[["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | [["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | [[["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | [["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)]]]]]]] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)]]]]]]]] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)]]]]]]]] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)]]]]]]]]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)]]]]]]]]]]] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_48_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: ~ [EF [[[[[[[[[[[[[[[[[["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)]] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)]]] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_16" \in [1, oo) && "Think_17" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)]]]]
normalized: ~ [E [true U [["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | [[["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)]]]]]]]]]]]]]]]]]]]]] | ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_49_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)] & ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_16" \in [1, oo) && "Think_17" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)]]]]]
normalized: ~ [E [true U [~ [["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_50_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m23sec


total processing time: 0m56sec

STOP 1369688376

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

1274
iterations count:1143 (4), effective:150 (0)

initing FirstDep: 0m0sec

3079 2839 2667 2575 2509 2327 1955 2167 1936 1850 1740 1678 1592 1532
iterations count:14171 (56), effective:2402 (9)
1278 1288 1316 1434 1490 1486 1270 1566 1435 1449 1280 1266 1491 1505
iterations count:14963 (59), effective:2498 (9)

iterations count:992 (3), effective:101 (0)
1760
iterations count:1233 (4), effective:103 (0)
1760
iterations count:1233 (4), effective:103 (0)
1764
iterations count:1479 (5), effective:150 (0)

iterations count:986 (3), effective:100 (0)
3879 3669 3466 3412 3377 3182 3046 3037 3187 2801 2731 2661 3015 2827 2554 2459
iterations count:16604 (66), effective:2800 (11)

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