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=CTLFireability
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
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 CTLFireability'
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=136968525300185_n_1)
=====================================================================
runnning marcie on Philosophers-PT-000050 (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 Philosophers-PT-000050, examination is CTLFireability
=====================================================================

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

START 1369700960

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: 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: AF [[["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) | ["Think_17" \in [1, oo) && "Fork_16" \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) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \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) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \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)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo) | ["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Catch2_25" \in [1, oo) && "Fork_24" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | ["Catch2_38" \in [1, oo) && "Fork_37" \in [1, oo) | [["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | ["Catch2_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Catch2_3" \in [1, oo) && "Fork_2" \in [1, oo) | [["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | [["Catch2_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | [[["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | [["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | ["Catch2_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | [[[[["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | [[[[["Catch2_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | ["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Catch2_7" \in [1, oo) && "Fork_6" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)]]]]]] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)]] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)]] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)] | "Catch2_43" \in [1, oo) && "Fork_42" \in [1, oo)]]]]] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)]]]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)]] | "Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo)]]]]] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)]]]] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)]]]]]]
normalized: ~ [EG [~ [[["Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo) | ["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Catch2_25" \in [1, oo) && "Fork_24" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | ["Catch2_38" \in [1, oo) && "Fork_37" \in [1, oo) | [["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | ["Catch2_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Catch2_3" \in [1, oo) && "Fork_2" \in [1, oo) | [["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | [["Catch2_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | [[["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | [["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | ["Catch2_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | [[[[["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | [[[[["Catch2_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | ["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Catch2_7" \in [1, oo) && "Fork_6" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)]]]]]] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)]] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)]] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)] | "Catch2_43" \in [1, oo) && "Fork_42" \in [1, oo)]]]]] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)]]]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)]] | "Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo)]]]]] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)]]]] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)]]]] & [[[[[[[[[[[[[[[[[["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \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) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \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_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \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)] | "Think_17" \in [1, oo) && "Fork_16" \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)]]]]]

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

FORMULA p_1841_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m34sec

checking: EF [[[["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | [["Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | [["Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | [[["Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo) | ["Catch2_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | ["Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo) | [["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo) | [["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | [["Catch2_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo) | ["Catch2_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo) | ["Catch2_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo) | [[["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | [[["Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo)] | "Catch2_8" \in [1, oo) && "Fork_7" \in [1, oo)]] | "Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo)]]]] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)]]]]]]]]]]]]]]] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)]] | "Catch2_50" \in [1, oo) && "Fork_49" \in [1, oo)]]]] | "Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo)]]]]] | "Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo)]]] | "Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo)]]]]] | "Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo)]] | "Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo)] | [["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [[["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | [["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \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) | ["Think_12" \in [1, oo) && "Fork_11" \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_7" \in [1, oo) && "Think_8" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [["Fork_6" \in [1, oo) && "Think_7" \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) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]]]] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)]] | "Fork_40" \in [1, oo) && "Think_41" \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)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)]]] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)]] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)]] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)]]]
normalized: E [true U [[["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [[["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | [["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | [["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \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) | ["Think_12" \in [1, oo) && "Fork_11" \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_7" \in [1, oo) && "Think_8" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [["Fork_6" \in [1, oo) && "Think_7" \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) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]]]] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)]] | "Fork_40" \in [1, oo) && "Think_41" \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)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)]]]]]]]]]]]]]]]]]]]] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)]]] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)]]]] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)]] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)]] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)] | ["Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo) | [["Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo) | [[[[["Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo) | [[["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo) | [[[[["Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo) | [[[["Catch2_50" \in [1, oo) && "Fork_49" \in [1, oo) | [["Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo) | [[[[[[[[[[[[[[["Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo) | ["Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo) | [[[["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | [["Catch2_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | [["Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo) | "Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)]]] | "Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo)] | "Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo)]]] | "Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo)] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Catch2_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)] | "Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo)] | "Catch2_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo)] | "Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo)] | "Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo)] | "Catch2_41" \in [1, oo) && "Fork_40" \in [1, oo)]] | "Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo)]] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo)]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)] | "Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo)] | "Catch2_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo)]]] | "Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo)] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)]] | "Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo)] | "Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo)] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo)]]]]

-> the formula is TRUE

FORMULA p_1842_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[["Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo) | [[[[["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | [[[[[[[[[[[["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | [[["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo) | [[["Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo) | [[[["Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo) | [[[[["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Fork_1" \in [1, oo) && "Catch2_2" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo) | ["Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | [["Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo) | "Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo)]]]]]]] | "Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)]] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo)]] | "Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)]]] | "Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo)]]] | "Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo)] | "Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo)] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)] | "Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo)]] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo)] | "Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo)]]] | "Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo)] | "Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo)] & [[[[[["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \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) | [[[["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | [[["Think_27" \in [1, oo) && "Fork_26" \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_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | [["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Fork_46" \in [1, oo) && "Think_47" \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) | [[[["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_14" \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_4" \in [1, oo) && "Think_5" \in [1, oo)]]] | "Fork_32" \in [1, oo) && "Think_33" \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_17" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)]] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)]]] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)]]]]] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \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_9" \in [1, oo) && "Think_10" \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)] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[["Think_34" \in [1, oo) && "Fork_33" \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) | [[["Fork_9" \in [1, oo) && "Think_10" \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_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | [[[[["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | [[["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | [["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | [["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_18" \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_32" \in [1, oo) && "Think_33" \in [1, oo) | [[["Fork_4" \in [1, oo) && "Think_5" \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)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_26" \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_46" \in [1, oo) && "Think_47" \in [1, oo)]]] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \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)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)]]] | "Fork_37" \in [1, oo) && "Think_38" \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)]] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)]]]]]] & ["Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo) | ["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo) | [["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo) | ["Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | ["Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo) | ["Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo) | [["Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo) | [[["Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo) | ["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | [["Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo) | [["Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo) | ["Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | [[[[[[["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)] | "Fork_1" \in [1, oo) && "Catch2_2" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo)]]]]] | "Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo)]]]] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)]]] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)]]] | "Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo)] | "Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo)]]] | "Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo)]]]]]]]]]]]] | "Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo)]]]]] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)]]]]]]]]


before gc: list nodes free: 1269308

after gc: idd nodes used:9413, unused:15990587; list nodes free:71259855
-> the formula is FALSE

FORMULA p_1843_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m27sec

checking: AG [[["Catch2_18" \in [1, oo) && "Fork_17" \in [1, oo) | [[["Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo) | [["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | [[["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | [["Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo) | [[[["Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | [[[[[["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | [["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo) | [[[[["Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo) | [[["Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | [[[[["Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo) | "Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)]] | "Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo)] | "Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo)]]] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo)]] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo)]] | "Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)]]] | "Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo)]]] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)] | "Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo)] | "Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo)]]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)] | "Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo)]] | "Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo)]]] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo)]] | "Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo)]]] | "Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo)]] | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | [["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | [[[[[["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | [["Fork_29" \in [1, oo) && "Think_30" \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_44" \in [1, oo) && "Think_45" \in [1, oo) | [[[[[[[[[["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \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_4" \in [1, oo) && "Think_5" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]] | "Fork_12" \in [1, oo) && "Think_13" \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_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_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_20" \in [1, oo) && "Think_21" \in [1, oo)]] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)]]] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \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_43" \in [1, oo) && "Think_44" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[[["Fork_43" \in [1, oo) && "Think_44" \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) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | [["Fork_20" \in [1, oo) && "Think_21" \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_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_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_12" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | [["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_5" \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_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)]]]]]]]]]] | "Fork_44" \in [1, oo) && "Think_45" \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_29" \in [1, oo) && "Think_30" \in [1, oo)]] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)]]]]]] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)]] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | [["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | [["Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo) | [[["Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo) | [["Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | ["Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo) | [[["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo) | ["Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo) | [[["Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo) | ["Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo) | ["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | [["Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo) | [["Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo) | [[["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | [["Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | [["Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)]]]]] | "Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)]]] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)]]] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)]]]]] | "Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo)]] | "Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo)]]]]]] | "Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo)] | "Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo)]]]] | "Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo)]] | "Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo)]]] | "Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo)]] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)]]] | "Catch2_18" \in [1, oo) && "Fork_17" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_1844_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m7sec

checking: AG [[["Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo) | [[[[[[[[["Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo) | [[[[["Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo) | [[[[[[[[[["Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo) | [[[["Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo) | ["Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo) | ["Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo) | [[[["Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo) | [[[["Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo) | [[[["Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo) | [["Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo) | "Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo)] | "Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo)]] | "Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo)]]] | "Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo)]]]]] | "Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo)]] | "Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo)] | "Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo)] | "Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo)] | "Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo)]] | "Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo)]]] | "Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo)] | "Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo)] | "Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo)] | "Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo)]] <-> EF [[[[[["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_16" \in [1, oo) | [[[[[[[["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | [[[[[[[["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | [[[["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | [[[["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | [[[[[[[[[[["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | [[["Fork_13" \in [1, oo) && "Think_14" \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_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \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_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)]]] | "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_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)] | "Think_17" \in [1, oo) && "Fork_16" \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 ~ [[[~ [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) | [[["Think_17" \in [1, oo) && "Fork_16" \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) | [[["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_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_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_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \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)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]]] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)]]]]]]]]]]] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)]]]] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)]]]] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)]]]]]]]] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)]]]]]]]] | "Fork_15" \in [1, oo) && "Think_16" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)]]]]]]] & ~ [[["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo) | [[["Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo) | ["Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | [["Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo) | ["Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | [["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo) | [[[[["Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | [["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)]]]] | "Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo)]]]] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo)]]]] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)] | "Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)]]]] | "Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo)]]]]]]]]]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)]]]]] | "Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo)]]]]]]]]] | "Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo)]]] | [[["Fork_4" \in [1, oo) && "Catch2_5" \in [1, oo) | ["Fork_24" \in [1, oo) && "Catch2_25" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch2_39" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch2_32" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch2_10" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch2_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch2_38" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch2_37" \in [1, oo) | [[["Fork_43" \in [1, oo) && "Catch2_44" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch2_3" \in [1, oo) | ["Fork_18" \in [1, oo) && "Catch2_19" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch2_16" \in [1, oo) | [["Fork_47" \in [1, oo) && "Catch2_48" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch2_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch2_35" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch2_13" \in [1, oo) | ["Fork_49" \in [1, oo) && "Catch2_50" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch2_23" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch2_22" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch2_41" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch2_9" \in [1, oo) | [["Fork_48" \in [1, oo) && "Catch2_49" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch2_43" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch2_42" \in [1, oo) | [[[[["Fork_30" \in [1, oo) && "Catch2_31" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch2_33" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch2_6" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Catch2_45" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch2_17" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch2_34" \in [1, oo) | [["Fork_11" \in [1, oo) && "Catch2_12" \in [1, oo) | ["Catch2_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch2_46" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Catch2_28" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch2_7" \in [1, oo) | "Catch2_1" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Catch2_26" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch2_8" \in [1, oo)]]]] | "Fork_23" \in [1, oo) && "Catch2_24" \in [1, oo)]]]] | "Fork_35" \in [1, oo) && "Catch2_36" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch2_14" \in [1, oo)]]]] | "Fork_28" \in [1, oo) && "Catch2_29" \in [1, oo)] | "Fork_46" \in [1, oo) && "Catch2_47" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch2_15" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch2_21" \in [1, oo)]]]] | "Fork_29" \in [1, oo) && "Catch2_30" \in [1, oo)]]]]]]]]]] | "Fork_3" \in [1, oo) && "Catch2_4" \in [1, oo)]]]]] | "Fork_26" \in [1, oo) && "Catch2_27" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch2_11" \in [1, oo)]]]]]]]]] | "Fork_17" \in [1, oo) && "Catch2_18" \in [1, oo)] & 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) | [[["Think_17" \in [1, oo) && "Fork_16" \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) | [[["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_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_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_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \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)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]]] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)]]]]]]]]]]] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)]]]] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)]]]] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)]]]]]]]] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)]]]]]]]] | "Fork_15" \in [1, oo) && "Think_16" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1845_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m11sec

checking: EG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Eat_41" \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_14" \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_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_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_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_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)] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_48" \in [1, oo) && "Think_48" \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_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)] | "Think_17" \in [1, oo) && "Fork_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)]]]
normalized: EG [[["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) | ["Think_17" \in [1, oo) && "Fork_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_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]]]]]] | "Fork_48" \in [1, oo) && "Think_48" \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_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_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_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_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_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_41" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

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

FORMULA p_1886_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m3sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \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)] | "Think_17" \in [1, oo) && "Fork_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_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)] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["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_14" \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_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_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_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_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_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_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_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)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ["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_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) | ["Think_17" \in [1, oo) && "Fork_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_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1887_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m7sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["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_14" \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_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_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_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)] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["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)] | "Think_17" \in [1, oo) && "Fork_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)]]]
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_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) | ["Think_17" \in [1, oo) && "Fork_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)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ["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_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_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_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)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1888_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m16sec


total processing time: 1m55sec

STOP 1369701076

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


iterations count:788 (3), effective:50 (0)
3844 3427 3052 2907 2712 2692 2332 2192 2062 1802 1722 1572 1373 1522
iterations count:14056 (56), effective:2400 (9)
1394 1362 1302 1402 1417 1572 1422 1457 1467 1382 1442 1432 1342 1517
iterations count:14625 (58), effective:2501 (10)
1762
iterations count:1232 (4), effective:147 (0)
1762
iterations count:1232 (4), effective:147 (0)
2093 1948 1924 2073 2125 2045 1852 2067 1822 1810 1798 1786 1774 1994
iterations count:14807 (59), effective:2533 (10)
1278 1288 1316 1434 1490 1486 1270 1566 1435 1449 1280 1266 1491 1505
iterations count:14963 (59), effective:2498 (9)
3079 2839 2667 2575 2509 2327 1955 2167 1936 1850 1740 1678 1592 1532
iterations count:14171 (56), effective:2402 (9)

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