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=ReachabilityMix
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Philosophers-PT-000100
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is Philosophers-PT-000100, examination is ReachabilityMix'
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=136968525100162_n_2)
=====================================================================
runnning marcie on Philosophers-PT-000100 (ReachabilityMix)
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 ReachabilityMix
=====================================================================

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

START 1369705886

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

-> the formula is FALSE

FORMULA p_37_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | ["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo) | ["Fork_77" \in [1, oo) && "Catch1_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) | ["Catch1_21" \in [1, oo) && "Fork_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo) | ["Catch1_1" \in [1, oo) && "Fork_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) | ["Fork_74" \in [1, oo) && "Catch1_74" \in [1, oo) | ["Catch1_75" \in [1, oo) && "Fork_75" \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_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_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_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) | ["Catch1_69" \in [1, oo) && "Fork_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_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) | ["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) | ["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | ["Catch1_42" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_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) | ["Catch1_71" \in [1, oo) && "Fork_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) | ["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) | ["Catch1_99" \in [1, oo) && "Fork_99" \in [1, oo) | ["Fork_17" \in [1, oo) && "Catch1_17" \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_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Catch1_41" \in [1, oo) && "Fork_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) | ["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) | [["Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo) | "Catch1_25" \in [1, oo) && "Fork_25" \in [1, oo)] | "Fork_52" \in [1, oo) && "Catch1_52" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)]]]]]] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \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_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)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["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_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_46" \in [1, oo) && "Catch1_46" \in [1, oo) | ["Catch1_69" \in [1, oo) && "Fork_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) | ["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) | ["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) | ["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | ["Catch1_42" \in [1, oo) && "Fork_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_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) | ["Catch1_71" \in [1, oo) && "Fork_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) | ["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) | ["Catch1_99" \in [1, oo) && "Fork_99" \in [1, oo) | ["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch1_37" \in [1, oo) | [["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | ["Fork_30" \in [1, oo) && "Catch1_30" \in [1, oo) | ["Fork_55" \in [1, oo) && "Catch1_55" \in [1, oo) | ["Catch1_41" \in [1, oo) && "Fork_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) | ["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) | ["Catch1_97" \in [1, oo) && "Fork_97" \in [1, oo) | ["Fork_70" \in [1, oo) && "Catch1_70" \in [1, oo) | [[["Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo) | "Catch1_25" \in [1, oo) && "Fork_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_5" \in [1, oo) && "Catch1_5" \in [1, oo)]]]]]] | "Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)]]]]] | "Fork_40" \in [1, oo) && "Catch1_40" \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)] | "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)] | "Catch1_63" \in [1, oo) && "Fork_63" \in [1, oo)] | "Fork_54" \in [1, oo) && "Catch1_54" \in [1, oo)] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)] | "Fork_74" \in [1, oo) && "Catch1_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)] | "Catch1_1" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_35" \in [1, oo) && "Catch1_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)] | "Catch1_21" \in [1, oo) && "Fork_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)] | "Fork_77" \in [1, oo) && "Catch1_77" \in [1, oo)] | "Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo)] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_38_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m12sec

checking: AG [[~ [["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo) | ["Catch1_77" \in [1, oo) && "Fork_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_50" \in [1, oo) && "Catch1_50" \in [1, oo) | ["Fork_56" \in [1, oo) && "Catch1_56" \in [1, oo) | [[[["Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Catch1_35" \in [1, oo) && "Fork_35" \in [1, oo) | ["Catch1_1" \in [1, oo) && "Fork_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) | ["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Fork_54" \in [1, oo) && "Catch1_54" \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) | ["Catch1_24" \in [1, oo) && "Fork_24" \in [1, oo) | ["Catch1_4" \in [1, oo) && "Fork_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_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_46" \in [1, oo) && "Catch1_46" \in [1, oo) | ["Fork_69" \in [1, oo) && "Catch1_69" \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) | ["Catch1_81" \in [1, oo) && "Fork_81" \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_42" \in [1, oo) && "Catch1_42" \in [1, oo) | [["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | [["Fork_36" \in [1, oo) && "Catch1_36" \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) | [[[[["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \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) | [[["Fork_41" \in [1, oo) && "Catch1_41" \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) | ["Catch1_88" \in [1, oo) && "Fork_88" \in [1, oo) | ["Catch1_47" \in [1, oo) && "Fork_47" \in [1, oo) | ["Catch1_97" \in [1, oo) && "Fork_97" \in [1, oo) | ["Catch1_70" \in [1, oo) && "Fork_70" \in [1, oo) | ["Catch1_90" \in [1, oo) && "Fork_90" \in [1, oo) | ["Catch1_52" \in [1, oo) && "Fork_52" \in [1, oo) | ["Catch1_25" \in [1, oo) && "Fork_25" \in [1, oo) | "Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo)]]]]]]]]] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)]] | "Fork_51" \in [1, oo) && "Catch1_51" \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_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)] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)]]] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)]] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)]] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)]]] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \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)] | "Fork_9" \in [1, oo) && "Catch1_9" \in [1, oo)]]]] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)]] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \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)]]]]]]]]]] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ~ [["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Catch1_68" \in [1, oo) && "Fork_68" \in [1, oo) | ["Catch1_77" \in [1, oo) && "Fork_77" \in [1, oo) | [["Fork_62" \in [1, oo) && "Catch1_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_21" \in [1, oo) && "Catch1_21" \in [1, oo) | ["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Catch1_35" \in [1, oo) && "Fork_35" \in [1, oo) | ["Catch1_1" \in [1, oo) && "Fork_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) | ["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Fork_54" \in [1, oo) && "Catch1_54" \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) | ["Catch1_24" \in [1, oo) && "Fork_24" \in [1, oo) | ["Catch1_4" \in [1, oo) && "Fork_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_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_46" \in [1, oo) && "Catch1_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) | ["Fork_89" \in [1, oo) && "Catch1_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_45" \in [1, oo) && "Catch1_45" \in [1, oo) | ["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | [[["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | [["Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo) | ["Fork_38" \in [1, oo) && "Catch1_38" \in [1, oo) | [["Fork_36" \in [1, oo) && "Catch1_36" \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) | [[[[["Fork_20" \in [1, oo) && "Catch1_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \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) | [[["Fork_41" \in [1, oo) && "Catch1_41" \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) | ["Catch1_88" \in [1, oo) && "Fork_88" \in [1, oo) | ["Catch1_47" \in [1, oo) && "Fork_47" \in [1, oo) | ["Catch1_97" \in [1, oo) && "Fork_97" \in [1, oo) | ["Catch1_70" \in [1, oo) && "Fork_70" \in [1, oo) | ["Catch1_90" \in [1, oo) && "Fork_90" \in [1, oo) | ["Catch1_52" \in [1, oo) && "Fork_52" \in [1, oo) | ["Catch1_25" \in [1, oo) && "Fork_25" \in [1, oo) | "Catch1_73" \in [1, oo) && "Fork_73" \in [1, oo)]]]]]]]]] | "Fork_15" \in [1, oo) && "Catch1_15" \in [1, oo)]] | "Fork_51" \in [1, oo) && "Catch1_51" \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_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)] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)]]] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)]] | "Fork_16" \in [1, oo) && "Catch1_16" \in [1, oo)]] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)]]] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)] | "Fork_13" \in [1, oo) && "Catch1_13" \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_65" \in [1, oo) && "Catch1_65" \in [1, oo)] | "Fork_11" \in [1, oo) && "Catch1_11" \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_43" \in [1, oo) && "Catch1_43" \in [1, oo)]]]]]]]]]

-> the formula is FALSE

FORMULA p_39_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | ~ [["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | [[[["Fork_62" \in [1, oo) && "Catch1_62" \in [1, oo) | ["Catch1_26" \in [1, oo) && "Fork_26" \in [1, oo) | ["Fork_50" \in [1, oo) && "Catch1_50" \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_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) | [[[["Catch1_74" \in [1, oo) && "Fork_74" \in [1, oo) | ["Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo) | ["Catch1_54" \in [1, oo) && "Fork_54" \in [1, oo) | ["Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo) | [[[[["Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo) | [[[[[[[["Fork_12" \in [1, oo) && "Catch1_12" \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_95" \in [1, oo) && "Catch1_95" \in [1, oo) | ["Fork_89" \in [1, oo) && "Catch1_89" \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_65" \in [1, oo) && "Catch1_65" \in [1, oo) | ["Fork_34" \in [1, oo) && "Catch1_34" \in [1, oo) | [[[[[[[[[[["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | [[[["Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo) | ["Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo) | [[["Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo) | ["Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo) | ["Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo) | ["Catch1_20" \in [1, oo) && "Fork_20" \in [1, oo) | ["Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo) | [[[["Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo) | ["Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo) | [[[["Fork_51" \in [1, oo) && "Catch1_51" \in [1, oo) | [[[[["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch1_47" \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_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)]]]]]]] | "Catch1_76" \in [1, oo) && "Fork_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_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_37" \in [1, oo) && "Catch1_37" \in [1, oo)] | "Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo)] | "Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo)]]]]]] | "Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_10" \in [1, oo) && "Catch1_10" \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_38" \in [1, oo) && "Catch1_38" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)] | "Fork_87" \in [1, oo) && "Catch1_87" \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_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_100" \in [1, oo) && "Catch1_100" \in [1, oo)] | "Fork_94" \in [1, oo) && "Catch1_94" \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_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_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_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_56" \in [1, oo) && "Catch1_56" \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 ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | ~ [[[[[[[[[[[[[[[[[[[[["Fork_22" \in [1, oo) && "Catch1_22" \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_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_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_94" \in [1, oo) && "Catch1_94" \in [1, oo) | ["Fork_100" \in [1, oo) && "Catch1_100" \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_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) | ["Fork_87" \in [1, oo) && "Catch1_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_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_10" \in [1, oo) && "Catch1_10" \in [1, oo) | ["Catch1_3" \in [1, oo) && "Fork_3" \in [1, oo) | [[[[[["Fork_17" \in [1, oo) && "Catch1_17" \in [1, oo) | ["Fork_61" \in [1, oo) && "Catch1_61" \in [1, oo) | ["Fork_37" \in [1, oo) && "Catch1_37" \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_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) | [[[[[[["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_70" \in [1, oo) && "Catch1_70" \in [1, oo)] | "Fork_97" \in [1, oo) && "Catch1_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_51" \in [1, oo) && "Catch1_51" \in [1, oo)]]]] | "Fork_66" \in [1, oo) && "Catch1_66" \in [1, oo)] | "Fork_23" \in [1, oo) && "Catch1_23" \in [1, oo)]]]] | "Fork_99" \in [1, oo) && "Catch1_99" \in [1, oo)] | "Catch1_20" \in [1, oo) && "Fork_20" \in [1, oo)] | "Fork_8" \in [1, oo) && "Catch1_8" \in [1, oo)] | "Fork_33" \in [1, oo) && "Catch1_33" \in [1, oo)] | "Fork_49" \in [1, oo) && "Catch1_49" \in [1, oo)]]] | "Fork_53" \in [1, oo) && "Catch1_53" \in [1, oo)] | "Fork_71" \in [1, oo) && "Catch1_71" \in [1, oo)]]]] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)]]]]]]]]]]] | "Fork_34" \in [1, oo) && "Catch1_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)] | "Catch1_81" \in [1, oo) && "Fork_81" \in [1, oo)]]] | "Fork_96" \in [1, oo) && "Catch1_96" \in [1, oo)] | "Fork_89" \in [1, oo) && "Catch1_89" \in [1, oo)] | "Fork_95" \in [1, oo) && "Catch1_95" \in [1, oo)]]] | "Fork_69" \in [1, oo) && "Catch1_69" \in [1, oo)] | "Catch1_46" \in [1, oo) && "Fork_46" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)]]]]]]]] | "Fork_48" \in [1, oo) && "Catch1_48" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Catch1_4" \in [1, oo)] | "Fork_24" \in [1, oo) && "Catch1_24" \in [1, oo)]]]]] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)] | "Catch1_54" \in [1, oo) && "Fork_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_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)] | "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_26" \in [1, oo) && "Fork_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)]]]]]]

-> the formula is FALSE

FORMULA p_40_mix_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m4sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ~ [[[["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_56" \in [1, oo) && "Catch1_56" \in [1, oo) | [["Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo) | ["Catch1_39" \in [1, oo) && "Fork_39" \in [1, oo) | [["Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo) | ["Catch1_35" \in [1, oo) && "Fork_35" \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_74" \in [1, oo) && "Fork_74" \in [1, oo) | ["Catch1_75" \in [1, oo) && "Fork_75" \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_24" \in [1, oo) && "Catch1_24" \in [1, oo) | [["Fork_85" \in [1, oo) && "Catch1_85" \in [1, oo) | ["Catch1_48" \in [1, oo) && "Fork_48" \in [1, oo) | ["Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo) | [[["Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo) | [[[["Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo) | ["Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo) | ["Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo) | [[["Fork_100" \in [1, oo) && "Catch1_100" \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_11" \in [1, oo) && "Catch1_11" \in [1, oo) | ["Catch1_65" \in [1, oo) && "Fork_65" \in [1, oo) | [["Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo) | ["Catch1_58" \in [1, oo) && "Fork_58" \in [1, oo) | [["Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo) | ["Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo) | [["Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo) | ["Fork_87" \in [1, oo) && "Catch1_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_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_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_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_70" \in [1, oo) && "Catch1_70" \in [1, oo)] | "Fork_97" \in [1, oo) && "Catch1_97" \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_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)] | "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_17" \in [1, oo) && "Catch1_17" \in [1, oo)] | "Fork_99" \in [1, oo) && "Catch1_99" \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_71" \in [1, oo) && "Catch1_71" \in [1, oo)]]] | "Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo)] | "Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo)]]]]] | "Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo)]]] | "Fork_34" \in [1, oo) && "Catch1_34" \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_94" \in [1, oo) && "Catch1_94" \in [1, oo)] | "Fork_69" \in [1, oo) && "Catch1_69" \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_40" \in [1, oo) && "Catch1_40" \in [1, oo)] | "Fork_60" \in [1, oo) && "Catch1_60" \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_54" \in [1, oo) && "Catch1_54" \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_1" \in [1, oo) && "Catch1_1" \in [1, oo)]]] | "Fork_21" \in [1, oo) && "Catch1_21" \in [1, oo)]]] | "Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo)]] | "Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo)] | "Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo)]]]] | "Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo)] | "Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_62 + Catch1_50 ) + Catch1_26 ) + Catch1_9 ) + Catch1_40 ) + Catch1_13 ) + Catch1_99 ) + Catch1_20 ) + Catch1_94 ) + Catch1_27 ) + Catch1_81 ) + Catch1_60 ) + Catch1_66 ) + Catch1_61 ) + Catch1_87 ) + Catch1_72 ) + Catch1_82 ) + Catch1_3 ) + Catch1_29 ) + Catch1_15 ) + Catch1_30 ) + Catch1_38 ) + Catch1_11 ) + Catch1_93 ) + Catch1_33 ) + Catch1_100 ) + Catch1_1 ) + Catch1_45 ) + Catch1_74 ) + Catch1_35 ) + Catch1_48 ) + Catch1_55 ) + Catch1_24 ) + Catch1_71 ) + Catch1_89 ) + Catch1_43 ) + Catch1_19 ) + Catch1_54 ) + Catch1_70 ) + Catch1_98 ) + Catch1_52 ) + Catch1_51 ) + Catch1_42 ) + Catch1_8 ) + Catch1_7 ) + Catch1_21 ) + Catch1_23 ) + Catch1_4 ) + Catch1_56 ) + Catch1_39 ) + Catch1_31 ) + Catch1_84 ) + Catch1_86 ) + Catch1_96 ) + Catch1_12 ) + Catch1_97 ) + Catch1_90 ) + Catch1_18 ) + Catch1_34 ) + Catch1_41 ) + Catch1_22 ) + Catch1_63 ) + Catch1_68 ) + Catch1_88 ) + Catch1_69 ) + Catch1_53 ) + Catch1_37 ) + Catch1_44 ) + Catch1_49 ) + Catch1_2 ) + Catch1_65 ) + Catch1_77 ) + Catch1_76 ) + Catch1_58 ) + Catch1_83 ) + Catch1_14 ) + Catch1_6 ) + Catch1_73 ) + Catch1_32 ) + Catch1_67 ) + Catch1_28 ) + Catch1_10 ) + Catch1_16 ) + Catch1_78 ) + Catch1_75 ) + Catch1_92 ) + Catch1_59 ) + Catch1_79 ) + Catch1_64 ) + Catch1_17 ) + Catch1_47 ) + Catch1_95 ) + Catch1_80 ) + Catch1_91 ) + Catch1_46 ) + Catch1_5 ) + Catch1_85 ) + Catch1_57 ) + Catch1_25 ) + Catch1_36 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ~ [["Fork_78" \in [1, oo) && "Catch1_78" \in [1, oo) | ["Fork_68" \in [1, oo) && "Catch1_68" \in [1, oo) | [[[["Fork_26" \in [1, oo) && "Catch1_26" \in [1, oo) | ["Fork_50" \in [1, oo) && "Catch1_50" \in [1, oo) | [["Fork_32" \in [1, oo) && "Catch1_32" \in [1, oo) | [[["Fork_21" \in [1, oo) && "Catch1_21" \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_31" \in [1, oo) && "Catch1_31" \in [1, oo) | [[["Fork_54" \in [1, oo) && "Catch1_54" \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_60" \in [1, oo) && "Catch1_60" \in [1, oo) | ["Fork_40" \in [1, oo) && "Catch1_40" \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_69" \in [1, oo) && "Catch1_69" \in [1, oo) | ["Fork_94" \in [1, oo) && "Catch1_94" \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_34" \in [1, oo) && "Catch1_34" \in [1, oo) | [[["Fork_45" \in [1, oo) && "Catch1_45" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Catch1_7" \in [1, oo) | [[[[["Fork_57" \in [1, oo) && "Catch1_57" \in [1, oo) | ["Fork_36" \in [1, oo) && "Catch1_36" \in [1, oo) | [[["Fork_71" \in [1, oo) && "Catch1_71" \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_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) | ["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_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) | ["Fork_88" \in [1, oo) && "Catch1_88" \in [1, oo) | ["Fork_47" \in [1, oo) && "Catch1_47" \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_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_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_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_38" \in [1, oo) && "Catch1_38" \in [1, oo)] | "Fork_44" \in [1, oo) && "Catch1_44" \in [1, oo)] | "Fork_87" \in [1, oo) && "Catch1_87" \in [1, oo)] | "Fork_42" \in [1, oo) && "Catch1_42" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Catch1_13" \in [1, oo)] | "Fork_2" \in [1, oo) && "Catch1_2" \in [1, oo)]] | "Catch1_58" \in [1, oo) && "Fork_58" \in [1, oo)] | "Fork_14" \in [1, oo) && "Catch1_14" \in [1, oo)]] | "Catch1_65" \in [1, oo) && "Fork_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_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)]]] | "Fork_100" \in [1, oo) && "Catch1_100" \in [1, oo)]]] | "Fork_46" \in [1, oo) && "Catch1_46" \in [1, oo)] | "Fork_27" \in [1, oo) && "Catch1_27" \in [1, oo)] | "Fork_12" \in [1, oo) && "Catch1_12" \in [1, oo)]]]] | "Fork_28" \in [1, oo) && "Catch1_28" \in [1, oo)]]] | "Fork_91" \in [1, oo) && "Catch1_91" \in [1, oo)] | "Catch1_48" \in [1, oo) && "Fork_48" \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)] | "Fork_64" \in [1, oo) && "Catch1_64" \in [1, oo)] | "Fork_63" \in [1, oo) && "Catch1_63" \in [1, oo)]] | "Catch1_75" \in [1, oo) && "Fork_75" \in [1, oo)] | "Catch1_74" \in [1, oo) && "Fork_74" \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_35" \in [1, oo) && "Fork_35" \in [1, oo)] | "Fork_98" \in [1, oo) && "Catch1_98" \in [1, oo)]] | "Catch1_39" \in [1, oo) && "Fork_39" \in [1, oo)] | "Catch1_80" \in [1, oo) && "Fork_80" \in [1, oo)]] | "Fork_56" \in [1, oo) && "Catch1_56" \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)]]]]]]]]

-> the formula is FALSE

FORMULA p_41_mix_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[Catch1_24>Eat_24 | [[[[[[[[[[[[[[[[Catch1_42>Eat_42 | [[[[[[[[[[[[[[[[[Catch1_100>Eat_100 | [[[[[[[[[[[[[[Catch1_63>Eat_63 | [[Catch1_61>Eat_61 | [[[[[[[Catch1_28>Eat_28 | [[[[[[[[[[[[[Catch1_30>Eat_30 | [[[[[[[[[Catch1_45>Eat_45 | [[[[[[Catch1_62>Eat_62 | [[Catch1_36>Eat_36 | [[[[[[[[false | Catch1_11>Eat_11] | Catch1_7>Eat_7] | Catch1_72>Eat_72] | Catch1_52>Eat_52] | Catch1_97>Eat_97] | Catch1_95>Eat_95] | Catch1_29>Eat_29] | Catch1_55>Eat_55]] | Catch1_49>Eat_49]] | Catch1_18>Eat_18] | Catch1_98>Eat_98] | Catch1_47>Eat_47] | Catch1_51>Eat_51] | Catch1_87>Eat_87]] | Catch1_6>Eat_6] | Catch1_32>Eat_32] | Catch1_59>Eat_59] | Catch1_50>Eat_50] | Catch1_57>Eat_57] | Catch1_12>Eat_12] | Catch1_85>Eat_85] | Catch1_96>Eat_96]] | Catch1_35>Eat_35] | Catch1_20>Eat_20] | Catch1_73>Eat_73] | Catch1_81>Eat_81] | Catch1_22>Eat_22] | Catch1_78>Eat_78] | Catch1_86>Eat_86] | Catch1_19>Eat_19] | Catch1_70>Eat_70] | Catch1_71>Eat_71] | Catch1_5>Eat_5] | Catch1_3>Eat_3]] | Catch1_94>Eat_94] | Catch1_8>Eat_8] | Catch1_76>Eat_76] | Catch1_31>Eat_31] | Catch1_89>Eat_89] | Catch1_90>Eat_90]] | Catch1_99>Eat_99]] | Catch1_65>Eat_65] | Catch1_4>Eat_4] | Catch1_58>Eat_58] | Catch1_53>Eat_53] | Catch1_54>Eat_54] | Catch1_9>Eat_9] | Catch1_56>Eat_56] | Catch1_26>Eat_26] | Catch1_92>Eat_92] | Catch1_38>Eat_38] | Catch1_68>Eat_68] | Catch1_44>Eat_44] | Catch1_27>Eat_27]] | Catch1_48>Eat_48] | Catch1_13>Eat_13] | Catch1_66>Eat_66] | Catch1_91>Eat_91] | Catch1_79>Eat_79] | Catch1_74>Eat_74] | Catch1_80>Eat_80] | Catch1_33>Eat_33] | Catch1_46>Eat_46] | Catch1_88>Eat_88] | Catch1_60>Eat_60] | Catch1_2>Eat_2] | Catch1_1>Eat_1] | Catch1_75>Eat_75] | Catch1_15>Eat_15] | Catch1_77>Eat_77]] | Catch1_17>Eat_17] | Catch1_67>Eat_67] | Catch1_10>Eat_10] | Catch1_23>Eat_23] | Catch1_25>Eat_25] | Catch1_83>Eat_83] | Catch1_34>Eat_34] | Catch1_14>Eat_14] | Catch1_84>Eat_84] | Catch1_21>Eat_21] | Catch1_43>Eat_43] | Catch1_37>Eat_37] | Catch1_40>Eat_40] | Catch1_69>Eat_69] | Catch1_64>Eat_64]] | Catch1_93>Eat_93] | Catch1_41>Eat_41] | Catch1_39>Eat_39] | Catch1_16>Eat_16] | Catch1_82>Eat_82] | false] & [[[[[[[[[[[[[[[[[[[[[[[[Catch1_77>Eat_77 & [[[[[[[[Catch1_33>Eat_33 & [[Catch1_74>Eat_74 & [[[[[[[[[Catch1_68>Eat_68 & [[[[Catch1_56>Eat_56 & [[[[[[[Catch1_63>Eat_63 & [[[[[[[[[[[Catch1_5>Eat_5 & [[[[Catch1_86>Eat_86 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch1_52>Eat_52 & [[[true & Catch1_11>Eat_11] & Catch1_7>Eat_7] & Catch1_72>Eat_72]] & Catch1_97>Eat_97] & Catch1_95>Eat_95] & Catch1_29>Eat_29] & Catch1_55>Eat_55] & Catch1_36>Eat_36] & Catch1_49>Eat_49] & Catch1_62>Eat_62] & Catch1_18>Eat_18] & Catch1_98>Eat_98] & Catch1_47>Eat_47] & Catch1_51>Eat_51] & Catch1_87>Eat_87] & Catch1_45>Eat_45] & Catch1_6>Eat_6] & Catch1_32>Eat_32] & Catch1_59>Eat_59] & Catch1_50>Eat_50] & Catch1_57>Eat_57] & Catch1_12>Eat_12] & Catch1_85>Eat_85] & Catch1_96>Eat_96] & Catch1_30>Eat_30] & Catch1_35>Eat_35] & Catch1_20>Eat_20] & Catch1_73>Eat_73] & Catch1_81>Eat_81] & Catch1_22>Eat_22] & Catch1_78>Eat_78]] & Catch1_19>Eat_19] & Catch1_70>Eat_70] & Catch1_71>Eat_71]] & Catch1_3>Eat_3] & Catch1_28>Eat_28] & Catch1_94>Eat_94] & Catch1_8>Eat_8] & Catch1_76>Eat_76] & Catch1_31>Eat_31] & Catch1_89>Eat_89] & Catch1_90>Eat_90] & Catch1_61>Eat_61] & Catch1_99>Eat_99]] & Catch1_65>Eat_65] & Catch1_4>Eat_4] & Catch1_58>Eat_58] & Catch1_53>Eat_53] & Catch1_54>Eat_54] & Catch1_9>Eat_9]] & Catch1_26>Eat_26] & Catch1_92>Eat_92] & Catch1_38>Eat_38]] & Catch1_44>Eat_44] & Catch1_27>Eat_27] & Catch1_100>Eat_100] & Catch1_48>Eat_48] & Catch1_13>Eat_13] & Catch1_66>Eat_66] & Catch1_91>Eat_91] & Catch1_79>Eat_79]] & Catch1_80>Eat_80]] & Catch1_46>Eat_46] & Catch1_88>Eat_88] & Catch1_60>Eat_60] & Catch1_2>Eat_2] & Catch1_1>Eat_1] & Catch1_75>Eat_75] & Catch1_15>Eat_15]] & Catch1_42>Eat_42] & Catch1_17>Eat_17] & Catch1_67>Eat_67] & Catch1_10>Eat_10] & Catch1_23>Eat_23] & Catch1_25>Eat_25] & Catch1_83>Eat_83] & Catch1_34>Eat_34] & Catch1_14>Eat_14] & Catch1_84>Eat_84] & Catch1_21>Eat_21] & Catch1_43>Eat_43] & Catch1_37>Eat_37] & Catch1_40>Eat_40] & Catch1_69>Eat_69] & Catch1_64>Eat_64] & Catch1_24>Eat_24] & Catch1_93>Eat_93] & Catch1_41>Eat_41] & Catch1_39>Eat_39] & Catch1_16>Eat_16] & Catch1_82>Eat_82] & true]] & [[[[[Catch1_93=Eat_93 & [[[[[[Catch1_43=Eat_43 & [[[[[[[[[Catch1_67=Eat_67 & [[[Catch1_77=Eat_77 & [[[Catch1_1=Eat_1 & [[[[[[Catch1_80=Eat_80 & [[[[[[[[[[[Catch1_38=Eat_38 & [[[[[[[[[[[[[[[[[[[[[[[[[Catch1_86=Eat_86 & [[[[[[[[[[[Catch1_57=Eat_57 & [[[[[Catch1_45=Eat_45 & [[[[[[[[[[[[[Catch1_52=Eat_52 & [[[Catch1_11=Eat_11 & true] & Catch1_7=Eat_7] & Catch1_72=Eat_72]] & Catch1_97=Eat_97] & Catch1_95=Eat_95] & Catch1_29=Eat_29] & Catch1_55=Eat_55] & Catch1_36=Eat_36] & Catch1_49=Eat_49] & Catch1_62=Eat_62] & Catch1_18=Eat_18] & Catch1_98=Eat_98] & Catch1_47=Eat_47] & Catch1_51=Eat_51] & Catch1_87=Eat_87]] & Catch1_6=Eat_6] & Catch1_32=Eat_32] & Catch1_59=Eat_59] & Catch1_50=Eat_50]] & Catch1_12=Eat_12] & Catch1_85=Eat_85] & Catch1_96=Eat_96] & Catch1_30=Eat_30] & Catch1_35=Eat_35] & Catch1_20=Eat_20] & Catch1_73=Eat_73] & Catch1_81=Eat_81] & Catch1_22=Eat_22] & Catch1_78=Eat_78]] & Catch1_19=Eat_19] & Catch1_70=Eat_70] & Catch1_71=Eat_71] & Catch1_5=Eat_5] & Catch1_3=Eat_3] & Catch1_28=Eat_28] & Catch1_94=Eat_94] & Catch1_8=Eat_8] & Catch1_76=Eat_76] & Catch1_31=Eat_31] & Catch1_89=Eat_89] & Catch1_90=Eat_90] & Catch1_61=Eat_61] & Catch1_99=Eat_99] & Catch1_63=Eat_63] & Catch1_65=Eat_65] & Catch1_4=Eat_4] & Catch1_58=Eat_58] & Catch1_53=Eat_53] & Catch1_54=Eat_54] & Catch1_9=Eat_9] & Catch1_56=Eat_56] & Catch1_26=Eat_26] & Catch1_92=Eat_92]] & Catch1_68=Eat_68] & Catch1_44=Eat_44] & Catch1_27=Eat_27] & Catch1_100=Eat_100] & Catch1_48=Eat_48] & Catch1_13=Eat_13] & Catch1_66=Eat_66] & Catch1_91=Eat_91] & Catch1_79=Eat_79] & Catch1_74=Eat_74]] & Catch1_33=Eat_33] & Catch1_46=Eat_46] & Catch1_88=Eat_88] & Catch1_60=Eat_60] & Catch1_2=Eat_2]] & Catch1_75=Eat_75] & Catch1_15=Eat_15]] & Catch1_42=Eat_42] & Catch1_17=Eat_17]] & Catch1_10=Eat_10] & Catch1_23=Eat_23] & Catch1_25=Eat_25] & Catch1_83=Eat_83] & Catch1_34=Eat_34] & Catch1_14=Eat_14] & Catch1_84=Eat_84] & Catch1_21=Eat_21]] & Catch1_37=Eat_37] & Catch1_40=Eat_40] & Catch1_69=Eat_69] & Catch1_64=Eat_64] & Catch1_24=Eat_24]] & Catch1_41=Eat_41] & Catch1_39=Eat_39] & Catch1_16=Eat_16] & Catch1_82=Eat_82]]]
normalized: ~ [E [true U ~ [[[Catch1_82=Eat_82 & [Catch1_16=Eat_16 & [Catch1_39=Eat_39 & [Catch1_41=Eat_41 & [Catch1_93=Eat_93 & [Catch1_24=Eat_24 & [Catch1_64=Eat_64 & [Catch1_69=Eat_69 & [Catch1_40=Eat_40 & [Catch1_37=Eat_37 & [Catch1_43=Eat_43 & [Catch1_21=Eat_21 & [Catch1_84=Eat_84 & [Catch1_14=Eat_14 & [Catch1_34=Eat_34 & [Catch1_83=Eat_83 & [Catch1_25=Eat_25 & [Catch1_23=Eat_23 & [Catch1_10=Eat_10 & [Catch1_67=Eat_67 & [Catch1_17=Eat_17 & [Catch1_42=Eat_42 & [Catch1_77=Eat_77 & [Catch1_15=Eat_15 & [Catch1_75=Eat_75 & [Catch1_1=Eat_1 & [Catch1_2=Eat_2 & [Catch1_60=Eat_60 & [Catch1_88=Eat_88 & [Catch1_46=Eat_46 & [Catch1_33=Eat_33 & [Catch1_80=Eat_80 & [Catch1_74=Eat_74 & [Catch1_79=Eat_79 & [Catch1_91=Eat_91 & [Catch1_66=Eat_66 & [Catch1_13=Eat_13 & [Catch1_48=Eat_48 & [Catch1_100=Eat_100 & [Catch1_27=Eat_27 & [Catch1_44=Eat_44 & [Catch1_68=Eat_68 & [Catch1_38=Eat_38 & [Catch1_92=Eat_92 & [Catch1_26=Eat_26 & [Catch1_56=Eat_56 & [Catch1_9=Eat_9 & [Catch1_54=Eat_54 & [Catch1_53=Eat_53 & [Catch1_58=Eat_58 & [Catch1_4=Eat_4 & [Catch1_65=Eat_65 & [Catch1_63=Eat_63 & [Catch1_99=Eat_99 & [Catch1_61=Eat_61 & [Catch1_90=Eat_90 & [Catch1_89=Eat_89 & [Catch1_31=Eat_31 & [Catch1_76=Eat_76 & [Catch1_8=Eat_8 & [Catch1_94=Eat_94 & [Catch1_28=Eat_28 & [Catch1_3=Eat_3 & [Catch1_5=Eat_5 & [Catch1_71=Eat_71 & [Catch1_70=Eat_70 & [Catch1_19=Eat_19 & [Catch1_86=Eat_86 & [Catch1_78=Eat_78 & [Catch1_22=Eat_22 & [Catch1_81=Eat_81 & [Catch1_73=Eat_73 & [Catch1_20=Eat_20 & [Catch1_35=Eat_35 & [Catch1_30=Eat_30 & [Catch1_96=Eat_96 & [Catch1_85=Eat_85 & [Catch1_12=Eat_12 & [Catch1_57=Eat_57 & [Catch1_50=Eat_50 & [Catch1_59=Eat_59 & [Catch1_32=Eat_32 & [Catch1_6=Eat_6 & [Catch1_45=Eat_45 & [Catch1_87=Eat_87 & [Catch1_51=Eat_51 & [Catch1_47=Eat_47 & [Catch1_98=Eat_98 & [Catch1_18=Eat_18 & [Catch1_62=Eat_62 & [Catch1_49=Eat_49 & [Catch1_36=Eat_36 & [Catch1_55=Eat_55 & [Catch1_29=Eat_29 & [Catch1_95=Eat_95 & [Catch1_97=Eat_97 & [Catch1_52=Eat_52 & [Catch1_72=Eat_72 & [Catch1_7=Eat_7 & [Catch1_11=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[true & [Catch1_82>Eat_82 & [Catch1_16>Eat_16 & [Catch1_39>Eat_39 & [Catch1_41>Eat_41 & [Catch1_93>Eat_93 & [Catch1_24>Eat_24 & [Catch1_64>Eat_64 & [Catch1_69>Eat_69 & [Catch1_40>Eat_40 & [Catch1_37>Eat_37 & [Catch1_43>Eat_43 & [Catch1_21>Eat_21 & [Catch1_84>Eat_84 & [Catch1_14>Eat_14 & [Catch1_34>Eat_34 & [Catch1_83>Eat_83 & [Catch1_25>Eat_25 & [Catch1_23>Eat_23 & [Catch1_10>Eat_10 & [Catch1_67>Eat_67 & [Catch1_17>Eat_17 & [Catch1_42>Eat_42 & [Catch1_77>Eat_77 & [Catch1_15>Eat_15 & [Catch1_75>Eat_75 & [Catch1_1>Eat_1 & [Catch1_2>Eat_2 & [Catch1_60>Eat_60 & [Catch1_88>Eat_88 & [Catch1_46>Eat_46 & [Catch1_33>Eat_33 & [Catch1_80>Eat_80 & [Catch1_74>Eat_74 & [Catch1_79>Eat_79 & [Catch1_91>Eat_91 & [Catch1_66>Eat_66 & [Catch1_13>Eat_13 & [Catch1_48>Eat_48 & [Catch1_100>Eat_100 & [Catch1_27>Eat_27 & [Catch1_44>Eat_44 & [Catch1_68>Eat_68 & [Catch1_38>Eat_38 & [Catch1_92>Eat_92 & [Catch1_26>Eat_26 & [Catch1_56>Eat_56 & [Catch1_9>Eat_9 & [Catch1_54>Eat_54 & [Catch1_53>Eat_53 & [Catch1_58>Eat_58 & [Catch1_4>Eat_4 & [Catch1_65>Eat_65 & [Catch1_63>Eat_63 & [Catch1_99>Eat_99 & [Catch1_61>Eat_61 & [Catch1_90>Eat_90 & [Catch1_89>Eat_89 & [Catch1_31>Eat_31 & [Catch1_76>Eat_76 & [Catch1_8>Eat_8 & [Catch1_94>Eat_94 & [Catch1_28>Eat_28 & [Catch1_3>Eat_3 & [Catch1_5>Eat_5 & [Catch1_71>Eat_71 & [Catch1_70>Eat_70 & [Catch1_19>Eat_19 & [Catch1_86>Eat_86 & [Catch1_78>Eat_78 & [Catch1_22>Eat_22 & [Catch1_81>Eat_81 & [Catch1_73>Eat_73 & [Catch1_20>Eat_20 & [Catch1_35>Eat_35 & [Catch1_30>Eat_30 & [Catch1_96>Eat_96 & [Catch1_85>Eat_85 & [Catch1_12>Eat_12 & [Catch1_57>Eat_57 & [Catch1_50>Eat_50 & [Catch1_59>Eat_59 & [Catch1_32>Eat_32 & [Catch1_6>Eat_6 & [Catch1_45>Eat_45 & [Catch1_87>Eat_87 & [Catch1_51>Eat_51 & [Catch1_47>Eat_47 & [Catch1_98>Eat_98 & [Catch1_18>Eat_18 & [Catch1_62>Eat_62 & [Catch1_49>Eat_49 & [Catch1_36>Eat_36 & [Catch1_55>Eat_55 & [Catch1_29>Eat_29 & [Catch1_95>Eat_95 & [Catch1_97>Eat_97 & [Catch1_52>Eat_52 & [Catch1_72>Eat_72 & [Catch1_7>Eat_7 & [Catch1_11>Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [false | [Catch1_82>Eat_82 | [Catch1_16>Eat_16 | [Catch1_39>Eat_39 | [Catch1_41>Eat_41 | [Catch1_93>Eat_93 | [Catch1_24>Eat_24 | [Catch1_64>Eat_64 | [Catch1_69>Eat_69 | [Catch1_40>Eat_40 | [Catch1_37>Eat_37 | [Catch1_43>Eat_43 | [Catch1_21>Eat_21 | [Catch1_84>Eat_84 | [Catch1_14>Eat_14 | [Catch1_34>Eat_34 | [Catch1_83>Eat_83 | [Catch1_25>Eat_25 | [Catch1_23>Eat_23 | [Catch1_10>Eat_10 | [Catch1_67>Eat_67 | [Catch1_17>Eat_17 | [Catch1_42>Eat_42 | [Catch1_77>Eat_77 | [Catch1_15>Eat_15 | [Catch1_75>Eat_75 | [Catch1_1>Eat_1 | [Catch1_2>Eat_2 | [Catch1_60>Eat_60 | [Catch1_88>Eat_88 | [Catch1_46>Eat_46 | [Catch1_33>Eat_33 | [Catch1_80>Eat_80 | [Catch1_74>Eat_74 | [Catch1_79>Eat_79 | [Catch1_91>Eat_91 | [Catch1_66>Eat_66 | [Catch1_13>Eat_13 | [Catch1_48>Eat_48 | [Catch1_100>Eat_100 | [Catch1_27>Eat_27 | [Catch1_44>Eat_44 | [Catch1_68>Eat_68 | [Catch1_38>Eat_38 | [Catch1_92>Eat_92 | [Catch1_26>Eat_26 | [Catch1_56>Eat_56 | [Catch1_9>Eat_9 | [Catch1_54>Eat_54 | [Catch1_53>Eat_53 | [Catch1_58>Eat_58 | [Catch1_4>Eat_4 | [Catch1_65>Eat_65 | [Catch1_63>Eat_63 | [Catch1_99>Eat_99 | [Catch1_61>Eat_61 | [Catch1_90>Eat_90 | [Catch1_89>Eat_89 | [Catch1_31>Eat_31 | [Catch1_76>Eat_76 | [Catch1_8>Eat_8 | [Catch1_94>Eat_94 | [Catch1_28>Eat_28 | [Catch1_3>Eat_3 | [Catch1_5>Eat_5 | [Catch1_71>Eat_71 | [Catch1_70>Eat_70 | [Catch1_19>Eat_19 | [Catch1_86>Eat_86 | [Catch1_78>Eat_78 | [Catch1_22>Eat_22 | [Catch1_81>Eat_81 | [Catch1_73>Eat_73 | [Catch1_20>Eat_20 | [Catch1_35>Eat_35 | [Catch1_30>Eat_30 | [Catch1_96>Eat_96 | [Catch1_85>Eat_85 | [Catch1_12>Eat_12 | [Catch1_57>Eat_57 | [Catch1_50>Eat_50 | [Catch1_59>Eat_59 | [Catch1_32>Eat_32 | [Catch1_6>Eat_6 | [Catch1_45>Eat_45 | [Catch1_87>Eat_87 | [Catch1_51>Eat_51 | [Catch1_47>Eat_47 | [Catch1_98>Eat_98 | [Catch1_18>Eat_18 | [Catch1_62>Eat_62 | [Catch1_49>Eat_49 | [Catch1_36>Eat_36 | [Catch1_55>Eat_55 | [Catch1_29>Eat_29 | [Catch1_95>Eat_95 | [Catch1_97>Eat_97 | [Catch1_52>Eat_52 | [Catch1_72>Eat_72 | [Catch1_7>Eat_7 | [Catch1_11>Eat_11 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_42_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[Catch1_37>Eat_37 & [[[[[[[[[[[[[[[[[Catch1_2>Eat_2 & [[[[Catch1_33>Eat_33 & [[[[[[[[[Catch1_27>Eat_27 & [[[[[[[[[Catch1_53>Eat_53 & [[[[[[[[Catch1_89>Eat_89 & [[[[Catch1_94>Eat_94 & [[[[Catch1_71>Eat_71 & [[[[[[[[Catch1_20>Eat_20 & [[[[[[[[[[[[[[[[[[[[[[[[Catch1_52>Eat_52 & [[[Catch1_11>Eat_11 & true] & Catch1_7>Eat_7] & Catch1_72>Eat_72]] & Catch1_97>Eat_97] & Catch1_95>Eat_95] & Catch1_29>Eat_29] & Catch1_55>Eat_55] & Catch1_36>Eat_36] & Catch1_49>Eat_49] & Catch1_62>Eat_62] & Catch1_18>Eat_18] & Catch1_98>Eat_98] & Catch1_47>Eat_47] & Catch1_51>Eat_51] & Catch1_87>Eat_87] & Catch1_45>Eat_45] & Catch1_6>Eat_6] & Catch1_32>Eat_32] & Catch1_59>Eat_59] & Catch1_50>Eat_50] & Catch1_57>Eat_57] & Catch1_12>Eat_12] & Catch1_85>Eat_85] & Catch1_96>Eat_96] & Catch1_30>Eat_30] & Catch1_35>Eat_35]] & Catch1_73>Eat_73] & Catch1_81>Eat_81] & Catch1_22>Eat_22] & Catch1_78>Eat_78] & Catch1_86>Eat_86] & Catch1_19>Eat_19] & Catch1_70>Eat_70]] & Catch1_5>Eat_5] & Catch1_3>Eat_3] & Catch1_28>Eat_28]] & Catch1_8>Eat_8] & Catch1_76>Eat_76] & Catch1_31>Eat_31]] & Catch1_90>Eat_90] & Catch1_61>Eat_61] & Catch1_99>Eat_99] & Catch1_63>Eat_63] & Catch1_65>Eat_65] & Catch1_4>Eat_4] & Catch1_58>Eat_58]] & Catch1_54>Eat_54] & Catch1_9>Eat_9] & Catch1_56>Eat_56] & Catch1_26>Eat_26] & Catch1_92>Eat_92] & Catch1_38>Eat_38] & Catch1_68>Eat_68] & Catch1_44>Eat_44]] & Catch1_100>Eat_100] & Catch1_48>Eat_48] & Catch1_13>Eat_13] & Catch1_66>Eat_66] & Catch1_91>Eat_91] & Catch1_79>Eat_79] & Catch1_74>Eat_74] & Catch1_80>Eat_80]] & Catch1_46>Eat_46] & Catch1_88>Eat_88] & Catch1_60>Eat_60]] & Catch1_1>Eat_1] & Catch1_75>Eat_75] & Catch1_15>Eat_15] & Catch1_77>Eat_77] & Catch1_42>Eat_42] & Catch1_17>Eat_17] & Catch1_67>Eat_67] & Catch1_10>Eat_10] & Catch1_23>Eat_23] & Catch1_25>Eat_25] & Catch1_83>Eat_83] & Catch1_34>Eat_34] & Catch1_14>Eat_14] & Catch1_84>Eat_84] & Catch1_21>Eat_21] & Catch1_43>Eat_43]] & Catch1_40>Eat_40] & Catch1_69>Eat_69] & Catch1_64>Eat_64] & Catch1_24>Eat_24] & Catch1_93>Eat_93] & Catch1_41>Eat_41] & Catch1_39>Eat_39] & Catch1_16>Eat_16] & Catch1_82>Eat_82] & true] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch1_11>Eat_11] | Catch1_7>Eat_7] | Catch1_72>Eat_72] | Catch1_52>Eat_52] | Catch1_97>Eat_97] | Catch1_95>Eat_95] | Catch1_29>Eat_29] | Catch1_55>Eat_55] | Catch1_36>Eat_36] | Catch1_49>Eat_49] | Catch1_62>Eat_62] | Catch1_18>Eat_18] | Catch1_98>Eat_98] | Catch1_47>Eat_47] | Catch1_51>Eat_51] | Catch1_87>Eat_87] | Catch1_45>Eat_45] | Catch1_6>Eat_6] | Catch1_32>Eat_32] | Catch1_59>Eat_59] | Catch1_50>Eat_50] | Catch1_57>Eat_57] | Catch1_12>Eat_12] | Catch1_85>Eat_85] | Catch1_96>Eat_96] | Catch1_30>Eat_30] | Catch1_35>Eat_35] | Catch1_20>Eat_20] | Catch1_73>Eat_73] | Catch1_81>Eat_81] | Catch1_22>Eat_22] | Catch1_78>Eat_78] | Catch1_86>Eat_86] | Catch1_19>Eat_19] | Catch1_70>Eat_70] | Catch1_71>Eat_71] | Catch1_5>Eat_5] | Catch1_3>Eat_3] | Catch1_28>Eat_28] | Catch1_94>Eat_94] | Catch1_8>Eat_8] | Catch1_76>Eat_76] | Catch1_31>Eat_31] | Catch1_89>Eat_89] | Catch1_90>Eat_90] | Catch1_61>Eat_61] | Catch1_99>Eat_99] | Catch1_63>Eat_63] | Catch1_65>Eat_65] | Catch1_4>Eat_4] | Catch1_58>Eat_58] | Catch1_53>Eat_53] | Catch1_54>Eat_54] | Catch1_9>Eat_9] | Catch1_56>Eat_56] | Catch1_26>Eat_26] | Catch1_92>Eat_92] | Catch1_38>Eat_38] | Catch1_68>Eat_68] | Catch1_44>Eat_44] | Catch1_27>Eat_27] | Catch1_100>Eat_100] | Catch1_48>Eat_48] | Catch1_13>Eat_13] | Catch1_66>Eat_66] | Catch1_91>Eat_91] | Catch1_79>Eat_79] | Catch1_74>Eat_74] | Catch1_80>Eat_80] | Catch1_33>Eat_33] | Catch1_46>Eat_46] | Catch1_88>Eat_88] | Catch1_60>Eat_60] | Catch1_2>Eat_2] | Catch1_1>Eat_1] | Catch1_75>Eat_75] | Catch1_15>Eat_15] | Catch1_77>Eat_77] | Catch1_42>Eat_42] | Catch1_17>Eat_17] | Catch1_67>Eat_67] | Catch1_10>Eat_10] | Catch1_23>Eat_23] | Catch1_25>Eat_25] | Catch1_83>Eat_83] | Catch1_34>Eat_34] | Catch1_14>Eat_14] | Catch1_84>Eat_84] | Catch1_21>Eat_21] | Catch1_43>Eat_43] | Catch1_37>Eat_37] | Catch1_40>Eat_40] | Catch1_69>Eat_69] | Catch1_64>Eat_64] | Catch1_24>Eat_24] | Catch1_93>Eat_93] | Catch1_41>Eat_41] | Catch1_39>Eat_39] | Catch1_16>Eat_16] | Catch1_82>Eat_82] | false]] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11=Eat_11] & Catch1_7=Eat_7] & Catch1_72=Eat_72] & Catch1_52=Eat_52] & Catch1_97=Eat_97] & Catch1_95=Eat_95] & Catch1_29=Eat_29] & Catch1_55=Eat_55] & Catch1_36=Eat_36] & Catch1_49=Eat_49] & Catch1_62=Eat_62] & Catch1_18=Eat_18] & Catch1_98=Eat_98] & Catch1_47=Eat_47] & Catch1_51=Eat_51] & Catch1_87=Eat_87] & Catch1_45=Eat_45] & Catch1_6=Eat_6] & Catch1_32=Eat_32] & Catch1_59=Eat_59] & Catch1_50=Eat_50] & Catch1_57=Eat_57] & Catch1_12=Eat_12] & Catch1_85=Eat_85] & Catch1_96=Eat_96] & Catch1_30=Eat_30] & Catch1_35=Eat_35] & Catch1_20=Eat_20] & Catch1_73=Eat_73] & Catch1_81=Eat_81] & Catch1_22=Eat_22] & Catch1_78=Eat_78] & Catch1_86=Eat_86] & Catch1_19=Eat_19] & Catch1_70=Eat_70] & Catch1_71=Eat_71] & Catch1_5=Eat_5] & Catch1_3=Eat_3] & Catch1_28=Eat_28] & Catch1_94=Eat_94] & Catch1_8=Eat_8] & Catch1_76=Eat_76] & Catch1_31=Eat_31] & Catch1_89=Eat_89] & Catch1_90=Eat_90] & Catch1_61=Eat_61] & Catch1_99=Eat_99] & Catch1_63=Eat_63] & Catch1_65=Eat_65] & Catch1_4=Eat_4] & Catch1_58=Eat_58] & Catch1_53=Eat_53] & Catch1_54=Eat_54] & Catch1_9=Eat_9] & Catch1_56=Eat_56] & Catch1_26=Eat_26] & Catch1_92=Eat_92] & Catch1_38=Eat_38] & Catch1_68=Eat_68] & Catch1_44=Eat_44] & Catch1_27=Eat_27] & Catch1_100=Eat_100] & Catch1_48=Eat_48] & Catch1_13=Eat_13] & Catch1_66=Eat_66] & Catch1_91=Eat_91] & Catch1_79=Eat_79] & Catch1_74=Eat_74] & Catch1_80=Eat_80] & Catch1_33=Eat_33] & Catch1_46=Eat_46] & Catch1_88=Eat_88] & Catch1_60=Eat_60] & Catch1_2=Eat_2] & Catch1_1=Eat_1] & Catch1_75=Eat_75] & Catch1_15=Eat_15] & Catch1_77=Eat_77] & Catch1_42=Eat_42] & Catch1_17=Eat_17] & Catch1_67=Eat_67] & Catch1_10=Eat_10] & Catch1_23=Eat_23] & Catch1_25=Eat_25] & Catch1_83=Eat_83] & Catch1_34=Eat_34] & Catch1_14=Eat_14] & Catch1_84=Eat_84] & Catch1_21=Eat_21] & Catch1_43=Eat_43] & Catch1_37=Eat_37] & Catch1_40=Eat_40] & Catch1_69=Eat_69] & Catch1_64=Eat_64] & Catch1_24=Eat_24] & Catch1_93=Eat_93] & Catch1_41=Eat_41] & Catch1_39=Eat_39] & Catch1_16=Eat_16] & Catch1_82=Eat_82]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11=Eat_11] & Catch1_7=Eat_7] & Catch1_72=Eat_72] & Catch1_52=Eat_52] & Catch1_97=Eat_97] & Catch1_95=Eat_95] & Catch1_29=Eat_29] & Catch1_55=Eat_55] & Catch1_36=Eat_36] & Catch1_49=Eat_49] & Catch1_62=Eat_62] & Catch1_18=Eat_18] & Catch1_98=Eat_98] & Catch1_47=Eat_47] & Catch1_51=Eat_51] & Catch1_87=Eat_87] & Catch1_45=Eat_45] & Catch1_6=Eat_6] & Catch1_32=Eat_32] & Catch1_59=Eat_59] & Catch1_50=Eat_50] & Catch1_57=Eat_57] & Catch1_12=Eat_12] & Catch1_85=Eat_85] & Catch1_96=Eat_96] & Catch1_30=Eat_30] & Catch1_35=Eat_35] & Catch1_20=Eat_20] & Catch1_73=Eat_73] & Catch1_81=Eat_81] & Catch1_22=Eat_22] & Catch1_78=Eat_78] & Catch1_86=Eat_86] & Catch1_19=Eat_19] & Catch1_70=Eat_70] & Catch1_71=Eat_71] & Catch1_5=Eat_5] & Catch1_3=Eat_3] & Catch1_28=Eat_28] & Catch1_94=Eat_94] & Catch1_8=Eat_8] & Catch1_76=Eat_76] & Catch1_31=Eat_31] & Catch1_89=Eat_89] & Catch1_90=Eat_90] & Catch1_61=Eat_61] & Catch1_99=Eat_99] & Catch1_63=Eat_63] & Catch1_65=Eat_65] & Catch1_4=Eat_4] & Catch1_58=Eat_58] & Catch1_53=Eat_53] & Catch1_54=Eat_54] & Catch1_9=Eat_9] & Catch1_56=Eat_56] & Catch1_26=Eat_26] & Catch1_92=Eat_92] & Catch1_38=Eat_38] & Catch1_68=Eat_68] & Catch1_44=Eat_44] & Catch1_27=Eat_27] & Catch1_100=Eat_100] & Catch1_48=Eat_48] & Catch1_13=Eat_13] & Catch1_66=Eat_66] & Catch1_91=Eat_91] & Catch1_79=Eat_79] & Catch1_74=Eat_74] & Catch1_80=Eat_80] & Catch1_33=Eat_33] & Catch1_46=Eat_46] & Catch1_88=Eat_88] & Catch1_60=Eat_60] & Catch1_2=Eat_2] & Catch1_1=Eat_1] & Catch1_75=Eat_75] & Catch1_15=Eat_15] & Catch1_77=Eat_77] & Catch1_42=Eat_42] & Catch1_17=Eat_17] & Catch1_67=Eat_67] & Catch1_10=Eat_10] & Catch1_23=Eat_23] & Catch1_25=Eat_25] & Catch1_83=Eat_83] & Catch1_34=Eat_34] & Catch1_14=Eat_14] & Catch1_84=Eat_84] & Catch1_21=Eat_21] & Catch1_43=Eat_43] & Catch1_37=Eat_37] & Catch1_40=Eat_40] & Catch1_69=Eat_69] & Catch1_64=Eat_64] & Catch1_24=Eat_24] & Catch1_93=Eat_93] & Catch1_41=Eat_41] & Catch1_39=Eat_39] & Catch1_16=Eat_16] & Catch1_82=Eat_82] | [[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch1_66>Eat_66 | [Catch1_13>Eat_13 | [Catch1_48>Eat_48 | [Catch1_100>Eat_100 | [Catch1_27>Eat_27 | [Catch1_44>Eat_44 | [Catch1_68>Eat_68 | [Catch1_38>Eat_38 | [Catch1_92>Eat_92 | [Catch1_26>Eat_26 | [Catch1_56>Eat_56 | [Catch1_9>Eat_9 | [Catch1_54>Eat_54 | [Catch1_53>Eat_53 | [Catch1_58>Eat_58 | [Catch1_4>Eat_4 | [Catch1_65>Eat_65 | [Catch1_63>Eat_63 | [Catch1_99>Eat_99 | [Catch1_61>Eat_61 | [Catch1_90>Eat_90 | [Catch1_89>Eat_89 | [Catch1_31>Eat_31 | [Catch1_76>Eat_76 | [Catch1_8>Eat_8 | [Catch1_94>Eat_94 | [Catch1_28>Eat_28 | [Catch1_3>Eat_3 | [Catch1_5>Eat_5 | [Catch1_71>Eat_71 | [Catch1_70>Eat_70 | [Catch1_19>Eat_19 | [Catch1_86>Eat_86 | [Catch1_78>Eat_78 | [Catch1_22>Eat_22 | [Catch1_81>Eat_81 | [Catch1_73>Eat_73 | [Catch1_20>Eat_20 | [Catch1_35>Eat_35 | [Catch1_30>Eat_30 | [Catch1_96>Eat_96 | [Catch1_85>Eat_85 | [Catch1_12>Eat_12 | [Catch1_57>Eat_57 | [Catch1_50>Eat_50 | [Catch1_59>Eat_59 | [Catch1_32>Eat_32 | [Catch1_6>Eat_6 | [Catch1_45>Eat_45 | [Catch1_87>Eat_87 | [Catch1_51>Eat_51 | [Catch1_47>Eat_47 | [Catch1_98>Eat_98 | [Catch1_18>Eat_18 | [Catch1_62>Eat_62 | [Catch1_49>Eat_49 | [Catch1_36>Eat_36 | [Catch1_55>Eat_55 | [Catch1_29>Eat_29 | [Catch1_95>Eat_95 | [Catch1_97>Eat_97 | [Catch1_52>Eat_52 | [Catch1_72>Eat_72 | [Catch1_7>Eat_7 | [Catch1_11>Eat_11 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | Catch1_91>Eat_91] | Catch1_79>Eat_79] | Catch1_74>Eat_74] | Catch1_80>Eat_80] | Catch1_33>Eat_33] | Catch1_46>Eat_46] | Catch1_88>Eat_88] | Catch1_60>Eat_60] | Catch1_2>Eat_2] | Catch1_1>Eat_1] | Catch1_75>Eat_75] | Catch1_15>Eat_15] | Catch1_77>Eat_77] | Catch1_42>Eat_42] | Catch1_17>Eat_17] | Catch1_67>Eat_67] | Catch1_10>Eat_10] | Catch1_23>Eat_23] | Catch1_25>Eat_25] | Catch1_83>Eat_83] | Catch1_34>Eat_34] | Catch1_14>Eat_14] | Catch1_84>Eat_84] | Catch1_21>Eat_21] | Catch1_43>Eat_43] | Catch1_37>Eat_37] | Catch1_40>Eat_40] | Catch1_69>Eat_69] | Catch1_64>Eat_64] | Catch1_24>Eat_24] | Catch1_93>Eat_93] | Catch1_41>Eat_41] | Catch1_39>Eat_39] | Catch1_16>Eat_16] | Catch1_82>Eat_82]] & [true & [Catch1_82>Eat_82 & [Catch1_16>Eat_16 & [Catch1_39>Eat_39 & [Catch1_41>Eat_41 & [Catch1_93>Eat_93 & [Catch1_24>Eat_24 & [Catch1_64>Eat_64 & [Catch1_69>Eat_69 & [Catch1_40>Eat_40 & [Catch1_37>Eat_37 & [Catch1_43>Eat_43 & [Catch1_21>Eat_21 & [Catch1_84>Eat_84 & [Catch1_14>Eat_14 & [Catch1_34>Eat_34 & [Catch1_83>Eat_83 & [Catch1_25>Eat_25 & [Catch1_23>Eat_23 & [Catch1_10>Eat_10 & [Catch1_67>Eat_67 & [Catch1_17>Eat_17 & [Catch1_42>Eat_42 & [Catch1_77>Eat_77 & [Catch1_15>Eat_15 & [Catch1_75>Eat_75 & [Catch1_1>Eat_1 & [Catch1_2>Eat_2 & [Catch1_60>Eat_60 & [Catch1_88>Eat_88 & [Catch1_46>Eat_46 & [Catch1_33>Eat_33 & [Catch1_80>Eat_80 & [Catch1_74>Eat_74 & [Catch1_79>Eat_79 & [Catch1_91>Eat_91 & [Catch1_66>Eat_66 & [Catch1_13>Eat_13 & [Catch1_48>Eat_48 & [Catch1_100>Eat_100 & [Catch1_27>Eat_27 & [Catch1_44>Eat_44 & [Catch1_68>Eat_68 & [Catch1_38>Eat_38 & [Catch1_92>Eat_92 & [Catch1_26>Eat_26 & [Catch1_56>Eat_56 & [Catch1_9>Eat_9 & [Catch1_54>Eat_54 & [Catch1_53>Eat_53 & [Catch1_58>Eat_58 & [Catch1_4>Eat_4 & [Catch1_65>Eat_65 & [Catch1_63>Eat_63 & [Catch1_99>Eat_99 & [Catch1_61>Eat_61 & [Catch1_90>Eat_90 & [Catch1_89>Eat_89 & [Catch1_31>Eat_31 & [Catch1_76>Eat_76 & [Catch1_8>Eat_8 & [Catch1_94>Eat_94 & [Catch1_28>Eat_28 & [Catch1_3>Eat_3 & [Catch1_5>Eat_5 & [Catch1_71>Eat_71 & [Catch1_70>Eat_70 & [Catch1_19>Eat_19 & [Catch1_86>Eat_86 & [Catch1_78>Eat_78 & [Catch1_22>Eat_22 & [Catch1_81>Eat_81 & [Catch1_73>Eat_73 & [Catch1_20>Eat_20 & [Catch1_35>Eat_35 & [Catch1_30>Eat_30 & [Catch1_96>Eat_96 & [Catch1_85>Eat_85 & [Catch1_12>Eat_12 & [Catch1_57>Eat_57 & [Catch1_50>Eat_50 & [Catch1_59>Eat_59 & [Catch1_32>Eat_32 & [Catch1_6>Eat_6 & [Catch1_45>Eat_45 & [Catch1_87>Eat_87 & [Catch1_51>Eat_51 & [Catch1_47>Eat_47 & [Catch1_98>Eat_98 & [Catch1_18>Eat_18 & [Catch1_62>Eat_62 & [Catch1_49>Eat_49 & [Catch1_36>Eat_36 & [Catch1_55>Eat_55 & [Catch1_29>Eat_29 & [Catch1_95>Eat_95 & [Catch1_97>Eat_97 & [Catch1_52>Eat_52 & [Catch1_72>Eat_72 & [Catch1_7>Eat_7 & [Catch1_11>Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_43_mix_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[Catch1_40=Eat_40 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11=Eat_11] & Catch1_7=Eat_7] & Catch1_72=Eat_72] & Catch1_52=Eat_52] & Catch1_97=Eat_97] & Catch1_95=Eat_95] & Catch1_29=Eat_29] & Catch1_55=Eat_55] & Catch1_36=Eat_36] & Catch1_49=Eat_49] & Catch1_62=Eat_62] & Catch1_18=Eat_18] & Catch1_98=Eat_98] & Catch1_47=Eat_47] & Catch1_51=Eat_51] & Catch1_87=Eat_87] & Catch1_45=Eat_45] & Catch1_6=Eat_6] & Catch1_32=Eat_32] & Catch1_59=Eat_59] & Catch1_50=Eat_50] & Catch1_57=Eat_57] & Catch1_12=Eat_12] & Catch1_85=Eat_85] & Catch1_96=Eat_96] & Catch1_30=Eat_30] & Catch1_35=Eat_35] & Catch1_20=Eat_20] & Catch1_73=Eat_73] & Catch1_81=Eat_81] & Catch1_22=Eat_22] & Catch1_78=Eat_78] & Catch1_86=Eat_86] & Catch1_19=Eat_19] & Catch1_70=Eat_70] & Catch1_71=Eat_71] & Catch1_5=Eat_5] & Catch1_3=Eat_3] & Catch1_28=Eat_28] & Catch1_94=Eat_94] & Catch1_8=Eat_8] & Catch1_76=Eat_76] & Catch1_31=Eat_31] & Catch1_89=Eat_89] & Catch1_90=Eat_90] & Catch1_61=Eat_61] & Catch1_99=Eat_99] & Catch1_63=Eat_63] & Catch1_65=Eat_65] & Catch1_4=Eat_4] & Catch1_58=Eat_58] & Catch1_53=Eat_53] & Catch1_54=Eat_54] & Catch1_9=Eat_9] & Catch1_56=Eat_56] & Catch1_26=Eat_26] & Catch1_92=Eat_92] & Catch1_38=Eat_38] & Catch1_68=Eat_68] & Catch1_44=Eat_44] & Catch1_27=Eat_27] & Catch1_100=Eat_100] & Catch1_48=Eat_48] & Catch1_13=Eat_13] & Catch1_66=Eat_66] & Catch1_91=Eat_91] & Catch1_79=Eat_79] & Catch1_74=Eat_74] & Catch1_80=Eat_80] & Catch1_33=Eat_33] & Catch1_46=Eat_46] & Catch1_88=Eat_88] & Catch1_60=Eat_60] & Catch1_2=Eat_2] & Catch1_1=Eat_1] & Catch1_75=Eat_75] & Catch1_15=Eat_15] & Catch1_77=Eat_77] & Catch1_42=Eat_42] & Catch1_17=Eat_17] & Catch1_67=Eat_67] & Catch1_10=Eat_10] & Catch1_23=Eat_23] & Catch1_25=Eat_25] & Catch1_83=Eat_83] & Catch1_34=Eat_34] & Catch1_14=Eat_14] & Catch1_84=Eat_84] & Catch1_21=Eat_21] & Catch1_43=Eat_43] & Catch1_37=Eat_37]] & Catch1_69=Eat_69] & Catch1_64=Eat_64] & Catch1_24=Eat_24] & Catch1_93=Eat_93] & Catch1_41=Eat_41] & Catch1_39=Eat_39] & Catch1_16=Eat_16] & Catch1_82=Eat_82] & [[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11>Eat_11] & Catch1_7>Eat_7] & Catch1_72>Eat_72] & Catch1_52>Eat_52] & Catch1_97>Eat_97] & Catch1_95>Eat_95] & Catch1_29>Eat_29] & Catch1_55>Eat_55] & Catch1_36>Eat_36] & Catch1_49>Eat_49] & Catch1_62>Eat_62] & Catch1_18>Eat_18] & Catch1_98>Eat_98] & Catch1_47>Eat_47] & Catch1_51>Eat_51] & Catch1_87>Eat_87] & Catch1_45>Eat_45] & Catch1_6>Eat_6] & Catch1_32>Eat_32] & Catch1_59>Eat_59] & Catch1_50>Eat_50] & Catch1_57>Eat_57] & Catch1_12>Eat_12] & Catch1_85>Eat_85] & Catch1_96>Eat_96] & Catch1_30>Eat_30] & Catch1_35>Eat_35] & Catch1_20>Eat_20] & Catch1_73>Eat_73] & Catch1_81>Eat_81] & Catch1_22>Eat_22] & Catch1_78>Eat_78] & Catch1_86>Eat_86] & Catch1_19>Eat_19] & Catch1_70>Eat_70] & Catch1_71>Eat_71] & Catch1_5>Eat_5] & Catch1_3>Eat_3] & Catch1_28>Eat_28] & Catch1_94>Eat_94] & Catch1_8>Eat_8] & Catch1_76>Eat_76] & Catch1_31>Eat_31] & Catch1_89>Eat_89] & Catch1_90>Eat_90] & Catch1_61>Eat_61] & Catch1_99>Eat_99] & Catch1_63>Eat_63] & Catch1_65>Eat_65] & Catch1_4>Eat_4] & Catch1_58>Eat_58] & Catch1_53>Eat_53] & Catch1_54>Eat_54] & Catch1_9>Eat_9] & Catch1_56>Eat_56] & Catch1_26>Eat_26] & Catch1_92>Eat_92] & Catch1_38>Eat_38] & Catch1_68>Eat_68] & Catch1_44>Eat_44] & Catch1_27>Eat_27] & Catch1_100>Eat_100] & Catch1_48>Eat_48] & Catch1_13>Eat_13] & Catch1_66>Eat_66] & Catch1_91>Eat_91] & Catch1_79>Eat_79] & Catch1_74>Eat_74] & Catch1_80>Eat_80] & Catch1_33>Eat_33] & Catch1_46>Eat_46] & Catch1_88>Eat_88] & Catch1_60>Eat_60] & Catch1_2>Eat_2] & Catch1_1>Eat_1] & Catch1_75>Eat_75] & Catch1_15>Eat_15] & Catch1_77>Eat_77] & Catch1_42>Eat_42] & Catch1_17>Eat_17] & Catch1_67>Eat_67] & Catch1_10>Eat_10] & Catch1_23>Eat_23] & Catch1_25>Eat_25] & Catch1_83>Eat_83] & Catch1_34>Eat_34] & Catch1_14>Eat_14] & Catch1_84>Eat_84] & Catch1_21>Eat_21] & Catch1_43>Eat_43] & Catch1_37>Eat_37] & Catch1_40>Eat_40] & Catch1_69>Eat_69] & Catch1_64>Eat_64] & Catch1_24>Eat_24] & Catch1_93>Eat_93] & Catch1_41>Eat_41] & Catch1_39>Eat_39] & Catch1_16>Eat_16] & Catch1_82>Eat_82]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch1_11>Eat_11] | Catch1_7>Eat_7] | Catch1_72>Eat_72] | Catch1_52>Eat_52] | Catch1_97>Eat_97] | Catch1_95>Eat_95] | Catch1_29>Eat_29] | Catch1_55>Eat_55] | Catch1_36>Eat_36] | Catch1_49>Eat_49] | Catch1_62>Eat_62] | Catch1_18>Eat_18] | Catch1_98>Eat_98] | Catch1_47>Eat_47] | Catch1_51>Eat_51] | Catch1_87>Eat_87] | Catch1_45>Eat_45] | Catch1_6>Eat_6] | Catch1_32>Eat_32] | Catch1_59>Eat_59] | Catch1_50>Eat_50] | Catch1_57>Eat_57] | Catch1_12>Eat_12] | Catch1_85>Eat_85] | Catch1_96>Eat_96] | Catch1_30>Eat_30] | Catch1_35>Eat_35] | Catch1_20>Eat_20] | Catch1_73>Eat_73] | Catch1_81>Eat_81] | Catch1_22>Eat_22] | Catch1_78>Eat_78] | Catch1_86>Eat_86] | Catch1_19>Eat_19] | Catch1_70>Eat_70] | Catch1_71>Eat_71] | Catch1_5>Eat_5] | Catch1_3>Eat_3] | Catch1_28>Eat_28] | Catch1_94>Eat_94] | Catch1_8>Eat_8] | Catch1_76>Eat_76] | Catch1_31>Eat_31] | Catch1_89>Eat_89] | Catch1_90>Eat_90] | Catch1_61>Eat_61] | Catch1_99>Eat_99] | Catch1_63>Eat_63] | Catch1_65>Eat_65] | Catch1_4>Eat_4] | Catch1_58>Eat_58] | Catch1_53>Eat_53] | Catch1_54>Eat_54] | Catch1_9>Eat_9] | Catch1_56>Eat_56] | Catch1_26>Eat_26] | Catch1_92>Eat_92] | Catch1_38>Eat_38] | Catch1_68>Eat_68] | Catch1_44>Eat_44] | Catch1_27>Eat_27] | Catch1_100>Eat_100] | Catch1_48>Eat_48] | Catch1_13>Eat_13] | Catch1_66>Eat_66] | Catch1_91>Eat_91] | Catch1_79>Eat_79] | Catch1_74>Eat_74] | Catch1_80>Eat_80] | Catch1_33>Eat_33] | Catch1_46>Eat_46] | Catch1_88>Eat_88] | Catch1_60>Eat_60] | Catch1_2>Eat_2] | Catch1_1>Eat_1] | Catch1_75>Eat_75] | Catch1_15>Eat_15] | Catch1_77>Eat_77] | Catch1_42>Eat_42] | Catch1_17>Eat_17] | Catch1_67>Eat_67] | Catch1_10>Eat_10] | Catch1_23>Eat_23] | Catch1_25>Eat_25] | Catch1_83>Eat_83] | Catch1_34>Eat_34] | Catch1_14>Eat_14] | Catch1_84>Eat_84] | Catch1_21>Eat_21] | Catch1_43>Eat_43] | Catch1_37>Eat_37] | Catch1_40>Eat_40] | Catch1_69>Eat_69] | Catch1_64>Eat_64] | Catch1_24>Eat_24] | Catch1_93>Eat_93] | Catch1_41>Eat_41] | Catch1_39>Eat_39] | Catch1_16>Eat_16] | Catch1_82>Eat_82] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch1_11>Eat_11] | Catch1_7>Eat_7] | Catch1_72>Eat_72] | Catch1_52>Eat_52] | Catch1_97>Eat_97] | Catch1_95>Eat_95] | Catch1_29>Eat_29] | Catch1_55>Eat_55] | Catch1_36>Eat_36] | Catch1_49>Eat_49] | Catch1_62>Eat_62] | Catch1_18>Eat_18] | Catch1_98>Eat_98] | Catch1_47>Eat_47] | Catch1_51>Eat_51] | Catch1_87>Eat_87] | Catch1_45>Eat_45] | Catch1_6>Eat_6] | Catch1_32>Eat_32] | Catch1_59>Eat_59] | Catch1_50>Eat_50] | Catch1_57>Eat_57] | Catch1_12>Eat_12] | Catch1_85>Eat_85] | Catch1_96>Eat_96] | Catch1_30>Eat_30] | Catch1_35>Eat_35] | Catch1_20>Eat_20] | Catch1_73>Eat_73] | Catch1_81>Eat_81] | Catch1_22>Eat_22] | Catch1_78>Eat_78] | Catch1_86>Eat_86] | Catch1_19>Eat_19] | Catch1_70>Eat_70] | Catch1_71>Eat_71] | Catch1_5>Eat_5] | Catch1_3>Eat_3] | Catch1_28>Eat_28] | Catch1_94>Eat_94] | Catch1_8>Eat_8] | Catch1_76>Eat_76] | Catch1_31>Eat_31] | Catch1_89>Eat_89] | Catch1_90>Eat_90] | Catch1_61>Eat_61] | Catch1_99>Eat_99] | Catch1_63>Eat_63] | Catch1_65>Eat_65] | Catch1_4>Eat_4] | Catch1_58>Eat_58] | Catch1_53>Eat_53] | Catch1_54>Eat_54] | Catch1_9>Eat_9] | Catch1_56>Eat_56] | Catch1_26>Eat_26] | Catch1_92>Eat_92] | Catch1_38>Eat_38] | Catch1_68>Eat_68] | Catch1_44>Eat_44] | Catch1_27>Eat_27] | Catch1_100>Eat_100] | Catch1_48>Eat_48] | Catch1_13>Eat_13] | Catch1_66>Eat_66] | Catch1_91>Eat_91] | Catch1_79>Eat_79] | Catch1_74>Eat_74] | Catch1_80>Eat_80] | Catch1_33>Eat_33] | Catch1_46>Eat_46] | Catch1_88>Eat_88] | Catch1_60>Eat_60] | Catch1_2>Eat_2] | Catch1_1>Eat_1] | Catch1_75>Eat_75] | Catch1_15>Eat_15] | Catch1_77>Eat_77] | Catch1_42>Eat_42] | Catch1_17>Eat_17] | Catch1_67>Eat_67] | Catch1_10>Eat_10] | Catch1_23>Eat_23] | Catch1_25>Eat_25] | Catch1_83>Eat_83] | Catch1_34>Eat_34] | Catch1_14>Eat_14] | Catch1_84>Eat_84] | Catch1_21>Eat_21] | Catch1_43>Eat_43] | Catch1_37>Eat_37] | Catch1_40>Eat_40] | Catch1_69>Eat_69] | Catch1_64>Eat_64] | Catch1_24>Eat_24] | Catch1_93>Eat_93] | Catch1_41>Eat_41] | Catch1_39>Eat_39] | Catch1_16>Eat_16] | Catch1_82>Eat_82]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11>Eat_11] & Catch1_7>Eat_7] & Catch1_72>Eat_72] & Catch1_52>Eat_52] & Catch1_97>Eat_97] & Catch1_95>Eat_95] & Catch1_29>Eat_29] & Catch1_55>Eat_55] & Catch1_36>Eat_36] & Catch1_49>Eat_49] & Catch1_62>Eat_62] & Catch1_18>Eat_18] & Catch1_98>Eat_98] & Catch1_47>Eat_47] & Catch1_51>Eat_51] & Catch1_87>Eat_87] & Catch1_45>Eat_45] & Catch1_6>Eat_6] & Catch1_32>Eat_32] & Catch1_59>Eat_59] & Catch1_50>Eat_50] & Catch1_57>Eat_57] & Catch1_12>Eat_12] & Catch1_85>Eat_85] & Catch1_96>Eat_96] & Catch1_30>Eat_30] & Catch1_35>Eat_35] & Catch1_20>Eat_20] & Catch1_73>Eat_73] & Catch1_81>Eat_81] & Catch1_22>Eat_22] & Catch1_78>Eat_78] & Catch1_86>Eat_86] & Catch1_19>Eat_19] & Catch1_70>Eat_70] & Catch1_71>Eat_71] & Catch1_5>Eat_5] & Catch1_3>Eat_3] & Catch1_28>Eat_28] & Catch1_94>Eat_94] & Catch1_8>Eat_8] & Catch1_76>Eat_76] & Catch1_31>Eat_31] & Catch1_89>Eat_89] & Catch1_90>Eat_90] & Catch1_61>Eat_61] & Catch1_99>Eat_99] & Catch1_63>Eat_63] & Catch1_65>Eat_65] & Catch1_4>Eat_4] & Catch1_58>Eat_58] & Catch1_53>Eat_53] & Catch1_54>Eat_54] & Catch1_9>Eat_9] & Catch1_56>Eat_56] & Catch1_26>Eat_26] & Catch1_92>Eat_92] & Catch1_38>Eat_38] & Catch1_68>Eat_68] & Catch1_44>Eat_44] & Catch1_27>Eat_27] & Catch1_100>Eat_100] & Catch1_48>Eat_48] & Catch1_13>Eat_13] & Catch1_66>Eat_66] & Catch1_91>Eat_91] & Catch1_79>Eat_79] & Catch1_74>Eat_74] & Catch1_80>Eat_80] & Catch1_33>Eat_33] & Catch1_46>Eat_46] & Catch1_88>Eat_88] & Catch1_60>Eat_60] & Catch1_2>Eat_2] & Catch1_1>Eat_1] & Catch1_75>Eat_75] & Catch1_15>Eat_15] & Catch1_77>Eat_77] & Catch1_42>Eat_42] & Catch1_17>Eat_17] & Catch1_67>Eat_67] & Catch1_10>Eat_10] & Catch1_23>Eat_23] & Catch1_25>Eat_25] & Catch1_83>Eat_83] & Catch1_34>Eat_34] & Catch1_14>Eat_14] & Catch1_84>Eat_84] & Catch1_21>Eat_21] & Catch1_43>Eat_43] & Catch1_37>Eat_37] & Catch1_40>Eat_40] & Catch1_69>Eat_69] & Catch1_64>Eat_64] & Catch1_24>Eat_24] & Catch1_93>Eat_93] & Catch1_41>Eat_41] & Catch1_39>Eat_39] & Catch1_16>Eat_16] & Catch1_82>Eat_82] & true]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_11=Eat_11] & Catch1_7=Eat_7] & Catch1_72=Eat_72] & Catch1_52=Eat_52] & Catch1_97=Eat_97] & Catch1_95=Eat_95] & Catch1_29=Eat_29] & Catch1_55=Eat_55] & Catch1_36=Eat_36] & Catch1_49=Eat_49] & Catch1_62=Eat_62] & Catch1_18=Eat_18] & Catch1_98=Eat_98] & Catch1_47=Eat_47] & Catch1_51=Eat_51] & Catch1_87=Eat_87] & Catch1_45=Eat_45] & Catch1_6=Eat_6] & Catch1_32=Eat_32] & Catch1_59=Eat_59] & Catch1_50=Eat_50] & Catch1_57=Eat_57] & Catch1_12=Eat_12] & Catch1_85=Eat_85] & Catch1_96=Eat_96] & Catch1_30=Eat_30] & Catch1_35=Eat_35] & Catch1_20=Eat_20] & Catch1_73=Eat_73] & Catch1_81=Eat_81] & Catch1_22=Eat_22] & Catch1_78=Eat_78] & Catch1_86=Eat_86] & Catch1_19=Eat_19] & Catch1_70=Eat_70] & Catch1_71=Eat_71] & Catch1_5=Eat_5] & Catch1_3=Eat_3] & Catch1_28=Eat_28] & Catch1_94=Eat_94] & Catch1_8=Eat_8] & Catch1_76=Eat_76] & Catch1_31=Eat_31] & Catch1_89=Eat_89] & Catch1_90=Eat_90] & Catch1_61=Eat_61] & Catch1_99=Eat_99] & Catch1_63=Eat_63] & Catch1_65=Eat_65] & Catch1_4=Eat_4] & Catch1_58=Eat_58] & Catch1_53=Eat_53] & Catch1_54=Eat_54] & Catch1_9=Eat_9] & Catch1_56=Eat_56] & Catch1_26=Eat_26] & Catch1_92=Eat_92] & Catch1_38=Eat_38] & Catch1_68=Eat_68] & Catch1_44=Eat_44] & Catch1_27=Eat_27] & Catch1_100=Eat_100] & Catch1_48=Eat_48] & Catch1_13=Eat_13] & Catch1_66=Eat_66] & Catch1_91=Eat_91] & Catch1_79=Eat_79] & Catch1_74=Eat_74] & Catch1_80=Eat_80] & Catch1_33=Eat_33] & Catch1_46=Eat_46] & Catch1_88=Eat_88] & Catch1_60=Eat_60] & Catch1_2=Eat_2] & Catch1_1=Eat_1] & Catch1_75=Eat_75] & Catch1_15=Eat_15] & Catch1_77=Eat_77] & Catch1_42=Eat_42] & Catch1_17=Eat_17] & Catch1_67=Eat_67] & Catch1_10=Eat_10] & Catch1_23=Eat_23] & Catch1_25=Eat_25] & Catch1_83=Eat_83] & Catch1_34=Eat_34] & Catch1_14=Eat_14] & Catch1_84=Eat_84] & Catch1_21=Eat_21] & Catch1_43=Eat_43] & Catch1_37=Eat_37] & Catch1_40=Eat_40] & Catch1_69=Eat_69] & Catch1_64=Eat_64] & Catch1_24=Eat_24] & Catch1_93=Eat_93] & Catch1_41=Eat_41] & Catch1_39=Eat_39] & Catch1_16=Eat_16] & Catch1_82=Eat_82]]]]]

-> the formula is FALSE

FORMULA p_44_mix_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m26sec

STOP 1369705913

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

952 2216
iterations count:2292 (4), effective:300 (0)

initing FirstDep: 0m0sec


iterations count:500 (1), effective:0 (0)
3574 2738 3338 3642 2736 3418 3734 3198 3522 2758 3314 3650 2706 3454 2770 3266 3614 2778 3438 2782 3270 3638 2730 3478 2794 3322 3710 3098 3570 2806 3434 2788 3292
iterations count:33448 (66), effective:3604 (7)

iterations count:500 (1), effective:0 (0)
5698 5531 5006
iterations count:3254 (6), effective:337 (0)

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

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

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

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

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