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

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

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

execution on node 2: quadhexa-2.u-paris10.fr (runId=136968525300186_n_2)
=====================================================================
runnning marcie on Philosophers-PT-000100 (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-000100, examination is CTLFireability
=====================================================================

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

START 1369709161

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: 500 NrTr: 500)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


-> reachability set: #nodes 2580 (2.6e+03) #states 515,377,520,732,011,331,036,461,129,765,621,272,702,107,522,001 (47)



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

checking: EG [[["Catch1_78" \in [1, oo) && "Fork_78" \in [1, oo) | ["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | ["Catch1_77" \in [1, oo) && "Fork_77" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | ["Catch1_62" \in [1, oo) && "Fork_62" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | ["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | ["Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo) | ["Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo) | ["Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | ["Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo) | ["Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo) | ["Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo) | ["Catch1_84" \in [1, oo) && "Fork_84" \in [1, oo) | ["Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo) | ["Catch1_22" \in [1, oo) && "Fork_22" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo) | ["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | [[["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | [["Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo) | [["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | [[["Catch1_85" \in [1, oo) && "Fork_85" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | ["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | [["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | [[["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | ["Catch1_12" \in [1, oo) && "Fork_12" \in [1, oo) | ["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | ["Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo) | [[[[["Catch1_89" \in [1, oo) && "Fork_89" \in [1, oo) | [[["Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo) | [[["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | ["Catch1_65" \in [1, oo) && "Fork_65" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | ["Catch1_14" \in [1, oo) && "Fork_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | [[[[["Catch1_87" \in [1, oo) && "Fork_87" \in [1, oo) | [[[[["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | [[["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | [["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | ["Catch1_33" \in [1, oo) && "Fork_33" \in [1, oo) | [["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | ["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | [[["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | [[["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | [["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | [[[[["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)]]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)] | "Catch1_88" \in [1, oo) && "Fork_88" \in [1, oo)] | "Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo)] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)]]] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)]]] | "Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo)] | "Catch1_66" \in [1, oo) && "Fork_66" \in [1, oo)]] | "Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo)] | "Catch1_61" \in [1, oo) && "Fork_61" \in [1, oo)]]]] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)]]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)]]] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)] | "Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo)]] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)]] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)]]]]]]] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)] | "Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo)]] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)]] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo)] | "Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo)]]]]] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)]]] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)]]]] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]] | "Catch1_67" \in [1, oo) && "Fork_67" \in [1, oo)]] | "Catch1_64" \in [1, oo) && "Fork_64" \in [1, oo)]] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]] & ["Fork_82" \in [1, oo) && "Think_83" \in [1, oo) | [["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | [[[[[[[[[["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | [[["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | [[["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | [[[[[[["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | [["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | [["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | [[[["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_80" \in [1, oo) && "Think_81" \in [1, oo) | [["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | [["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [[[["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Fork_67" \in [1, oo) && "Think_68" \in [1, oo) | [[[["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | [[["Fork_94" \in [1, oo) && "Think_95" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | [[[["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_76" \in [1, oo) && "Think_77" \in [1, oo) | [[[[["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | [["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | [["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | [[[["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]] | "Fork_72" \in [1, oo) && "Think_73" \in [1, oo)] | "Fork_84" \in [1, oo) && "Think_85" \in [1, oo)] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)]] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)]]] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)]]]]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Fork_85" \in [1, oo) && "Think_86" \in [1, oo)]] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)]]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)] | "Fork_2" \in [1, oo) && "Think_3" \in [1, oo)] | "Fork_53" \in [1, oo) && "Think_54" \in [1, oo)]]]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)]]]]] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)]]]] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)]] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]] | "Fork_56" \in [1, oo) && "Think_57" \in [1, oo)]] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)]]] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)]]] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)]]] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]] | "Fork_99" \in [1, oo) && "Think_100" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]] | "Fork_71" \in [1, oo) && "Think_72" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)]]]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)]]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)]]]]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)]]]]
normalized: EG [[["Fork_82" \in [1, oo) && "Think_83" \in [1, oo) | [["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | [[[[[[[[[["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | [[["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | [[["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | [[[[[[["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | [["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | [["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | [[[["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_80" \in [1, oo) && "Think_81" \in [1, oo) | [["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | [["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [[[["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Fork_67" \in [1, oo) && "Think_68" \in [1, oo) | [[[["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | [[["Fork_94" \in [1, oo) && "Think_95" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | [[[["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_76" \in [1, oo) && "Think_77" \in [1, oo) | [[[[["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | [["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | [["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | [[[["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]] | "Fork_72" \in [1, oo) && "Think_73" \in [1, oo)] | "Fork_84" \in [1, oo) && "Think_85" \in [1, oo)] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)]] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)]]] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)]]]]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Fork_85" \in [1, oo) && "Think_86" \in [1, oo)]] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)]]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)] | "Fork_2" \in [1, oo) && "Think_3" \in [1, oo)] | "Fork_53" \in [1, oo) && "Think_54" \in [1, oo)]]]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)]]]]] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)]]]] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)]] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]] | "Fork_56" \in [1, oo) && "Think_57" \in [1, oo)]] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)]]] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)]]] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)]]] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]] | "Fork_99" \in [1, oo) && "Think_100" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]] | "Fork_71" \in [1, oo) && "Think_72" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)]]]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)]]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)]]]]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)]] & [[[[[[[[[[[[[[[[[[[[[[["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo) | [["Catch1_64" \in [1, oo) && "Fork_64" \in [1, oo) | [["Catch1_67" \in [1, oo) && "Fork_67" \in [1, oo) | [["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | ["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | [[[["Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo) | [[[[[[["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | ["Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo) | ["Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo) | ["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | ["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Catch1_89" \in [1, oo) && "Fork_89" \in [1, oo) | ["Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo) | ["Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo) | ["Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo) | ["Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | ["Catch1_65" \in [1, oo) && "Fork_65" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | ["Catch1_14" \in [1, oo) && "Fork_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo) | ["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Catch1_87" \in [1, oo) && "Fork_87" \in [1, oo) | ["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | ["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | ["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | ["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | ["Catch1_33" \in [1, oo) && "Fork_33" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | ["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | ["Catch1_61" \in [1, oo) && "Fork_61" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Catch1_66" \in [1, oo) && "Fork_66" \in [1, oo) | ["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | ["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | ["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | ["Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo) | ["Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo) | ["Catch1_88" \in [1, oo) && "Fork_88" \in [1, oo) | [["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)]]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Catch1_12" \in [1, oo) && "Fork_12" \in [1, oo)] | "Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo)] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo)]] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)] | "Catch1_85" \in [1, oo) && "Fork_85" \in [1, oo)]]] | "Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo)]] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)]] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)]]] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)] | "Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo)] | "Catch1_22" \in [1, oo) && "Fork_22" \in [1, oo)] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)] | "Catch1_84" \in [1, oo) && "Fork_84" \in [1, oo)] | "Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo)] | "Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo)] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)] | "Catch1_62" \in [1, oo) && "Fork_62" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo)] | "Catch1_77" \in [1, oo) && "Fork_77" \in [1, oo)] | "Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo)] | "Catch1_78" \in [1, oo) && "Fork_78" \in [1, oo)]]]

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

FORMULA p_1841_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m10sec

checking: AG [[[["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | [["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | [["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | ["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | [[[[["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | [[["Catch1_86" \in [1, oo) && "Fork_86" \in [1, oo) | ["Catch1_72" \in [1, oo) && "Fork_72" \in [1, oo) | ["Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo) | [["Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo) | [["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | [["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | ["Catch1_64" \in [1, oo) && "Fork_64" \in [1, oo) | [[[["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | [["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | [[["Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo) | [[["Catch1_18" \in [1, oo) && "Fork_18" \in [1, oo) | ["Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo) | ["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | [["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | [["Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo) | [["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | ["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo) | [["Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo) | ["Catch1_93" \in [1, oo) && "Fork_93" \in [1, oo) | [[["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | ["Catch1_65" \in [1, oo) && "Fork_65" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | ["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo) | ["Catch1_7" \in [1, oo) && "Fork_7" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo) | ["Catch1_44" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | ["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | ["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Catch1_53" \in [1, oo) && "Fork_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | ["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Catch1_49" \in [1, oo) && "Fork_49" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | ["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | ["Catch1_37" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | ["Catch1_30" \in [1, oo) && "Fork_30" \in [1, oo) | ["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | ["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | ["Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo) | ["Fork_76" \in [1, oo) && "Catch1_76" \in [1, oo) | ["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo) | ["Catch1_97" \in [1, oo) && "Fork_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | ["Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo) | ["Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)] | "Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo)]]] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)]]]] | "Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo)]] | "Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo)]] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)]]]] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo)]] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)]] | "Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo)] | "Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)]]] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)]] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)]]] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)]]]] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)]]] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)]]] | "Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo)]] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)]] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)] | ["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Fork_75" \in [1, oo) && "Think_76" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Fork_95" \in [1, oo) && "Think_96" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Think_62" \in [1, oo) | [["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | [["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | [[["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | ["Fork_52" \in [1, oo) && "Think_53" \in [1, oo) | [[["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[[["Fork_70" \in [1, oo) && "Think_71" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Fork_56" \in [1, oo) && "Think_57" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Fork_2" \in [1, oo) && "Think_3" \in [1, oo) | ["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Fork_65" \in [1, oo) && "Think_66" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Fork_72" \in [1, oo) && "Think_73" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)]]]] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]]] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]]] | "Fork_62" \in [1, oo) && "Think_63" \in [1, oo)]] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | [["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | [["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | ["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | [["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | [[[["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | [["Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo) | [["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | [[[["Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo) | [[["Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo) | "Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)] | "Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo)] | "Catch1_97" \in [1, oo) && "Fork_97" \in [1, oo)] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)] | "Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo)] | "Fork_76" \in [1, oo) && "Catch1_76" \in [1, oo)] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)] | "Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo)] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo)] | "Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo)] | "Catch1_30" \in [1, oo) && "Fork_30" \in [1, oo)] | "Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo)] | "Catch1_37" \in [1, oo) && "Fork_37" \in [1, oo)] | "Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo)] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)] | "Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo)] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)] | "Catch1_49" \in [1, oo) && "Fork_49" \in [1, oo)] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo)] | "Catch1_53" \in [1, oo) && "Fork_53" \in [1, oo)] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)] | "Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo)] | "Catch1_44" \in [1, oo) && "Fork_44" \in [1, oo)] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)] | "Catch1_7" \in [1, oo) && "Fork_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)] | "Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo)] | "Catch1_65" \in [1, oo) && "Fork_65" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo)]]] | "Catch1_93" \in [1, oo) && "Fork_93" \in [1, oo)] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)]] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)]] | "Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo)]] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)]] | "Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo)] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Catch1_18" \in [1, oo) && "Fork_18" \in [1, oo)]]] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)]]] | "Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo)]] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]]] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)] | "Catch1_64" \in [1, oo) && "Fork_64" \in [1, oo)] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)] | "Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo)] | "Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo)] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)] | "Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo)] | "Catch1_72" \in [1, oo) && "Fork_72" \in [1, oo)] | "Catch1_86" \in [1, oo) && "Fork_86" \in [1, oo)] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)] | "Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo)] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)] | "Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo)] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)] | ["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Fork_75" \in [1, oo) && "Think_76" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Fork_95" \in [1, oo) && "Think_96" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Think_62" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Fork_62" \in [1, oo) && "Think_63" \in [1, oo) | ["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | ["Fork_52" \in [1, oo) && "Think_53" \in [1, oo) | ["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | [["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Fork_70" \in [1, oo) && "Think_71" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Fork_56" \in [1, oo) && "Think_57" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Fork_2" \in [1, oo) && "Think_3" \in [1, oo) | ["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Fork_65" \in [1, oo) && "Think_66" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Fork_72" \in [1, oo) && "Think_73" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)]]]]]]]]]]]]]]] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)]]]]]]


before gc: list nodes free: 1906424

after gc: idd nodes used:10911, unused:15989089; list nodes free:71250061
-> the formula is FALSE

FORMULA p_1842_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 2m5sec

checking: AG [[[["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | [["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | [[["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | [[["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | [["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Think_62" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | ["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | ["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | ["Fork_93" \in [1, oo) && "Think_94" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | ["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | [[[["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_67" \in [1, oo) && "Think_68" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_77" \in [1, oo) && "Think_78" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | [[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | [["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | [["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | [[["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | [[[["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)]] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)]]] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)]]] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)]]]]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)]] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Fork_81" \in [1, oo) && "Think_82" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)]] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)]]] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)]]]]] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)]]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)] & ["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo) | [[[[["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | [[["Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo) | [[[[[[[["Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo) | ["Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo) | ["Catch1_31" \in [1, oo) && "Fork_31" \in [1, oo) | [[["Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo) | ["Catch1_63" \in [1, oo) && "Fork_63" \in [1, oo) | ["Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo) | [[["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | ["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | ["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | ["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | [[[[[[[[[["Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo) | ["Catch1_69" \in [1, oo) && "Fork_69" \in [1, oo) | [[[["Catch1_89" \in [1, oo) && "Fork_89" \in [1, oo) | ["Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo) | [[["Fork_81" \in [1, oo) && "Catch1_81" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | ["Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo) | ["Catch1_34" \in [1, oo) && "Fork_34" \in [1, oo) | [[[["Catch1_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo) | [[["Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo) | ["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | [[[[["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | ["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | ["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | [["Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | [[["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | [["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | [[[[["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | [[["Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo) | ["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo) | [["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | [[["Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo) | "Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)]] | "Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo)]]]] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)]] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)] | "Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo)] | "Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo)]]]] | "Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo)]] | "Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo)]]] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)]]]]]] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo)]]] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)] | "Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo)]]]]]] | "Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo)] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)]]] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo)]]] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)] | "Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo)] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo)] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)]]]]]] | "Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)]]]] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)]]]]] | "Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo)] | "Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo)] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)]] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)]] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)] | "Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo)] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)]]]]]
normalized: ~ [E [true U ~ [[[[["Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | ["Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | [["Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo) | [["Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | ["Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo) | ["Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo) | ["Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo) | [[[[["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | ["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | [[[["Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo) | ["Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo) | [[[[[["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | ["Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | ["Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo) | ["Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo) | ["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | ["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | [[["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | ["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | [[["Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo) | ["Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo) | [[[[[["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | ["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | [[["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | ["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | [[[[[["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | [[["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | [["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | [[[["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | ["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | ["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | [["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | ["Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo) | [[[["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | [["Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo) | ["Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo) | ["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)]]] | "Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo)]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)] | "Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo)] | "Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo)]]] | "Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo)]]]]] | "Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo)]] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)]]] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo)] | "Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo)] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)] | "Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo)]]]]] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)]]] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Catch1_2" \in [1, oo) && "Fork_2" \in [1, oo)]]]] | "Catch1_34" \in [1, oo) && "Fork_34" \in [1, oo)] | "Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo)] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)] | "Fork_81" \in [1, oo) && "Catch1_81" \in [1, oo)]]] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)] | "Catch1_89" \in [1, oo) && "Fork_89" \in [1, oo)]]]] | "Catch1_69" \in [1, oo) && "Fork_69" \in [1, oo)] | "Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo)]]]]]]]]]] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)] | "Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)] | "Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo)]]] | "Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo)] | "Catch1_63" \in [1, oo) && "Fork_63" \in [1, oo)] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)]]] | "Catch1_31" \in [1, oo) && "Fork_31" \in [1, oo)] | "Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo)] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)] | "Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo)]]]]]]]] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)]]] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)]]]]] | "Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo)] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)] & ["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [[["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[[[["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | [[["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | [["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_81" \in [1, oo) && "Think_82" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | [["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | [[[[["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | [[["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | [[["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | [["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)]]]] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)]]] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)]] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)]] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)]]] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_77" \in [1, oo) && "Think_78" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Fork_67" \in [1, oo) && "Think_68" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)]]]] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)] | "Fork_93" \in [1, oo) && "Think_94" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Fork_61" \in [1, oo) && "Think_62" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)]]] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)]]] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)]] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)]]]]]]


before gc: list nodes free: 1765098

after gc: idd nodes used:22283, unused:15977717; list nodes free:71200368
-> the formula is FALSE

FORMULA p_1843_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 4m16sec

checking: AF [[[[[[["Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo) | [[[[[["Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo) | [[[["Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo) | [[["Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo) | ["Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo) | ["Catch1_22" \in [1, oo) && "Fork_22" \in [1, oo) | [["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | ["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo) | [[["Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | [[[["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | ["Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo) | ["Catch1_92" \in [1, oo) && "Fork_92" \in [1, oo) | [["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | ["Catch1_27" \in [1, oo) && "Fork_27" \in [1, oo) | [["Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo) | ["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | [[["Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo) | [[["Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo) | ["Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo) | ["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | [["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | [[[["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | ["Catch1_13" \in [1, oo) && "Fork_13" \in [1, oo) | ["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | [[["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | [["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | ["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | [[["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | [["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | ["Catch1_23" \in [1, oo) && "Fork_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | ["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | ["Catch1_55" \in [1, oo) && "Fork_55" \in [1, oo) | [["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | ["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | [["Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo) | ["Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo) | [["Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo) | [[["Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo) | ["Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo) | ["Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo) | "Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo)]]] | "Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo)] | "Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo)]] | "Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo)]]] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)]]] | "Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo)]]]]]] | "Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo)]] | "Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo)]] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)]]]] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)]]]] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)] | "Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo)]] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)]]]] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)] | "Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo)]] | "Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo)]]]] | "Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo)] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)]] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)]]]] | "Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo)]]] | "Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo)]]]] | "Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo)] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)]] | "Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)]] | "Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo)] | "Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo)]] | "Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo)] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)]]]] | "Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo)]]]] | "Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo)] | "Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)]] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)]] | "Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo)] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)] | "Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo)] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | [[[[[[[[[[[[["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | [[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[[[[[[[["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | [[["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | [[[[[[[[[[[[[[[[["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Fork_59" \in [1, oo) && "Think_60" \in [1, oo) | [["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | [[["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | [[["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | [[[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | [["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | [[[["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | [[["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)]] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)]]]]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)]]]] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)]]]] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)]] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)]]]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)]]] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)]] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)]] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)]] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)]]]
normalized: ~ [EG [~ [[["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | [["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | ["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | ["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | ["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | [["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | [["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | [[["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [[[["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | [[["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | [[[["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | [[[["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[[[["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | [["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)]]] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)]]]] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)]] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)]]]] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)]] | "Fork_59" \in [1, oo) && "Think_60" \in [1, oo)] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)]]]]]]]]]]]]]]]]] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)]]] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)]]]]]]]]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)]]] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]]]]]]]]]]]]] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)]]]]]]]]]]]]]]]]]]]]] | ["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | ["Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | [["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | ["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | ["Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo) | ["Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo) | [["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | [["Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo) | ["Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo) | [[[["Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo) | [[[["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | ["Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo) | [["Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | [["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | ["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | [["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | ["Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | [[[["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | [[["Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo) | [[[["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo) | [["Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo) | ["Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo) | [[[["Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo) | [["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | ["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | [[[["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo) | [["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | ["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | [[[["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | [[[["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo) | [["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | [["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | [[[[[["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | [[["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | [[["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | [["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | [[["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)]]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)]] | "Catch1_76" \in [1, oo) && "Fork_76" \in [1, oo)] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)]] | "Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo)] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)]] | "Catch1_55" \in [1, oo) && "Fork_55" \in [1, oo)] | "Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo)] | "Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo)] | "Catch1_23" \in [1, oo) && "Fork_23" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo)]] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)]]] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)]]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo)] | "Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo)]] | "Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)]]] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Catch1_13" \in [1, oo) && "Fork_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)]]]] | "Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo)]] | "Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo)] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)] | "Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo)]]] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)]]] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo)] | "Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo)]] | "Catch1_27" \in [1, oo) && "Fork_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)]] | "Catch1_92" \in [1, oo) && "Fork_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)]]]] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)]]] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]]] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)]]] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)]] | "Catch1_22" \in [1, oo) && "Fork_22" \in [1, oo)] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)] | "Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo)]]] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)]]]] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)]]]]]] | "Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo)]]]]]]]]]


before gc: list nodes free: 1465301

after gc: idd nodes used:15381, unused:15984619; list nodes free:71230571
.....................
before gc: list nodes free: 2171468

after gc: idd nodes used:188310, unused:15811690; list nodes free:70466777
.............
before gc: list nodes free: 2173733

after gc: idd nodes used:172673, unused:15827327; list nodes free:70535403
.................
EG iterations: 51
-> the formula is TRUE

FORMULA p_1844_fireability_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 4m27sec

checking: AG [A [["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | [[["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_100" \in [1, oo) | [[[["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | [[[[["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | [[["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | [[["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | [["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | [[["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | [[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | [["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[[[[["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | [["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | [[["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | [[["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | [[[["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | [[["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | [[["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | [[[[[["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | ["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | [[["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | [[[["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)]]]]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]]] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)]]]] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)]]]] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)]] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)]] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)]]]] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)]] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)]]] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]]]] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)]]]] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)]]] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)]] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)]]]] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)]] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)]]]]]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)]] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)]]] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)]]] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)]] U AF [["Catch1_78" \in [1, oo) && "Fork_78" \in [1, oo) | [[[[[["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | ["Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo) | ["Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo) | ["Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo) | [[[[[[[[[[[[["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo) | [[[[[["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | [[[["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | ["Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo) | [[["Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo) | ["Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | ["Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo) | [[[[[["Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo) | ["Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo) | ["Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo) | [["Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo) | [["Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo) | [[[["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo) | ["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | ["Catch1_38" \in [1, oo) && "Fork_38" \in [1, oo) | [[[[[[[["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | [["Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo) | [[[["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | [[[[[["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | [["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | [[["Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo) | ["Fork_76" \in [1, oo) && "Catch1_76" \in [1, oo) | ["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo) | [[[["Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo) | ["Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo) | "Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo)]] | "Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo)] | "Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo)] | "Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo)]]]]] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)] | "Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo)]] | "Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo)]] | "Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo)] | "Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo)] | "Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo)] | "Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo)]] | "Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo)] | "Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo)] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)]] | "Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo)] | "Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo)] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)] | "Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo)] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)]]] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)]]]]] | "Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo)] | "Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo)]] | "Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo)]] | "Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo)]]]] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo)] | "Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo)]]] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)] | "Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo)]]] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)] | "Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo)]]] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)] | "Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo)] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)]] | "Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo)] | "Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo)] | "Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo)] | "Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo)] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)]]] | "Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo)] | "Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo)] | "Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo)] | "Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo)] | "Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo)] | "Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo)] | "Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo)] | "Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)] | "Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo)]]]]] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)] | "Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo)] | "Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo)] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)] | "Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo)]]]]]
normalized: ~ [E [true U ~ [[~ [EG [EG [~ [[["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | ["Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | ["Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | [[[[["Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | ["Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo) | ["Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo) | ["Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo) | ["Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo) | ["Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo) | ["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | [[["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | ["Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo) | ["Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | [["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | ["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | [[["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | [[["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | [[["Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo) | ["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | ["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo) | [[[["Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo) | [["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | [["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | ["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | [[[[["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo) | [[["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | ["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | [["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | [["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | [["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | ["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | [["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | [["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | [[[[["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | ["Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo) | [["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)]]]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)] | "Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo)] | "Fork_76" \in [1, oo) && "Catch1_76" \in [1, oo)] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)]]] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)]] | "Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo)]]]]]] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)]]]] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)]]]]]]]] | "Catch1_38" \in [1, oo) && "Fork_38" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)]]]] | "Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo)]] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)]] | "Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo)] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)]]]]]] | "Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)]]] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)]]] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)]]]] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]]]]]] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)]]]]]]]]]]]]] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)]]]]]] | "Catch1_78" \in [1, oo) && "Fork_78" \in [1, oo)]]]]] & ~ [E [~ [[["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | [[["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | [[["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | [["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | [[[[[["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | [["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | [[[["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | ["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | [["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | [[[["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | [[[["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | [[["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | [["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | [[[["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | [["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | [["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [[[["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | [[[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | [[[["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[[[["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]]]] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)]]] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)]]]]]] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)]]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)]]] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)]]] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)]] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)]]]]]] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)]]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)]] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)]]] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]]] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)]]] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]]]]] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)]]]] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)]]] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)]] U [~ [[["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | [[["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | [[["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | [["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | [[[[[["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | [["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | [[[["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | ["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | [["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | [[[["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | [[[["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | [[["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | [["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | [[[["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | [["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | [["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [[[["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | [[[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | [[[["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[[[["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]]]] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)]]] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)]]]]]] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)]]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)]]] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)]]] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)]] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)]]]]]] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)]]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)]] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)]]] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]]] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)]]] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]]]]] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)]]]] | "Think_1" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)]]] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)]] & EG [~ [[["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | ["Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo) | ["Fork_43" \in [1, oo) && "Catch1_43" \in [1, oo) | ["Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo) | ["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | [[[[["Fork_39" \in [1, oo) && "Catch1_39" \in [1, oo) | ["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | ["Fork_1" \in [1, oo) && "Catch1_1" \in [1, oo) | ["Fork_86" \in [1, oo) && "Catch1_86" \in [1, oo) | ["Fork_72" \in [1, oo) && "Catch1_72" \in [1, oo) | ["Fork_84" \in [1, oo) && "Catch1_84" \in [1, oo) | ["Fork_82" \in [1, oo) && "Catch1_82" \in [1, oo) | ["Fork_22" \in [1, oo) && "Catch1_22" \in [1, oo) | ["Fork_31" \in [1, oo) && "Catch1_31" \in [1, oo) | ["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | [[["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | ["Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo) | ["Fork_19" \in [1, oo) && "Catch1_19" \in [1, oo) | ["Fork_67" \in [1, oo) && "Catch1_67" \in [1, oo) | ["Fork_29" \in [1, oo) && "Catch1_29" \in [1, oo) | [["Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo) | ["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | ["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | [[["Fork_40" \in [1, oo) && "Catch1_40" \in [1, oo) | ["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | [[["Fork_59" \in [1, oo) && "Catch1_59" \in [1, oo) | ["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | [[["Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo) | ["Fork_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo) | ["Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo) | [[[["Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo) | [["Fork_11" \in [1, oo) && "Catch1_11" \in [1, oo) | [["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | ["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Fork_58" \in [1, oo) && "Catch1_58" \in [1, oo) | [[[[["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo) | [[["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | ["Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo) | ["Fork_6" \in [1, oo) && "Catch1_6" \in [1, oo) | ["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | ["Fork_10" \in [1, oo) && "Catch1_10" \in [1, oo) | [["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | [["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | ["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | [["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | ["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | ["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | [["Fork_41" \in [1, oo) && "Catch1_41" \in [1, oo) | [["Fork_5" \in [1, oo) && "Catch1_5" \in [1, oo) | ["Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo) | [[[[["Fork_97" \in [1, oo) && "Catch1_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | ["Fork_90" \in [1, oo) && "Catch1_90" \in [1, oo) | [["Fork_25" \in [1, oo) && "Catch1_25" \in [1, oo) | "Fork_73" \in [1, oo) && "Catch1_73" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)]]]] | "Fork_47" \in [1, oo) && "Catch1_47" \in [1, oo)] | "Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo)] | "Fork_76" \in [1, oo) && "Catch1_76" \in [1, oo)] | "Fork_83" \in [1, oo) && "Catch1_83" \in [1, oo)]]] | "Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo)]] | "Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo)]]]]]] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)]]]] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)]]]]]]]] | "Catch1_38" \in [1, oo) && "Fork_38" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)]]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)]]]] | "Fork_65" \in [1, oo) && "Catch1_65" \in [1, oo)]] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)]] | "Fork_93" \in [1, oo) && "Catch1_93" \in [1, oo)] | "Fork_79" \in [1, oo) && "Catch1_79" \in [1, oo)] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)]]]]]] | "Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)]]] | "Fork_92" \in [1, oo) && "Catch1_92" \in [1, oo)] | "Fork_18" \in [1, oo) && "Catch1_18" \in [1, oo)]]] | "Fork_60" \in [1, oo) && "Catch1_60" \in [1, oo)] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)]]]] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]]]]]] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)]]]]]]]]]]]]] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)] | "Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo)] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)]]]]]] | "Catch1_78" \in [1, oo) && "Fork_78" \in [1, oo)]]]]]]]]]]

....
before gc: list nodes free: 1904198

after gc: idd nodes used:63181, unused:15936819; list nodes free:71021751
.......
before gc: list nodes free: 1238350

after gc: idd nodes used:122872, unused:15877128; list nodes free:70759729
....
before gc: list nodes free: 1190687

after gc: idd nodes used:140962, unused:15859038; list nodes free:70678149
.......
before gc: list nodes free: 1223317

after gc: idd nodes used:84400, unused:15915600; list nodes free:70928141
.....
EG iterations: 27
....
before gc: list nodes free: 1384370

after gc: idd nodes used:79621, unused:15920379; list nodes free:70947763
.......
before gc: list nodes free: 1235645

after gc: idd nodes used:137690, unused:15862310; list nodes free:70693163
....
before gc: list nodes free: 1189538

after gc: idd nodes used:165134, unused:15834866; list nodes free:70570672
.......
before gc: list nodes free: 1223496

after gc: idd nodes used:104397, unused:15895603; list nodes free:70838547
.....
EG iterations: 27
.
EG iterations: 1

before gc: list nodes free: 1343501

after gc: idd nodes used:69508, unused:15930492; list nodes free:70993575

before gc: list nodes free: 1456883

after gc: idd nodes used:64552, unused:15935448; list nodes free:71015219

before gc: list nodes free: 1449471

after gc: idd nodes used:60821, unused:15939179; list nodes free:71031499

before gc: list nodes free: 1435804

after gc: idd nodes used:56381, unused:15943619; list nodes free:71050896

before gc: list nodes free: 1391814

after gc: idd nodes used:50919, unused:15949081; list nodes free:71074736