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

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

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

execution on node 3: quadhexa-2.u-paris10.fr (runId=136968525000139_n_3)
=====================================================================
runnning marcie on Philosophers-PT-000200 (ReachabilityMarkingComparison)
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-000200, examination is ReachabilityMarkingComparison
=====================================================================

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

START 1369705468

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 1000 NrTr: 1000)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m2sec


-> reachability set: #nodes 5180 (5.2e+03) #states 265,613,988,875,874,769,338,781,322,035,779,626,829,233,452,653,394,495,974,574,961,739,092,490,901,302,182,994,384,699,044,001 (95)



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

checking: AG [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [[Eat_193=0.000000000000000 & [[Eat_81=0.000000000000000 & [[Eat_151=0.000000000000000 & [[Eat_72=0.000000000000000 & [[[[Eat_170=0.000000000000000 & [[[[[[[[[Eat_67=0.000000000000000 & [[Eat_32=0.000000000000000 & [[Eat_110=0.000000000000000 & [[Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [[[Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [[[Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [[[[Eat_103=0.000000000000000 & [[Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [[[[Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [[[Eat_36=0.000000000000000 & [[Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [[[Eat_152=0.000000000000000 & [[[[[[[Eat_25=0.000000000000000 & [[[[[Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [[[[Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [[[[[[[[[[[[[Eat_145=0.000000000000000 & [[[Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [[[[Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [[Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [[Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [[[[[Eat_123=0.000000000000000 & [[Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [[Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [[[Eat_94=0.000000000000000 & [[[[[[[Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [[[[[[[[Eat_18=0.000000000000000 & [[[[[[Eat_68=0.000000000000000 & [[Eat_82=0.000000000000000 & [[Eat_113=0.000000000000000 & [[[[[[Eat_175=0.000000000000000 & [[Eat_105=0.000000000000000 & [[Eat_74=0.000000000000000 & [[[Eat_182=0.000000000000000 & [[[Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [[Eat_199=0.000000000000000 & [[[Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [[[[[Eat_13=0.000000000000000 & [[[[[[[[Eat_186=0.000000000000000 & [[[Eat_89=0.000000000000000 & [[[[[[[Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000] & Eat_194=0.000000000000000] & Eat_61=0.000000000000000] & Eat_133=0.000000000000000] & Eat_50=0.000000000000000]] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000]] & Eat_75=0.000000000000000] & Eat_27=0.000000000000000] & Eat_181=0.000000000000000] & Eat_19=0.000000000000000] & Eat_164=0.000000000000000] & Eat_144=0.000000000000000] & Eat_91=0.000000000000000]] & Eat_131=0.000000000000000] & Eat_168=0.000000000000000] & Eat_169=0.000000000000000] & Eat_34=0.000000000000000]]]] & Eat_24=0.000000000000000] & Eat_188=0.000000000000000]] & Eat_93=0.000000000000000]]] & Eat_60=0.000000000000000] & Eat_146=0.000000000000000]] & Eat_8=0.000000000000000] & Eat_148=0.000000000000000]] & Eat_106=0.000000000000000]] & Eat_126=0.000000000000000]] & Eat_78=0.000000000000000] & Eat_21=0.000000000000000] & Eat_149=0.000000000000000] & Eat_197=0.000000000000000] & Eat_42=0.000000000000000]] & Eat_136=0.000000000000000]] & Eat_39=0.000000000000000]] & Eat_3=0.000000000000000] & Eat_47=0.000000000000000] & Eat_178=0.000000000000000] & Eat_191=0.000000000000000] & Eat_5=0.000000000000000]] & Eat_125=0.000000000000000] & Eat_26=0.000000000000000] & Eat_55=0.000000000000000] & Eat_160=0.000000000000000] & Eat_53=0.000000000000000] & Eat_137=0.000000000000000] & Eat_183=0.000000000000000]]] & Eat_127=0.000000000000000] & Eat_64=0.000000000000000] & Eat_132=0.000000000000000] & Eat_171=0.000000000000000] & Eat_77=0.000000000000000] & Eat_200=0.000000000000000]] & Eat_22=0.000000000000000] & Eat_117=0.000000000000000]]]]]]]] & Eat_4=0.000000000000000]]] & Eat_187=0.000000000000000]] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000] & Eat_156=0.000000000000000]]]] & Eat_87=0.000000000000000]]] & Eat_45=0.000000000000000]]] & Eat_37=0.000000000000000] & Eat_143=0.000000000000000] & Eat_177=0.000000000000000]]] & Eat_16=0.000000000000000] & Eat_98=0.000000000000000]] & Eat_159=0.000000000000000] & Eat_46=0.000000000000000] & Eat_142=0.000000000000000] & Eat_174=0.000000000000000] & Eat_120=0.000000000000000] & Eat_115=0.000000000000000] & Eat_112=0.000000000000000] & Eat_20=0.000000000000000] & Eat_73=0.000000000000000] & Eat_95=0.000000000000000] & Eat_63=0.000000000000000] & Eat_54=0.000000000000000]]] & Eat_90=0.000000000000000] & Eat_134=0.000000000000000] & Eat_192=0.000000000000000]]] & Eat_56=0.000000000000000] & Eat_35=0.000000000000000] & Eat_58=0.000000000000000] & Eat_190=0.000000000000000]] & Eat_184=0.000000000000000] & Eat_96=0.000000000000000] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000] & Eat_33=0.000000000000000] & Eat_118=0.000000000000000]] & Eat_85=0.000000000000000] & Eat_167=0.000000000000000]]] & Eat_129=0.000000000000000]] & Eat_15=0.000000000000000] & Eat_163=0.000000000000000]]] & Eat_57=0.000000000000000] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000]]] & Eat_138=0.000000000000000]] & Eat_30=0.000000000000000] & Eat_121=0.000000000000000] & Eat_84=0.000000000000000]]] & Eat_196=0.000000000000000] & Eat_11=0.000000000000000]]]] & Eat_104=0.000000000000000] & Eat_71=0.000000000000000]]] & Eat_140=0.000000000000000]] & Eat_185=0.000000000000000]] & Eat_195=0.000000000000000]] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000] & Eat_122=0.000000000000000] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000] & Eat_59=0.000000000000000] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000]] & Eat_2=0.000000000000000] & Eat_76=0.000000000000000] & Eat_154=0.000000000000000]] & Eat_92=0.000000000000000]] & Eat_10=0.000000000000000]] & Eat_97=0.000000000000000]] & Eat_69=0.000000000000000]]] & [Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [[Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [[Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [[Catch2_36=0.000000000000000 & [[[Catch2_83=0.000000000000000 & [[[Catch2_157=0.000000000000000 & [[[Catch2_24=0.000000000000000 & [[[Catch2_88=0.000000000000000 & [[[[[[[[[[[[Catch2_164=0.000000000000000 & [[[Catch2_170=0.000000000000000 & [[[Catch2_84=0.000000000000000 & [[[[[[Catch2_95=0.000000000000000 & [[[Catch2_112=0.000000000000000 & [[[[[[Catch2_188=0.000000000000000 & [[[Catch2_127=0.000000000000000 & [[[[[[Catch2_173=0.000000000000000 & [[[[[[Catch2_161=0.000000000000000 & [[[Catch2_117=0.000000000000000 & [[[Catch2_142=0.000000000000000 & [[[Catch2_102=0.000000000000000 & [[[Catch2_160=0.000000000000000 & [[[Catch2_66=0.000000000000000 & [[[Catch2_61=0.000000000000000 & [[[[[[Catch2_34=0.000000000000000 & [[[Catch2_176=0.000000000000000 & [[[[[[Catch2_13=0.000000000000000 & [[[Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [[[Catch2_101=0.000000000000000 & [[[[[[[Catch2_15=0.000000000000000 & [[Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [[[Catch2_106=0.000000000000000 & [[[[Catch2_9=0.000000000000000 & [[[[Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [[[[[[[Catch2_26=0.000000000000000 & [[Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [[[[Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [[Catch2_153=0.000000000000000 & [[Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [[[[Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [[[Catch2_94=0.000000000000000 & [[Catch2_46=0.000000000000000 & [[[[[Catch2_185=0.000000000000000 & [[Catch2_99=0.000000000000000 & [[[Catch2_52=0.000000000000000 & [[[[[[[[[[[Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [[[[Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [[Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]] & Catch2_177=0.000000000000000]]]]]]] & Catch2_44=0.000000000000000] & Catch2_78=0.000000000000000] & Catch2_192=0.000000000000000]]] & Catch2_135=0.000000000000000] & Catch2_124=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_183=0.000000000000000] & Catch2_63=0.000000000000000] & Catch2_163=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_156=0.000000000000000] & Catch2_162=0.000000000000000] & Catch2_11=0.000000000000000]] & Catch2_56=0.000000000000000] & Catch2_1=0.000000000000000]] & Catch2_37=0.000000000000000]] & Catch2_147=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_107=0.000000000000000] & Catch2_58=0.000000000000000]] & Catch2_139=0.000000000000000]] & Catch2_55=0.000000000000000] & Catch2_131=0.000000000000000]]] & Catch2_133=0.000000000000000] & Catch2_154=0.000000000000000] & Catch2_45=0.000000000000000]]] & Catch2_96=0.000000000000000]] & Catch2_128=0.000000000000000]]] & Catch2_114=0.000000000000000] & Catch2_68=0.000000000000000] & Catch2_198=0.000000000000000]]] & Catch2_49=0.000000000000000]] & Catch2_143=0.000000000000000] & Catch2_141=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_113=0.000000000000000] & Catch2_199=0.000000000000000] & Catch2_91=0.000000000000000]]] & Catch2_149=0.000000000000000] & Catch2_31=0.000000000000000] & Catch2_17=0.000000000000000]] & Catch2_79=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_39=0.000000000000000]] & Catch2_126=0.000000000000000] & Catch2_62=0.000000000000000]]]]] & Catch2_87=0.000000000000000]] & Catch2_35=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_171=0.000000000000000] & Catch2_80=0.000000000000000] & Catch2_104=0.000000000000000] & Catch2_196=0.000000000000000]] & Catch2_40=0.000000000000000] & Catch2_148=0.000000000000000]]] & Catch2_193=0.000000000000000] & Catch2_5=0.000000000000000]] & Catch2_20=0.000000000000000] & Catch2_145=0.000000000000000] & Catch2_121=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_21=0.000000000000000]] & Catch2_47=0.000000000000000] & Catch2_29=0.000000000000000]] & Catch2_165=0.000000000000000] & Catch2_76=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_27=0.000000000000000]] & Catch2_82=0.000000000000000] & Catch2_30=0.000000000000000]] & Catch2_123=0.000000000000000] & Catch2_32=0.000000000000000]] & Catch2_89=0.000000000000000] & Catch2_59=0.000000000000000]] & Catch2_2=0.000000000000000] & Catch2_175=0.000000000000000]] & Catch2_111=0.000000000000000] & Catch2_181=0.000000000000000]] & Catch2_19=0.000000000000000] & Catch2_122=0.000000000000000]] & Catch2_72=0.000000000000000] & Catch2_172=0.000000000000000] & Catch2_98=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_77=0.000000000000000]] & Catch2_115=0.000000000000000] & Catch2_155=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_189=0.000000000000000] & Catch2_103=0.000000000000000]] & Catch2_194=0.000000000000000] & Catch2_41=0.000000000000000]] & Catch2_118=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_150=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_38=0.000000000000000]] & Catch2_200=0.000000000000000] & Catch2_71=0.000000000000000]] & Catch2_108=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_136=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_93=0.000000000000000]] & Catch2_191=0.000000000000000] & Catch2_69=0.000000000000000]] & Catch2_137=0.000000000000000] & Catch2_7=0.000000000000000]] & Catch2_144=0.000000000000000] & Catch2_51=0.000000000000000] & Catch2_110=0.000000000000000] & Catch2_159=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_179=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_134=0.000000000000000] & Catch2_167=0.000000000000000] & Catch2_97=0.000000000000000]] & Catch2_180=0.000000000000000] & Catch2_53=0.000000000000000]] & Catch2_109=0.000000000000000] & Catch2_195=0.000000000000000]] & Catch2_186=0.000000000000000] & Catch2_48=0.000000000000000]] & Catch2_116=0.000000000000000] & Catch2_169=0.000000000000000]] & Catch2_119=0.000000000000000]]] & Catch2_85=0.000000000000000]]]] & Catch2_22=0.000000000000000]]]]]
normalized: ~ [E [true U ~ [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [[Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]]] & Eat_7=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [Catch2_119=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [Catch2_116=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_186=0.000000000000000 & [Catch2_157=0.000000000000000 & [Catch2_195=0.000000000000000 & [Catch2_109=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_180=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_167=0.000000000000000 & [Catch2_134=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_179=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_159=0.000000000000000 & [Catch2_110=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_144=0.000000000000000 & [Catch2_164=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_137=0.000000000000000 & [Catch2_170=0.000000000000000 & [Catch2_69=0.000000000000000 & [Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_136=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_108=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_200=0.000000000000000 & [Catch2_112=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_150=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_118=0.000000000000000 & [Catch2_188=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_172=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_161=0.000000000000000 & [Catch2_122=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_117=0.000000000000000 & [Catch2_181=0.000000000000000 & [Catch2_111=0.000000000000000 & [Catch2_142=0.000000000000000 & [Catch2_175=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_102=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_160=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_123=0.000000000000000 & [Catch2_66=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_165=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_176=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_121=0.000000000000000 & [Catch2_145=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_193=0.000000000000000 & [Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_148=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [Catch2_104=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_171=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_126=0.000000000000000 & [Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [Catch2_198=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [Catch2_133=0.000000000000000 & [Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_107=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [Catch2_156=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [Catch2_177=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_27_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m2sec

checking: AG [[[[[[[[Eat_81=0.000000000000000 & [[[[Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [[[[[[Eat_59=0.000000000000000 & [[[Eat_122=0.000000000000000 & [[[[[[[Eat_110=0.000000000000000 & [[[[[Eat_104=0.000000000000000 & [[[[[[[Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [[[[Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [[Eat_28=0.000000000000000 & [[[[Eat_163=0.000000000000000 & [[Eat_36=0.000000000000000 & [[[[Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [[[[[[Eat_184=0.000000000000000 & [[[[[Eat_56=0.000000000000000 & [[[[[[Eat_44=0.000000000000000 & [[[[[Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [[[[Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [[[[Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [[[[Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [[[[Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [[[[Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [[[[Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [[[[Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [[[Eat_77=0.000000000000000 & [[Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [[Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [[[Eat_160=0.000000000000000 & [[[Eat_125=0.000000000000000 & [[[Eat_191=0.000000000000000 & [[[[[Eat_39=0.000000000000000 & [[Eat_136=0.000000000000000 & [[Eat_42=0.000000000000000 & [[[Eat_21=0.000000000000000 & [[[Eat_126=0.000000000000000 & [[[[[[[[Eat_60=0.000000000000000 & [[Eat_109=0.000000000000000 & [[[[[Eat_155=0.000000000000000 & [[[Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [[Eat_131=0.000000000000000 & [[[Eat_144=0.000000000000000 & [[[[Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [[[[[[[Eat_61=0.000000000000000 & [[[[Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000] & Eat_194=0.000000000000000]] & Eat_133=0.000000000000000] & Eat_50=0.000000000000000] & Eat_89=0.000000000000000] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000] & Eat_186=0.000000000000000]]] & Eat_181=0.000000000000000] & Eat_19=0.000000000000000] & Eat_164=0.000000000000000]] & Eat_91=0.000000000000000] & Eat_13=0.000000000000000]] & Eat_168=0.000000000000000]]] & Eat_189=0.000000000000000] & Eat_114=0.000000000000000]] & Eat_24=0.000000000000000] & Eat_188=0.000000000000000] & Eat_199=0.000000000000000] & Eat_93=0.000000000000000]] & Eat_29=0.000000000000000]] & Eat_146=0.000000000000000] & Eat_182=0.000000000000000] & Eat_8=0.000000000000000] & Eat_148=0.000000000000000] & Eat_74=0.000000000000000] & Eat_106=0.000000000000000] & Eat_105=0.000000000000000]] & Eat_175=0.000000000000000] & Eat_78=0.000000000000000]] & Eat_149=0.000000000000000] & Eat_197=0.000000000000000]] & Eat_113=0.000000000000000]] & Eat_82=0.000000000000000]] & Eat_68=0.000000000000000] & Eat_3=0.000000000000000] & Eat_47=0.000000000000000] & Eat_178=0.000000000000000]] & Eat_5=0.000000000000000] & Eat_18=0.000000000000000]] & Eat_26=0.000000000000000] & Eat_55=0.000000000000000]] & Eat_53=0.000000000000000] & Eat_137=0.000000000000000]]]] & Eat_127=0.000000000000000]]] & Eat_171=0.000000000000000]] & Eat_200=0.000000000000000] & Eat_94=0.000000000000000]]] & Eat_12=0.000000000000000] & Eat_172=0.000000000000000] & Eat_17=0.000000000000000]]]] & Eat_88=0.000000000000000] & Eat_4=0.000000000000000] & Eat_23=0.000000000000000]]]] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000]]]] & Eat_86=0.000000000000000] & Eat_87=0.000000000000000] & Eat_66=0.000000000000000]]]] & Eat_108=0.000000000000000] & Eat_37=0.000000000000000] & Eat_143=0.000000000000000]]]] & Eat_16=0.000000000000000] & Eat_98=0.000000000000000] & Eat_145=0.000000000000000]]]] & Eat_174=0.000000000000000] & Eat_120=0.000000000000000] & Eat_115=0.000000000000000]]]] & Eat_95=0.000000000000000] & Eat_63=0.000000000000000] & Eat_54=0.000000000000000] & Eat_135=0.000000000000000]] & Eat_90=0.000000000000000] & Eat_134=0.000000000000000] & Eat_192=0.000000000000000] & Eat_43=0.000000000000000] & Eat_48=0.000000000000000]] & Eat_35=0.000000000000000] & Eat_58=0.000000000000000] & Eat_190=0.000000000000000] & Eat_25=0.000000000000000]] & Eat_96=0.000000000000000] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000] & Eat_33=0.000000000000000] & Eat_118=0.000000000000000]]]] & Eat_139=0.000000000000000] & Eat_102=0.000000000000000] & Eat_129=0.000000000000000]] & Eat_15=0.000000000000000]] & Eat_166=0.000000000000000] & Eat_1=0.000000000000000] & Eat_57=0.000000000000000]] & Eat_173=0.000000000000000]]] & Eat_138=0.000000000000000] & Eat_103=0.000000000000000] & Eat_30=0.000000000000000]]]] & Eat_130=0.000000000000000] & Eat_196=0.000000000000000] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000] & Eat_158=0.000000000000000] & Eat_128=0.000000000000000]] & Eat_71=0.000000000000000] & Eat_150=0.000000000000000] & Eat_153=0.000000000000000] & Eat_140=0.000000000000000]] & Eat_185=0.000000000000000] & Eat_32=0.000000000000000] & Eat_195=0.000000000000000] & Eat_67=0.000000000000000] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000]] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000]] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000] & Eat_170=0.000000000000000] & Eat_2=0.000000000000000] & Eat_76=0.000000000000000]]] & Eat_92=0.000000000000000] & Eat_151=0.000000000000000] & Eat_10=0.000000000000000]] & Eat_97=0.000000000000000] & Eat_193=0.000000000000000] & Eat_69=0.000000000000000] & Eat_165=0.000000000000000] & Eat_176=0.000000000000000] | [Catch2_10=0.000000000000000 & [[[[[[[[Catch2_125=0.000000000000000 & [[Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [[[[[[Catch2_195=0.000000000000000 & [[Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [[Catch2_88=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_200=0.000000000000000 & [[[[[[Catch2_118=0.000000000000000 & [[[Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [[[[[Catch2_72=0.000000000000000 & [[[[[[Catch2_111=0.000000000000000 & [[Catch2_175=0.000000000000000 & [[[[Catch2_89=0.000000000000000 & [[[[[Catch2_30=0.000000000000000 & [[[Catch2_27=0.000000000000000 & [[[Catch2_76=0.000000000000000 & [[[[[Catch2_176=0.000000000000000 & [[[[[Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [[[[[[[Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [[Catch2_80=0.000000000000000 & [[[[[[[Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [[[[[[[[[Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [[[[[Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [[[[[Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [[[[[Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [[[[[Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [[[[[Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [[[[[Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [[[[[[[[1.000000000000000=Catch2_105 & true] & Catch2_90=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_177=0.000000000000000] & Catch2_138=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_54=0.000000000000000] & Catch2_197=0.000000000000000]]]]] & Catch2_192=0.000000000000000] & Catch2_184=0.000000000000000] & Catch2_182=0.000000000000000] & Catch2_135=0.000000000000000]]]]]]] & Catch2_156=0.000000000000000] & Catch2_162=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_52=0.000000000000000]]]]]]] & Catch2_4=0.000000000000000] & Catch2_107=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_46=0.000000000000000]]]]]]] & Catch2_133=0.000000000000000] & Catch2_154=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_86=0.000000000000000]]]]]]] & Catch2_114=0.000000000000000] & Catch2_68=0.000000000000000] & Catch2_198=0.000000000000000] & Catch2_178=0.000000000000000]]]]]]] & Catch2_113=0.000000000000000] & Catch2_199=0.000000000000000] & Catch2_91=0.000000000000000] & Catch2_168=0.000000000000000]]] & Catch2_31=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_106=0.000000000000000] & Catch2_126=0.000000000000000]]]]] & Catch2_65=0.000000000000000] & Catch2_87=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_171=0.000000000000000]] & Catch2_104=0.000000000000000]]] & Catch2_40=0.000000000000000] & Catch2_148=0.000000000000000] & Catch2_57=0.000000000000000] & Catch2_129=0.000000000000000] & Catch2_193=0.000000000000000] & Catch2_5=0.000000000000000]]] & Catch2_145=0.000000000000000] & Catch2_121=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_21=0.000000000000000]] & Catch2_47=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_165=0.000000000000000]] & Catch2_92=0.000000000000000] & Catch2_73=0.000000000000000]] & Catch2_61=0.000000000000000] & Catch2_82=0.000000000000000]] & Catch2_66=0.000000000000000] & Catch2_123=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_160=0.000000000000000]] & Catch2_59=0.000000000000000] & Catch2_102=0.000000000000000] & Catch2_2=0.000000000000000]] & Catch2_142=0.000000000000000]] & Catch2_181=0.000000000000000] & Catch2_117=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_122=0.000000000000000] & Catch2_161=0.000000000000000]] & Catch2_172=0.000000000000000] & Catch2_98=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_77=0.000000000000000]]]]]]]]] & Catch2_41=0.000000000000000] & Catch2_188=0.000000000000000]] & Catch2_70=0.000000000000000] & Catch2_150=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_112=0.000000000000000]] & Catch2_71=0.000000000000000] & Catch2_95=0.000000000000000] & Catch2_108=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_136=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_93=0.000000000000000] & Catch2_84=0.000000000000000] & Catch2_191=0.000000000000000] & Catch2_69=0.000000000000000] & Catch2_170=0.000000000000000] & Catch2_137=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_164=0.000000000000000] & Catch2_144=0.000000000000000] & Catch2_51=0.000000000000000] & Catch2_110=0.000000000000000] & Catch2_159=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_179=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_134=0.000000000000000] & Catch2_167=0.000000000000000] & Catch2_97=0.000000000000000]] & Catch2_180=0.000000000000000]]] & Catch2_109=0.000000000000000]] & Catch2_157=0.000000000000000] & Catch2_186=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_83=0.000000000000000] & Catch2_116=0.000000000000000]]] & Catch2_119=0.000000000000000]] & Catch2_190=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_158=0.000000000000000] & Catch2_146=0.000000000000000] & Catch2_152=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_50=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [Catch2_119=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [Catch2_116=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_186=0.000000000000000 & [Catch2_157=0.000000000000000 & [Catch2_195=0.000000000000000 & [Catch2_109=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_180=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_167=0.000000000000000 & [Catch2_134=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_179=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_159=0.000000000000000 & [Catch2_110=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_144=0.000000000000000 & [Catch2_164=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_137=0.000000000000000 & [Catch2_170=0.000000000000000 & [Catch2_69=0.000000000000000 & [Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_136=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_108=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_200=0.000000000000000 & [Catch2_112=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_150=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_118=0.000000000000000 & [Catch2_188=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_172=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_161=0.000000000000000 & [Catch2_122=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_117=0.000000000000000 & [Catch2_181=0.000000000000000 & [Catch2_111=0.000000000000000 & [Catch2_142=0.000000000000000 & [Catch2_175=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_102=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_160=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_123=0.000000000000000 & [Catch2_66=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_165=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_176=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_121=0.000000000000000 & [Catch2_145=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_193=0.000000000000000 & [Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_148=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [Catch2_104=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_171=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_126=0.000000000000000 & [Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [Catch2_198=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [Catch2_133=0.000000000000000 & [Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_107=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [Catch2_156=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [Catch2_177=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_28_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [[[Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [[[Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [[[Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [[[Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [[[Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [[[Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [[[Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [[[Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [[[Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [[[Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [[[Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [[[Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [[[Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [[[Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [[[Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [[[Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [[[Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [[[Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [[[Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [[[Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [[[Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [[[Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [[[Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [[[Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [[[Eat_45=0.000000000000000 & [[[[[[[[[[[[[[[[[Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [[[[[[[[Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [[[[Eat_127=0.000000000000000 & [[[[Eat_137=0.000000000000000 & [[[[[Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [[[[Eat_47=0.000000000000000 & [[[[[Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [[[[Eat_21=0.000000000000000 & [[[[[[Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [[[[Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [[[[[[Eat_155=0.000000000000000 & [[[[[Eat_168=0.000000000000000 & [[[[[[[[Eat_27=0.000000000000000 & [[Eat_186=0.000000000000000 & [[[[[[Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [[[Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000]]] & Eat_133=0.000000000000000] & Eat_50=0.000000000000000] & Eat_89=0.000000000000000] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000]] & Eat_75=0.000000000000000]] & Eat_181=0.000000000000000] & Eat_19=0.000000000000000] & Eat_164=0.000000000000000] & Eat_144=0.000000000000000] & Eat_91=0.000000000000000] & Eat_13=0.000000000000000] & Eat_131=0.000000000000000]] & Eat_169=0.000000000000000] & Eat_34=0.000000000000000] & Eat_189=0.000000000000000] & Eat_114=0.000000000000000]] & Eat_24=0.000000000000000] & Eat_188=0.000000000000000] & Eat_199=0.000000000000000] & Eat_93=0.000000000000000] & Eat_109=0.000000000000000]]] & Eat_146=0.000000000000000] & Eat_182=0.000000000000000] & Eat_8=0.000000000000000]]] & Eat_106=0.000000000000000] & Eat_105=0.000000000000000] & Eat_126=0.000000000000000] & Eat_175=0.000000000000000] & Eat_78=0.000000000000000]] & Eat_149=0.000000000000000] & Eat_197=0.000000000000000] & Eat_42=0.000000000000000]]] & Eat_82=0.000000000000000] & Eat_39=0.000000000000000] & Eat_68=0.000000000000000] & Eat_3=0.000000000000000]] & Eat_178=0.000000000000000] & Eat_191=0.000000000000000] & Eat_5=0.000000000000000]]] & Eat_26=0.000000000000000] & Eat_55=0.000000000000000] & Eat_160=0.000000000000000] & Eat_53=0.000000000000000]] & Eat_183=0.000000000000000] & Eat_14=0.000000000000000] & Eat_111=0.000000000000000]] & Eat_64=0.000000000000000] & Eat_132=0.000000000000000] & Eat_171=0.000000000000000]]] & Eat_94=0.000000000000000] & Eat_22=0.000000000000000] & Eat_117=0.000000000000000] & Eat_12=0.000000000000000] & Eat_172=0.000000000000000] & Eat_17=0.000000000000000] & Eat_161=0.000000000000000]]] & Eat_88=0.000000000000000] & Eat_4=0.000000000000000] & Eat_23=0.000000000000000] & Eat_79=0.000000000000000] & Eat_187=0.000000000000000] & Eat_123=0.000000000000000] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000] & Eat_156=0.000000000000000] & Eat_100=0.000000000000000] & Eat_107=0.000000000000000] & Eat_86=0.000000000000000] & Eat_87=0.000000000000000] & Eat_66=0.000000000000000] & Eat_124=0.000000000000000]] & Eat_41=0.000000000000000] & Eat_108=0.000000000000000]]] & Eat_177=0.000000000000000] & Eat_49=0.000000000000000]]] & Eat_98=0.000000000000000] & Eat_145=0.000000000000000]]] & Eat_142=0.000000000000000] & Eat_174=0.000000000000000]]] & Eat_112=0.000000000000000] & Eat_20=0.000000000000000]]] & Eat_63=0.000000000000000] & Eat_54=0.000000000000000]]] & Eat_90=0.000000000000000] & Eat_134=0.000000000000000]]] & Eat_48=0.000000000000000] & Eat_56=0.000000000000000]]] & Eat_190=0.000000000000000] & Eat_25=0.000000000000000]]] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000]]] & Eat_152=0.000000000000000] & Eat_85=0.000000000000000]]] & Eat_102=0.000000000000000] & Eat_129=0.000000000000000]]] & Eat_163=0.000000000000000] & Eat_166=0.000000000000000]]] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000]]] & Eat_138=0.000000000000000] & Eat_103=0.000000000000000]]] & Eat_84=0.000000000000000] & Eat_9=0.000000000000000]]] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000]]] & Eat_104=0.000000000000000] & Eat_71=0.000000000000000]]] & Eat_140=0.000000000000000] & Eat_110=0.000000000000000]]] & Eat_195=0.000000000000000] & Eat_67=0.000000000000000]]] & Eat_122=0.000000000000000] & Eat_83=0.000000000000000]]] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000]]] & Eat_76=0.000000000000000] & Eat_154=0.000000000000000]]] & Eat_151=0.000000000000000] & Eat_10=0.000000000000000]]] & Eat_193=0.000000000000000] & Eat_69=0.000000000000000]]] & [Catch2_10=0.000000000000000 & [[[Catch2_152=0.000000000000000 & [[[[[Catch2_125=0.000000000000000 & [[[Catch2_169=0.000000000000000 & [[[Catch2_48=0.000000000000000 & [[[Catch2_195=0.000000000000000 & [[[[[[[[Catch2_134=0.000000000000000 & [[[Catch2_100=0.000000000000000 & [[[[[[Catch2_164=0.000000000000000 & [[Catch2_137=0.000000000000000 & [[[Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [[[[[Catch2_108=0.000000000000000 & [[[Catch2_200=0.000000000000000 & [[[[[[[[Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [[Catch2_103=0.000000000000000 & [[[Catch2_155=0.000000000000000 & [[[[[[Catch2_172=0.000000000000000 & [[[[[[[[[[[[Catch2_59=0.000000000000000 & [[[Catch2_32=0.000000000000000 & [[[[[[[[[[Catch2_165=0.000000000000000 & [[[[[[[[[[[[[[[Catch2_148=0.000000000000000 & [[[[Catch2_104=0.000000000000000 & [[[[[[Catch2_87=0.000000000000000 & [[[[[[[Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [[[[[[Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [[[Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [[[Catch2_143=0.000000000000000 & [[[Catch2_14=0.000000000000000 & [[[[Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [[[[Catch2_96=0.000000000000000 & [[[Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [[[[Catch2_131=0.000000000000000 & [[[Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [[[Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [[[Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [[[Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [[[Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [[[Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [[[Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [[[Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [[[Catch2_138=0.000000000000000 & [[[[1.000000000000000=Catch2_105 & true] & Catch2_90=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_177=0.000000000000000]] & Catch2_23=0.000000000000000] & Catch2_54=0.000000000000000]]] & Catch2_187=0.000000000000000] & Catch2_44=0.000000000000000]]] & Catch2_184=0.000000000000000] & Catch2_182=0.000000000000000]]] & Catch2_3=0.000000000000000] & Catch2_183=0.000000000000000]]] & Catch2_6=0.000000000000000] & Catch2_156=0.000000000000000]]] & Catch2_52=0.000000000000000] & Catch2_56=0.000000000000000]]] & Catch2_37=0.000000000000000] & Catch2_185=0.000000000000000]]] & Catch2_107=0.000000000000000] & Catch2_58=0.000000000000000]]] & Catch2_94=0.000000000000000] & Catch2_55=0.000000000000000]] & Catch2_174=0.000000000000000] & Catch2_140=0.000000000000000] & Catch2_133=0.000000000000000]]] & Catch2_86=0.000000000000000] & Catch2_166=0.000000000000000]] & Catch2_153=0.000000000000000] & Catch2_128=0.000000000000000] & Catch2_151=0.000000000000000]]] & Catch2_68=0.000000000000000] & Catch2_198=0.000000000000000] & Catch2_178=0.000000000000000]] & Catch2_49=0.000000000000000] & Catch2_26=0.000000000000000]] & Catch2_141=0.000000000000000] & Catch2_16=0.000000000000000]]] & Catch2_91=0.000000000000000] & Catch2_168=0.000000000000000]]] & Catch2_31=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_81=0.000000000000000]]] & Catch2_126=0.000000000000000] & Catch2_62=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_132=0.000000000000000] & Catch2_130=0.000000000000000] & Catch2_65=0.000000000000000]] & Catch2_15=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_171=0.000000000000000] & Catch2_80=0.000000000000000]] & Catch2_196=0.000000000000000] & Catch2_101=0.000000000000000] & Catch2_40=0.000000000000000]] & Catch2_57=0.000000000000000] & Catch2_129=0.000000000000000] & Catch2_193=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_20=0.000000000000000] & Catch2_145=0.000000000000000] & Catch2_121=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_176=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_34=0.000000000000000]] & Catch2_76=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_61=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_66=0.000000000000000] & Catch2_123=0.000000000000000]] & Catch2_160=0.000000000000000] & Catch2_89=0.000000000000000]] & Catch2_102=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_175=0.000000000000000] & Catch2_142=0.000000000000000] & Catch2_111=0.000000000000000] & Catch2_181=0.000000000000000] & Catch2_117=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_122=0.000000000000000] & Catch2_161=0.000000000000000] & Catch2_72=0.000000000000000]] & Catch2_98=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_77=0.000000000000000] & Catch2_173=0.000000000000000] & Catch2_115=0.000000000000000]] & Catch2_28=0.000000000000000] & Catch2_189=0.000000000000000]] & Catch2_127=0.000000000000000]]] & Catch2_188=0.000000000000000] & Catch2_118=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_150=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_112=0.000000000000000]] & Catch2_71=0.000000000000000] & Catch2_95=0.000000000000000]] & Catch2_64=0.000000000000000] & Catch2_136=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_93=0.000000000000000]]] & Catch2_69=0.000000000000000] & Catch2_170=0.000000000000000]] & Catch2_7=0.000000000000000]] & Catch2_144=0.000000000000000] & Catch2_51=0.000000000000000] & Catch2_110=0.000000000000000] & Catch2_159=0.000000000000000] & Catch2_67=0.000000000000000]] & Catch2_179=0.000000000000000] & Catch2_18=0.000000000000000]] & Catch2_167=0.000000000000000] & Catch2_97=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_180=0.000000000000000] & Catch2_53=0.000000000000000] & Catch2_24=0.000000000000000] & Catch2_109=0.000000000000000]] & Catch2_157=0.000000000000000] & Catch2_186=0.000000000000000]] & Catch2_83=0.000000000000000] & Catch2_116=0.000000000000000]] & Catch2_36=0.000000000000000] & Catch2_119=0.000000000000000]] & Catch2_190=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_158=0.000000000000000] & Catch2_146=0.000000000000000]] & Catch2_22=0.000000000000000] & Catch2_50=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [Catch2_119=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [Catch2_116=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_186=0.000000000000000 & [Catch2_157=0.000000000000000 & [Catch2_195=0.000000000000000 & [Catch2_109=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_180=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_167=0.000000000000000 & [Catch2_134=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_179=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_159=0.000000000000000 & [Catch2_110=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_144=0.000000000000000 & [Catch2_164=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_137=0.000000000000000 & [Catch2_170=0.000000000000000 & [Catch2_69=0.000000000000000 & [Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_136=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_108=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_200=0.000000000000000 & [Catch2_112=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_150=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_118=0.000000000000000 & [Catch2_188=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_172=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_161=0.000000000000000 & [Catch2_122=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_117=0.000000000000000 & [Catch2_181=0.000000000000000 & [Catch2_111=0.000000000000000 & [Catch2_142=0.000000000000000 & [Catch2_175=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_102=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_160=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_123=0.000000000000000 & [Catch2_66=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_165=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_176=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_121=0.000000000000000 & [Catch2_145=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_193=0.000000000000000 & [Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_148=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [Catch2_104=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_171=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_126=0.000000000000000 & [Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [Catch2_198=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [Catch2_133=0.000000000000000 & [Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_107=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [Catch2_156=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [Catch2_177=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_29_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[Eat_69=0.000000000000000 & [[[[[Eat_151=0.000000000000000 & [[[[[Eat_2=0.000000000000000 & [[[[[[[[[[Eat_67=0.000000000000000 & [[Eat_32=0.000000000000000 & [[[Eat_140=0.000000000000000 & [[[[[Eat_128=0.000000000000000 & [[[[[[[Eat_84=0.000000000000000 & [[[[[Eat_62=0.000000000000000 & [[[[[[[[[[Eat_129=0.000000000000000 & [[Eat_139=0.000000000000000 & [[[Eat_152=0.000000000000000 & [[[[[Eat_96=0.000000000000000 & [[[[[[[Eat_48=0.000000000000000 & [[[[[Eat_44=0.000000000000000 & [[[[[Eat_73=0.000000000000000 & [[[[[[[[[[[[[[[[[[Eat_41=0.000000000000000 & [[Eat_124=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[Eat_172=0.000000000000000 & [[[Eat_22=0.000000000000000 & [[[[[[[[Eat_111=0.000000000000000 & [[Eat_183=0.000000000000000 & [[[Eat_160=0.000000000000000 & [[Eat_26=0.000000000000000 & [[[[[[[[[[[[[[[[Eat_21=0.000000000000000 & [[[Eat_126=0.000000000000000 & [[[[[[[[[[[[[Eat_188=0.000000000000000 & [[[Eat_114=0.000000000000000 & [[[[[[[[[[Eat_19=0.000000000000000 & [[[Eat_75=0.000000000000000 & [[[[[[Eat_133=0.000000000000000 & [[[[[[true & 1.000000000000000=Eat_40] & Eat_99=0.000000000000000] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000] & Eat_194=0.000000000000000] & Eat_61=0.000000000000000]] & Eat_50=0.000000000000000] & Eat_89=0.000000000000000] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000] & Eat_186=0.000000000000000]] & Eat_27=0.000000000000000] & Eat_181=0.000000000000000]] & Eat_164=0.000000000000000] & Eat_144=0.000000000000000] & Eat_91=0.000000000000000] & Eat_13=0.000000000000000] & Eat_131=0.000000000000000] & Eat_168=0.000000000000000] & Eat_169=0.000000000000000] & Eat_34=0.000000000000000] & Eat_189=0.000000000000000]] & Eat_155=0.000000000000000] & Eat_24=0.000000000000000]] & Eat_199=0.000000000000000] & Eat_93=0.000000000000000] & Eat_109=0.000000000000000] & Eat_29=0.000000000000000] & Eat_60=0.000000000000000] & Eat_146=0.000000000000000] & Eat_182=0.000000000000000] & Eat_8=0.000000000000000] & Eat_148=0.000000000000000] & Eat_74=0.000000000000000] & Eat_106=0.000000000000000] & Eat_105=0.000000000000000]] & Eat_175=0.000000000000000] & Eat_78=0.000000000000000]] & Eat_149=0.000000000000000] & Eat_197=0.000000000000000] & Eat_42=0.000000000000000] & Eat_113=0.000000000000000] & Eat_136=0.000000000000000] & Eat_82=0.000000000000000] & Eat_39=0.000000000000000] & Eat_68=0.000000000000000] & Eat_3=0.000000000000000] & Eat_47=0.000000000000000] & Eat_178=0.000000000000000] & Eat_191=0.000000000000000] & Eat_5=0.000000000000000] & Eat_18=0.000000000000000] & Eat_125=0.000000000000000]] & Eat_55=0.000000000000000]] & Eat_53=0.000000000000000] & Eat_137=0.000000000000000]] & Eat_14=0.000000000000000]] & Eat_127=0.000000000000000] & Eat_64=0.000000000000000] & Eat_132=0.000000000000000] & Eat_171=0.000000000000000] & Eat_77=0.000000000000000] & Eat_200=0.000000000000000] & Eat_94=0.000000000000000]] & Eat_117=0.000000000000000] & Eat_12=0.000000000000000]] & Eat_17=0.000000000000000] & Eat_161=0.000000000000000] & Eat_51=0.000000000000000] & Eat_157=0.000000000000000] & Eat_88=0.000000000000000] & Eat_4=0.000000000000000] & Eat_23=0.000000000000000] & Eat_79=0.000000000000000] & Eat_187=0.000000000000000] & Eat_123=0.000000000000000] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000] & Eat_156=0.000000000000000] & Eat_100=0.000000000000000] & Eat_107=0.000000000000000] & Eat_86=0.000000000000000] & Eat_87=0.000000000000000] & Eat_66=0.000000000000000]] & Eat_45=0.000000000000000]] & Eat_108=0.000000000000000] & Eat_37=0.000000000000000] & Eat_143=0.000000000000000] & Eat_177=0.000000000000000] & Eat_49=0.000000000000000] & Eat_119=0.000000000000000] & Eat_16=0.000000000000000] & Eat_98=0.000000000000000] & Eat_145=0.000000000000000] & Eat_159=0.000000000000000] & Eat_46=0.000000000000000] & Eat_142=0.000000000000000] & Eat_174=0.000000000000000] & Eat_120=0.000000000000000] & Eat_115=0.000000000000000] & Eat_112=0.000000000000000] & Eat_20=0.000000000000000]] & Eat_95=0.000000000000000] & Eat_63=0.000000000000000] & Eat_54=0.000000000000000] & Eat_135=0.000000000000000]] & Eat_90=0.000000000000000] & Eat_134=0.000000000000000] & Eat_192=0.000000000000000] & Eat_43=0.000000000000000]] & Eat_56=0.000000000000000] & Eat_35=0.000000000000000] & Eat_58=0.000000000000000] & Eat_190=0.000000000000000] & Eat_25=0.000000000000000] & Eat_184=0.000000000000000]] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000] & Eat_33=0.000000000000000] & Eat_118=0.000000000000000]] & Eat_85=0.000000000000000] & Eat_167=0.000000000000000]] & Eat_102=0.000000000000000]] & Eat_36=0.000000000000000] & Eat_15=0.000000000000000] & Eat_163=0.000000000000000] & Eat_166=0.000000000000000] & Eat_1=0.000000000000000] & Eat_57=0.000000000000000] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000] & Eat_116=0.000000000000000]] & Eat_138=0.000000000000000] & Eat_103=0.000000000000000] & Eat_30=0.000000000000000] & Eat_121=0.000000000000000]] & Eat_9=0.000000000000000] & Eat_130=0.000000000000000] & Eat_196=0.000000000000000] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000] & Eat_158=0.000000000000000]] & Eat_104=0.000000000000000] & Eat_71=0.000000000000000] & Eat_150=0.000000000000000] & Eat_153=0.000000000000000]] & Eat_110=0.000000000000000] & Eat_185=0.000000000000000]] & Eat_195=0.000000000000000]] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000] & Eat_122=0.000000000000000] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000] & Eat_59=0.000000000000000] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000] & Eat_170=0.000000000000000]] & Eat_76=0.000000000000000] & Eat_154=0.000000000000000] & Eat_72=0.000000000000000] & Eat_92=0.000000000000000]] & Eat_10=0.000000000000000] & Eat_81=0.000000000000000] & Eat_97=0.000000000000000] & Eat_193=0.000000000000000]] & Eat_165=0.000000000000000] & Eat_176=0.000000000000000] | [[[[[[[[[[Catch2_119=0.000000000000000 & [[[[[Catch2_48=0.000000000000000 & [[[[[Catch2_24=0.000000000000000 & [[[[[[[Catch2_18=0.000000000000000 & [[[[[Catch2_110=0.000000000000000 & [[[[[[[Catch2_69=0.000000000000000 & [[[[[[[Catch2_108=0.000000000000000 & [[[[[[[[[[Catch2_188=0.000000000000000 & [[Catch2_194=0.000000000000000 & [[[[[Catch2_155=0.000000000000000 & [[[[[Catch2_98=0.000000000000000 & [[Catch2_72=0.000000000000000 & [[[[[[[[[[[[Catch2_89=0.000000000000000 & [[[[[[[[[[[[Catch2_165=0.000000000000000 & [[[[[[[[[[Catch2_13=0.000000000000000 & [[[[[[[Catch2_101=0.000000000000000 & [[[[[[[Catch2_15=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_139=0.000000000000000 & [[[[[[[[[[[[[[[[[[[Catch2_3=0.000000000000000 & [[[[[Catch2_192=0.000000000000000 & [[[[[Catch2_197=0.000000000000000 & [[[[[[[1.000000000000000=Catch2_105 & true] & Catch2_90=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_177=0.000000000000000] & Catch2_138=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_54=0.000000000000000]] & Catch2_12=0.000000000000000] & Catch2_187=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_78=0.000000000000000]] & Catch2_184=0.000000000000000] & Catch2_182=0.000000000000000] & Catch2_135=0.000000000000000] & Catch2_124=0.000000000000000]] & Catch2_183=0.000000000000000] & Catch2_63=0.000000000000000] & Catch2_163=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_156=0.000000000000000] & Catch2_162=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_52=0.000000000000000] & Catch2_56=0.000000000000000] & Catch2_1=0.000000000000000] & Catch2_99=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_185=0.000000000000000] & Catch2_147=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_107=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_46=0.000000000000000]] & Catch2_94=0.000000000000000] & Catch2_55=0.000000000000000] & Catch2_131=0.000000000000000] & Catch2_174=0.000000000000000] & Catch2_140=0.000000000000000] & Catch2_133=0.000000000000000] & Catch2_154=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_86=0.000000000000000] & Catch2_166=0.000000000000000] & Catch2_96=0.000000000000000] & Catch2_153=0.000000000000000] & Catch2_128=0.000000000000000] & Catch2_151=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_114=0.000000000000000] & Catch2_68=0.000000000000000] & Catch2_198=0.000000000000000] & Catch2_178=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_143=0.000000000000000] & Catch2_141=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_113=0.000000000000000] & Catch2_199=0.000000000000000] & Catch2_91=0.000000000000000] & Catch2_168=0.000000000000000] & Catch2_120=0.000000000000000] & Catch2_149=0.000000000000000] & Catch2_31=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_106=0.000000000000000] & Catch2_126=0.000000000000000] & Catch2_62=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_132=0.000000000000000] & Catch2_130=0.000000000000000] & Catch2_65=0.000000000000000] & Catch2_87=0.000000000000000]] & Catch2_35=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_171=0.000000000000000] & Catch2_80=0.000000000000000] & Catch2_104=0.000000000000000] & Catch2_196=0.000000000000000]] & Catch2_40=0.000000000000000] & Catch2_148=0.000000000000000] & Catch2_57=0.000000000000000] & Catch2_129=0.000000000000000] & Catch2_193=0.000000000000000] & Catch2_5=0.000000000000000]] & Catch2_20=0.000000000000000] & Catch2_145=0.000000000000000] & Catch2_121=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_176=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_34=0.000000000000000]] & Catch2_76=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_61=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_66=0.000000000000000] & Catch2_123=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_160=0.000000000000000]] & Catch2_59=0.000000000000000] & Catch2_102=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_175=0.000000000000000] & Catch2_142=0.000000000000000] & Catch2_111=0.000000000000000] & Catch2_181=0.000000000000000] & Catch2_117=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_122=0.000000000000000] & Catch2_161=0.000000000000000]] & Catch2_172=0.000000000000000]] & Catch2_60=0.000000000000000] & Catch2_77=0.000000000000000] & Catch2_173=0.000000000000000] & Catch2_115=0.000000000000000]] & Catch2_28=0.000000000000000] & Catch2_189=0.000000000000000] & Catch2_103=0.000000000000000] & Catch2_127=0.000000000000000]] & Catch2_41=0.000000000000000]] & Catch2_118=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_150=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_112=0.000000000000000] & Catch2_200=0.000000000000000] & Catch2_71=0.000000000000000] & Catch2_95=0.000000000000000]] & Catch2_64=0.000000000000000] & Catch2_136=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_93=0.000000000000000] & Catch2_84=0.000000000000000] & Catch2_191=0.000000000000000]] & Catch2_170=0.000000000000000] & Catch2_137=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_164=0.000000000000000] & Catch2_144=0.000000000000000] & Catch2_51=0.000000000000000]] & Catch2_159=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_179=0.000000000000000]] & Catch2_134=0.000000000000000] & Catch2_167=0.000000000000000] & Catch2_97=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_180=0.000000000000000] & Catch2_53=0.000000000000000]] & Catch2_109=0.000000000000000] & Catch2_195=0.000000000000000] & Catch2_157=0.000000000000000] & Catch2_186=0.000000000000000]] & Catch2_83=0.000000000000000] & Catch2_116=0.000000000000000] & Catch2_169=0.000000000000000] & Catch2_36=0.000000000000000]] & Catch2_125=0.000000000000000] & Catch2_190=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_158=0.000000000000000] & Catch2_146=0.000000000000000] & Catch2_152=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_50=0.000000000000000] & Catch2_10=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [Catch2_119=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [Catch2_116=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_186=0.000000000000000 & [Catch2_157=0.000000000000000 & [Catch2_195=0.000000000000000 & [Catch2_109=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_180=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_167=0.000000000000000 & [Catch2_134=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_179=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_159=0.000000000000000 & [Catch2_110=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_144=0.000000000000000 & [Catch2_164=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_137=0.000000000000000 & [Catch2_170=0.000000000000000 & [Catch2_69=0.000000000000000 & [Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_136=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_108=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_200=0.000000000000000 & [Catch2_112=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_150=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_118=0.000000000000000 & [Catch2_188=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_172=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_161=0.000000000000000 & [Catch2_122=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_117=0.000000000000000 & [Catch2_181=0.000000000000000 & [Catch2_111=0.000000000000000 & [Catch2_142=0.000000000000000 & [Catch2_175=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_102=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_160=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_123=0.000000000000000 & [Catch2_66=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_165=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_176=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_121=0.000000000000000 & [Catch2_145=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_193=0.000000000000000 & [Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_148=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [Catch2_104=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_171=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_126=0.000000000000000 & [Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [Catch2_198=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [Catch2_133=0.000000000000000 & [Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_107=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [Catch2_156=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [Catch2_177=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_30_markingcomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch2_10=0.000000000000000 & [[[[[[[[[[[[[Catch2_83=0.000000000000000 & [[[[[[[[[[[[[[[[[[Catch2_110=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_176=0.000000000000000 & [[[[Catch2_145=0.000000000000000 & [[[[[[[[[[[Catch2_104=0.000000000000000 & [[[[[[[[[[[[[[[[[[Catch2_17=0.000000000000000 & [[[[Catch2_168=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Catch2_154=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_182=0.000000000000000 & [[[[Catch2_44=0.000000000000000 & [[[[[[[Catch2_177=0.000000000000000 & [[Catch2_90=0.000000000000000 & [true & 1.000000000000000=Catch2_105]] & Catch2_42=0.000000000000000]] & Catch2_138=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_54=0.000000000000000] & Catch2_197=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_187=0.000000000000000]] & Catch2_78=0.000000000000000] & Catch2_192=0.000000000000000] & Catch2_184=0.000000000000000]] & Catch2_135=0.000000000000000] & Catch2_124=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_183=0.000000000000000] & Catch2_63=0.000000000000000] & Catch2_163=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_156=0.000000000000000] & Catch2_162=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_52=0.000000000000000] & Catch2_56=0.000000000000000] & Catch2_1=0.000000000000000] & Catch2_99=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_185=0.000000000000000] & Catch2_147=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_107=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_139=0.000000000000000] & Catch2_94=0.000000000000000] & Catch2_55=0.000000000000000] & Catch2_131=0.000000000000000] & Catch2_174=0.000000000000000] & Catch2_140=0.000000000000000] & Catch2_133=0.000000000000000]] & Catch2_45=0.000000000000000] & Catch2_86=0.000000000000000] & Catch2_166=0.000000000000000] & Catch2_96=0.000000000000000] & Catch2_153=0.000000000000000] & Catch2_128=0.000000000000000] & Catch2_151=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_114=0.000000000000000] & Catch2_68=0.000000000000000] & Catch2_198=0.000000000000000] & Catch2_178=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_143=0.000000000000000] & Catch2_141=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_113=0.000000000000000] & Catch2_199=0.000000000000000] & Catch2_91=0.000000000000000]] & Catch2_120=0.000000000000000] & Catch2_149=0.000000000000000] & Catch2_31=0.000000000000000]] & Catch2_9=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_106=0.000000000000000] & Catch2_126=0.000000000000000] & Catch2_62=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_132=0.000000000000000] & Catch2_130=0.000000000000000] & Catch2_65=0.000000000000000] & Catch2_87=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_171=0.000000000000000] & Catch2_80=0.000000000000000]] & Catch2_196=0.000000000000000] & Catch2_101=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_148=0.000000000000000] & Catch2_57=0.000000000000000] & Catch2_129=0.000000000000000] & Catch2_193=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_20=0.000000000000000]] & Catch2_121=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_21=0.000000000000000]] & Catch2_47=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_165=0.000000000000000] & Catch2_76=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_61=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_66=0.000000000000000] & Catch2_123=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_160=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_59=0.000000000000000] & Catch2_102=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_175=0.000000000000000] & Catch2_142=0.000000000000000] & Catch2_111=0.000000000000000] & Catch2_181=0.000000000000000] & Catch2_117=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_122=0.000000000000000] & Catch2_161=0.000000000000000] & Catch2_72=0.000000000000000] & Catch2_172=0.000000000000000] & Catch2_98=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_77=0.000000000000000] & Catch2_173=0.000000000000000] & Catch2_115=0.000000000000000] & Catch2_155=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_189=0.000000000000000] & Catch2_103=0.000000000000000] & Catch2_127=0.000000000000000] & Catch2_194=0.000000000000000] & Catch2_41=0.000000000000000] & Catch2_188=0.000000000000000] & Catch2_118=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_150=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_112=0.000000000000000] & Catch2_200=0.000000000000000] & Catch2_71=0.000000000000000] & Catch2_95=0.000000000000000] & Catch2_108=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_136=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_93=0.000000000000000] & Catch2_84=0.000000000000000] & Catch2_191=0.000000000000000] & Catch2_69=0.000000000000000] & Catch2_170=0.000000000000000] & Catch2_137=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_164=0.000000000000000] & Catch2_144=0.000000000000000] & Catch2_51=0.000000000000000]] & Catch2_159=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_179=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_134=0.000000000000000] & Catch2_167=0.000000000000000] & Catch2_97=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_180=0.000000000000000] & Catch2_53=0.000000000000000] & Catch2_24=0.000000000000000] & Catch2_109=0.000000000000000] & Catch2_195=0.000000000000000] & Catch2_157=0.000000000000000] & Catch2_186=0.000000000000000] & Catch2_48=0.000000000000000]] & Catch2_116=0.000000000000000] & Catch2_169=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_119=0.000000000000000] & Catch2_125=0.000000000000000] & Catch2_190=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_158=0.000000000000000] & Catch2_146=0.000000000000000] & Catch2_152=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_50=0.000000000000000]] & [[[[Eat_193=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Eat_185=0.000000000000000 & [[[[[[[[[[[Eat_196=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[Eat_118=0.000000000000000 & [[[[[[[Eat_190=0.000000000000000 & [[[[[[[[[[[Eat_54=0.000000000000000 & [[Eat_95=0.000000000000000 & [[[[[[[[[[[[[[[Eat_177=0.000000000000000 & [[[[[[[[[[[Eat_100=0.000000000000000 & [[[[[[[[[[[[[[[[Eat_12=0.000000000000000 & [[[[Eat_200=0.000000000000000 & [[[[[Eat_127=0.000000000000000 & [[Eat_14=0.000000000000000 & [[[[[[[[[[[Eat_178=0.000000000000000 & [[[[[Eat_82=0.000000000000000 & [[[[[[[Eat_78=0.000000000000000 & [[[[[[[[[Eat_146=0.000000000000000 & [[[[[[[Eat_24=0.000000000000000 & [[[[[[[[[Eat_91=0.000000000000000 & [[[[[[[[[[Eat_89=0.000000000000000 & [[[[[[[Eat_99=0.000000000000000 & [true & 1.000000000000000=Eat_40]] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000] & Eat_194=0.000000000000000] & Eat_61=0.000000000000000] & Eat_133=0.000000000000000] & Eat_50=0.000000000000000]] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000] & Eat_186=0.000000000000000] & Eat_75=0.000000000000000] & Eat_27=0.000000000000000] & Eat_181=0.000000000000000] & Eat_19=0.000000000000000] & Eat_164=0.000000000000000] & Eat_144=0.000000000000000]] & Eat_13=0.000000000000000] & Eat_131=0.000000000000000] & Eat_168=0.000000000000000] & Eat_169=0.000000000000000] & Eat_34=0.000000000000000] & Eat_189=0.000000000000000] & Eat_114=0.000000000000000] & Eat_155=0.000000000000000]] & Eat_188=0.000000000000000] & Eat_199=0.000000000000000] & Eat_93=0.000000000000000] & Eat_109=0.000000000000000] & Eat_29=0.000000000000000] & Eat_60=0.000000000000000]] & Eat_182=0.000000000000000] & Eat_8=0.000000000000000] & Eat_148=0.000000000000000] & Eat_74=0.000000000000000] & Eat_106=0.000000000000000] & Eat_105=0.000000000000000] & Eat_126=0.000000000000000] & Eat_175=0.000000000000000]] & Eat_21=0.000000000000000] & Eat_149=0.000000000000000] & Eat_197=0.000000000000000] & Eat_42=0.000000000000000] & Eat_113=0.000000000000000] & Eat_136=0.000000000000000]] & Eat_39=0.000000000000000] & Eat_68=0.000000000000000] & Eat_3=0.000000000000000] & Eat_47=0.000000000000000]] & Eat_191=0.000000000000000] & Eat_5=0.000000000000000] & Eat_18=0.000000000000000] & Eat_125=0.000000000000000] & Eat_26=0.000000000000000] & Eat_55=0.000000000000000] & Eat_160=0.000000000000000] & Eat_53=0.000000000000000] & Eat_137=0.000000000000000] & Eat_183=0.000000000000000]] & Eat_111=0.000000000000000]] & Eat_64=0.000000000000000] & Eat_132=0.000000000000000] & Eat_171=0.000000000000000] & Eat_77=0.000000000000000]] & Eat_94=0.000000000000000] & Eat_22=0.000000000000000] & Eat_117=0.000000000000000]] & Eat_172=0.000000000000000] & Eat_17=0.000000000000000] & Eat_161=0.000000000000000] & Eat_51=0.000000000000000] & Eat_157=0.000000000000000] & Eat_88=0.000000000000000] & Eat_4=0.000000000000000] & Eat_23=0.000000000000000] & Eat_79=0.000000000000000] & Eat_187=0.000000000000000] & Eat_123=0.000000000000000] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000] & Eat_156=0.000000000000000]] & Eat_107=0.000000000000000] & Eat_86=0.000000000000000] & Eat_87=0.000000000000000] & Eat_66=0.000000000000000] & Eat_124=0.000000000000000] & Eat_45=0.000000000000000] & Eat_41=0.000000000000000] & Eat_108=0.000000000000000] & Eat_37=0.000000000000000] & Eat_143=0.000000000000000]] & Eat_49=0.000000000000000] & Eat_119=0.000000000000000] & Eat_16=0.000000000000000] & Eat_98=0.000000000000000] & Eat_145=0.000000000000000] & Eat_159=0.000000000000000] & Eat_46=0.000000000000000] & Eat_142=0.000000000000000] & Eat_174=0.000000000000000] & Eat_120=0.000000000000000] & Eat_115=0.000000000000000] & Eat_112=0.000000000000000] & Eat_20=0.000000000000000] & Eat_73=0.000000000000000]] & Eat_63=0.000000000000000]] & Eat_135=0.000000000000000] & Eat_44=0.000000000000000] & Eat_90=0.000000000000000] & Eat_134=0.000000000000000] & Eat_192=0.000000000000000] & Eat_43=0.000000000000000] & Eat_48=0.000000000000000] & Eat_56=0.000000000000000] & Eat_35=0.000000000000000] & Eat_58=0.000000000000000]] & Eat_25=0.000000000000000] & Eat_184=0.000000000000000] & Eat_96=0.000000000000000] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000] & Eat_33=0.000000000000000]] & Eat_152=0.000000000000000] & Eat_85=0.000000000000000] & Eat_167=0.000000000000000] & Eat_139=0.000000000000000] & Eat_102=0.000000000000000] & Eat_129=0.000000000000000] & Eat_36=0.000000000000000] & Eat_15=0.000000000000000] & Eat_163=0.000000000000000] & Eat_166=0.000000000000000] & Eat_1=0.000000000000000] & Eat_57=0.000000000000000] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000] & Eat_116=0.000000000000000] & Eat_62=0.000000000000000] & Eat_138=0.000000000000000] & Eat_103=0.000000000000000] & Eat_30=0.000000000000000] & Eat_121=0.000000000000000] & Eat_84=0.000000000000000] & Eat_9=0.000000000000000] & Eat_130=0.000000000000000]] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000] & Eat_158=0.000000000000000] & Eat_128=0.000000000000000] & Eat_104=0.000000000000000] & Eat_71=0.000000000000000] & Eat_150=0.000000000000000] & Eat_153=0.000000000000000] & Eat_140=0.000000000000000] & Eat_110=0.000000000000000]] & Eat_32=0.000000000000000] & Eat_195=0.000000000000000] & Eat_67=0.000000000000000] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000] & Eat_122=0.000000000000000] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000] & Eat_59=0.000000000000000] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000] & Eat_170=0.000000000000000] & Eat_2=0.000000000000000] & Eat_76=0.000000000000000] & Eat_154=0.000000000000000] & Eat_72=0.000000000000000] & Eat_92=0.000000000000000] & Eat_151=0.000000000000000] & Eat_10=0.000000000000000] & Eat_81=0.000000000000000] & Eat_97=0.000000000000000]] & Eat_69=0.000000000000000] & Eat_165=0.000000000000000] & Eat_176=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_10=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_152=0.000000000000000 & [Catch2_146=0.000000000000000 & [Catch2_158=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_190=0.000000000000000 & [Catch2_125=0.000000000000000 & [Catch2_119=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_169=0.000000000000000 & [Catch2_116=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_186=0.000000000000000 & [Catch2_157=0.000000000000000 & [Catch2_195=0.000000000000000 & [Catch2_109=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_180=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_167=0.000000000000000 & [Catch2_134=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_179=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_159=0.000000000000000 & [Catch2_110=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_144=0.000000000000000 & [Catch2_164=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_137=0.000000000000000 & [Catch2_170=0.000000000000000 & [Catch2_69=0.000000000000000 & [Catch2_191=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_136=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_108=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_200=0.000000000000000 & [Catch2_112=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_150=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_118=0.000000000000000 & [Catch2_188=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_194=0.000000000000000 & [Catch2_127=0.000000000000000 & [Catch2_103=0.000000000000000 & [Catch2_189=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_155=0.000000000000000 & [Catch2_115=0.000000000000000 & [Catch2_173=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_172=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_161=0.000000000000000 & [Catch2_122=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_117=0.000000000000000 & [Catch2_181=0.000000000000000 & [Catch2_111=0.000000000000000 & [Catch2_142=0.000000000000000 & [Catch2_175=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_102=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_160=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_123=0.000000000000000 & [Catch2_66=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_165=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_176=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_121=0.000000000000000 & [Catch2_145=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_193=0.000000000000000 & [Catch2_129=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_148=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_101=0.000000000000000 & [Catch2_196=0.000000000000000 & [Catch2_104=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_171=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_130=0.000000000000000 & [Catch2_132=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_126=0.000000000000000 & [Catch2_106=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_149=0.000000000000000 & [Catch2_120=0.000000000000000 & [Catch2_168=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_199=0.000000000000000 & [Catch2_113=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_141=0.000000000000000 & [Catch2_143=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_178=0.000000000000000 & [Catch2_198=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_114=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_151=0.000000000000000 & [Catch2_128=0.000000000000000 & [Catch2_153=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_166=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_154=0.000000000000000 & [Catch2_133=0.000000000000000 & [Catch2_140=0.000000000000000 & [Catch2_174=0.000000000000000 & [Catch2_131=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_139=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_107=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_147=0.000000000000000 & [Catch2_185=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_162=0.000000000000000 & [Catch2_156=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_163=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_183=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_124=0.000000000000000 & [Catch2_135=0.000000000000000 & [Catch2_182=0.000000000000000 & [Catch2_184=0.000000000000000 & [Catch2_192=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_187=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_197=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_138=0.000000000000000 & [Catch2_177=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_90=0.000000000000000 & [1.000000000000000=Catch2_105 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_31_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Eat_165=0.000000000000000 & [[[[[[[Eat_92=0.000000000000000 & [[Eat_154=0.000000000000000 & [[[[[[[[[Eat_122=0.000000000000000 & [[[[[[[[[Eat_153=0.000000000000000 & [[Eat_71=0.000000000000000 & [[[[[[[[[[[[[Eat_138=0.000000000000000 & [[[[[[[[[[[Eat_129=0.000000000000000 & [[[[[[Eat_118=0.000000000000000 & [[[[[[[[[[[[[Eat_192=0.000000000000000 & [[Eat_90=0.000000000000000 & [[[[Eat_63=0.000000000000000 & [[[[Eat_112=0.000000000000000 & [[Eat_120=0.000000000000000 & [[[[Eat_159=0.000000000000000 & [[Eat_98=0.000000000000000 & [[[[[[[[[[[[Eat_87=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_137=0.000000000000000 & [[[[[[[[[[[[Eat_68=0.000000000000000 & [[Eat_82=0.000000000000000 & [[[[Eat_197=0.000000000000000 & [[[[[[[Eat_106=0.000000000000000 & [[[[[[Eat_60=0.000000000000000 & [[[[[[[[[[[[[Eat_131=0.000000000000000 & [[[[[[[Eat_27=0.000000000000000 & [[[[[[Eat_50=0.000000000000000 & [[[[[[[true & 1.000000000000000=Eat_17] & Eat_99=0.000000000000000] & Eat_6=0.000000000000000] & Eat_7=0.000000000000000] & Eat_194=0.000000000000000] & Eat_61=0.000000000000000] & Eat_133=0.000000000000000]] & Eat_89=0.000000000000000] & Eat_52=0.000000000000000] & Eat_38=0.000000000000000] & Eat_186=0.000000000000000] & Eat_75=0.000000000000000]] & Eat_181=0.000000000000000] & Eat_19=0.000000000000000] & Eat_164=0.000000000000000] & Eat_144=0.000000000000000] & Eat_91=0.000000000000000] & Eat_13=0.000000000000000]] & Eat_168=0.000000000000000] & Eat_169=0.000000000000000] & Eat_34=0.000000000000000] & Eat_189=0.000000000000000] & Eat_114=0.000000000000000] & Eat_155=0.000000000000000] & Eat_24=0.000000000000000] & Eat_188=0.000000000000000] & Eat_199=0.000000000000000] & Eat_93=0.000000000000000] & Eat_109=0.000000000000000] & Eat_29=0.000000000000000]] & Eat_146=0.000000000000000] & Eat_182=0.000000000000000] & Eat_8=0.000000000000000] & Eat_148=0.000000000000000] & Eat_74=0.000000000000000]] & Eat_105=0.000000000000000] & Eat_126=0.000000000000000] & Eat_175=0.000000000000000] & Eat_78=0.000000000000000] & Eat_21=0.000000000000000] & Eat_149=0.000000000000000]] & Eat_42=0.000000000000000] & Eat_113=0.000000000000000] & Eat_136=0.000000000000000]] & Eat_39=0.000000000000000]] & Eat_3=0.000000000000000] & Eat_47=0.000000000000000] & Eat_178=0.000000000000000] & Eat_191=0.000000000000000] & Eat_5=0.000000000000000] & Eat_18=0.000000000000000] & Eat_125=0.000000000000000] & Eat_26=0.000000000000000] & Eat_55=0.000000000000000] & Eat_160=0.000000000000000] & Eat_53=0.000000000000000]] & Eat_183=0.000000000000000] & Eat_14=0.000000000000000] & Eat_111=0.000000000000000] & Eat_127=0.000000000000000] & Eat_64=0.000000000000000] & Eat_132=0.000000000000000] & Eat_171=0.000000000000000] & Eat_77=0.000000000000000] & Eat_200=0.000000000000000] & Eat_94=0.000000000000000] & Eat_22=0.000000000000000] & Eat_117=0.000000000000000] & Eat_12=0.000000000000000] & Eat_172=0.000000000000000] & Eat_161=0.000000000000000] & Eat_51=0.000000000000000] & Eat_157=0.000000000000000] & Eat_88=0.000000000000000] & Eat_4=0.000000000000000] & Eat_23=0.000000000000000] & Eat_79=0.000000000000000] & Eat_187=0.000000000000000] & Eat_40=0.000000000000000] & Eat_123=0.000000000000000] & Eat_141=0.000000000000000] & Eat_65=0.000000000000000] & Eat_31=0.000000000000000] & Eat_156=0.000000000000000] & Eat_100=0.000000000000000] & Eat_107=0.000000000000000] & Eat_86=0.000000000000000]] & Eat_66=0.000000000000000] & Eat_124=0.000000000000000] & Eat_45=0.000000000000000] & Eat_41=0.000000000000000] & Eat_108=0.000000000000000] & Eat_37=0.000000000000000] & Eat_143=0.000000000000000] & Eat_177=0.000000000000000] & Eat_49=0.000000000000000] & Eat_119=0.000000000000000] & Eat_16=0.000000000000000]] & Eat_145=0.000000000000000]] & Eat_46=0.000000000000000] & Eat_142=0.000000000000000] & Eat_174=0.000000000000000]] & Eat_115=0.000000000000000]] & Eat_20=0.000000000000000] & Eat_73=0.000000000000000] & Eat_95=0.000000000000000]] & Eat_54=0.000000000000000] & Eat_135=0.000000000000000] & Eat_44=0.000000000000000]] & Eat_134=0.000000000000000]] & Eat_43=0.000000000000000] & Eat_48=0.000000000000000] & Eat_56=0.000000000000000] & Eat_35=0.000000000000000] & Eat_58=0.000000000000000] & Eat_190=0.000000000000000] & Eat_25=0.000000000000000] & Eat_184=0.000000000000000] & Eat_96=0.000000000000000] & Eat_147=0.000000000000000] & Eat_162=0.000000000000000] & Eat_33=0.000000000000000]] & Eat_152=0.000000000000000] & Eat_85=0.000000000000000] & Eat_167=0.000000000000000] & Eat_139=0.000000000000000] & Eat_102=0.000000000000000]] & Eat_36=0.000000000000000] & Eat_15=0.000000000000000] & Eat_163=0.000000000000000] & Eat_166=0.000000000000000] & Eat_1=0.000000000000000] & Eat_57=0.000000000000000] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000] & Eat_116=0.000000000000000] & Eat_62=0.000000000000000]] & Eat_103=0.000000000000000] & Eat_30=0.000000000000000] & Eat_121=0.000000000000000] & Eat_84=0.000000000000000] & Eat_9=0.000000000000000] & Eat_130=0.000000000000000] & Eat_196=0.000000000000000] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000] & Eat_158=0.000000000000000] & Eat_128=0.000000000000000] & Eat_104=0.000000000000000]] & Eat_150=0.000000000000000]] & Eat_140=0.000000000000000] & Eat_110=0.000000000000000] & Eat_185=0.000000000000000] & Eat_32=0.000000000000000] & Eat_195=0.000000000000000] & Eat_67=0.000000000000000] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000]] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000] & Eat_59=0.000000000000000] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000] & Eat_170=0.000000000000000] & Eat_2=0.000000000000000] & Eat_76=0.000000000000000]] & Eat_72=0.000000000000000]] & Eat_151=0.000000000000000] & Eat_10=0.000000000000000] & Eat_81=0.000000000000000] & Eat_97=0.000000000000000] & Eat_193=0.000000000000000] & Eat_69=0.000000000000000]] & Eat_176=0.000000000000000] & [[[true & 1.000000000000000<=Eat_173] & true] & [[false | 1.000000000000000 normalized: ~ [E [true U ~ [[[[[Eat_176!=0.000000000000000 | [Eat_165!=0.000000000000000 | [Eat_69!=0.000000000000000 | [Eat_193!=0.000000000000000 | [Eat_97!=0.000000000000000 | [Eat_81!=0.000000000000000 | [Eat_10!=0.000000000000000 | [Eat_151!=0.000000000000000 | [Eat_92!=0.000000000000000 | [Eat_72!=0.000000000000000 | [Eat_154!=0.000000000000000 | [Eat_76!=0.000000000000000 | [Eat_2!=0.000000000000000 | [Eat_170!=0.000000000000000 | [Eat_101!=0.000000000000000 | [Eat_180!=0.000000000000000 | [Eat_59!=0.000000000000000 | [Eat_80!=0.000000000000000 | [Eat_83!=0.000000000000000 | [Eat_122!=0.000000000000000 | [Eat_198!=0.000000000000000 | [Eat_70!=0.000000000000000 | [Eat_67!=0.000000000000000 | [Eat_195!=0.000000000000000 | [Eat_32!=0.000000000000000 | [Eat_185!=0.000000000000000 | [Eat_110!=0.000000000000000 | [Eat_140!=0.000000000000000 | [Eat_153!=0.000000000000000 | [Eat_150!=0.000000000000000 | [Eat_71!=0.000000000000000 | [Eat_104!=0.000000000000000 | [Eat_128!=0.000000000000000 | [Eat_158!=0.000000000000000 | [Eat_179!=0.000000000000000 | [Eat_11!=0.000000000000000 | [Eat_196!=0.000000000000000 | [Eat_130!=0.000000000000000 | [Eat_9!=0.000000000000000 | [Eat_84!=0.000000000000000 | [Eat_121!=0.000000000000000 | [Eat_30!=0.000000000000000 | [Eat_103!=0.000000000000000 | [Eat_138!=0.000000000000000 | [Eat_62!=0.000000000000000 | [Eat_116!=0.000000000000000 | [Eat_28!=0.000000000000000 | [Eat_57!=0.000000000000000 | [Eat_1!=0.000000000000000 | [Eat_166!=0.000000000000000 | [Eat_163!=0.000000000000000 | [Eat_15!=0.000000000000000 | [Eat_36!=0.000000000000000 | [Eat_129!=0.000000000000000 | [Eat_102!=0.000000000000000 | [Eat_139!=0.000000000000000 | [Eat_167!=0.000000000000000 | [Eat_85!=0.000000000000000 | [Eat_152!=0.000000000000000 | [Eat_118!=0.000000000000000 | [Eat_33!=0.000000000000000 | [Eat_162!=0.000000000000000 | [Eat_147!=0.000000000000000 | [Eat_96!=0.000000000000000 | [Eat_184!=0.000000000000000 | [Eat_25!=0.000000000000000 | [Eat_190!=0.000000000000000 | [Eat_58!=0.000000000000000 | [Eat_35!=0.000000000000000 | [Eat_56!=0.000000000000000 | [Eat_48!=0.000000000000000 | [Eat_43!=0.000000000000000 | [Eat_192!=0.000000000000000 | [Eat_134!=0.000000000000000 | [Eat_90!=0.000000000000000 | [Eat_44!=0.000000000000000 | [Eat_135!=0.000000000000000 | [Eat_54!=0.000000000000000 | [Eat_63!=0.000000000000000 | [Eat_95!=0.000000000000000 | [Eat_73!=0.000000000000000 | [Eat_20!=0.000000000000000 | [Eat_112!=0.000000000000000 | [Eat_115!=0.000000000000000 | [Eat_120!=0.000000000000000 | [Eat_174!=0.000000000000000 | [Eat_142!=0.000000000000000 | [Eat_46!=0.000000000000000 | [Eat_159!=0.000000000000000 | [Eat_145!=0.000000000000000 | [Eat_98!=0.000000000000000 | [Eat_16!=0.000000000000000 | [Eat_119!=0.000000000000000 | [Eat_49!=0.000000000000000 | [Eat_177!=0.000000000000000 | [Eat_143!=0.000000000000000 | [Eat_37!=0.000000000000000 | [Eat_108!=0.000000000000000 | [Eat_41!=0.000000000000000 | [Eat_45!=0.000000000000000 | [Eat_124!=0.000000000000000 | [Eat_66!=0.000000000000000 | [Eat_87!=0.000000000000000 | [Eat_86!=0.000000000000000 | [Eat_107!=0.000000000000000 | [Eat_100!=0.000000000000000 | [Eat_156!=0.000000000000000 | [Eat_31!=0.000000000000000 | [Eat_65!=0.000000000000000 | [Eat_141!=0.000000000000000 | [Eat_123!=0.000000000000000 | [Eat_40!=0.000000000000000 | [Eat_187!=0.000000000000000 | [Eat_79!=0.000000000000000 | [Eat_23!=0.000000000000000 | [Eat_4!=0.000000000000000 | [Eat_88!=0.000000000000000 | [Eat_157!=0.000000000000000 | [Eat_51!=0.000000000000000 | [Eat_161!=0.000000000000000 | [Eat_17!=0.000000000000000 | [Eat_172!=0.000000000000000 | [Eat_12!=0.000000000000000 | [Eat_117!=0.000000000000000 | [Eat_22!=0.000000000000000 | [Eat_94!=0.000000000000000 | [Eat_200!=0.000000000000000 | [Eat_77!=0.000000000000000 | [Eat_171!=0.000000000000000 | [Eat_132!=0.000000000000000 | [Eat_64!=0.000000000000000 | [Eat_127!=0.000000000000000 | [Eat_111!=0.000000000000000 | [Eat_14!=0.000000000000000 | [Eat_183!=0.000000000000000 | [Eat_137!=0.000000000000000 | [Eat_53!=0.000000000000000 | [Eat_160!=0.000000000000000 | [Eat_55!=0.000000000000000 | [Eat_26!=0.000000000000000 | [Eat_125!=0.000000000000000 | [Eat_18!=0.000000000000000 | [Eat_5!=0.000000000000000 | [Eat_191!=0.000000000000000 | [Eat_178!=0.000000000000000 | [Eat_47!=0.000000000000000 | [Eat_3!=0.000000000000000 | [Eat_68!=0.000000000000000 | [Eat_39!=0.000000000000000 | [Eat_82!=0.000000000000000 | [Eat_136!=0.000000000000000 | [Eat_113!=0.000000000000000 | [Eat_42!=0.000000000000000 | [Eat_197!=0.000000000000000 | [Eat_149!=0.000000000000000 | [Eat_21!=0.000000000000000 | [Eat_78!=0.000000000000000 | [Eat_175!=0.000000000000000 | [Eat_126!=0.000000000000000 | [Eat_105!=0.000000000000000 | [Eat_106!=0.000000000000000 | [Eat_74!=0.000000000000000 | [Eat_148!=0.000000000000000 | [Eat_8!=0.000000000000000 | [Eat_182!=0.000000000000000 | [Eat_146!=0.000000000000000 | [Eat_60!=0.000000000000000 | [Eat_29!=0.000000000000000 | [Eat_109!=0.000000000000000 | [Eat_93!=0.000000000000000 | [Eat_199!=0.000000000000000 | [Eat_188!=0.000000000000000 | [Eat_24!=0.000000000000000 | [Eat_155!=0.000000000000000 | [Eat_114!=0.000000000000000 | [Eat_189!=0.000000000000000 | [Eat_34!=0.000000000000000 | [Eat_169!=0.000000000000000 | [Eat_168!=0.000000000000000 | [Eat_131!=0.000000000000000 | [Eat_13!=0.000000000000000 | [Eat_91!=0.000000000000000 | [Eat_144!=0.000000000000000 | [Eat_164!=0.000000000000000 | [Eat_19!=0.000000000000000 | [Eat_181!=0.000000000000000 | [Eat_27!=0.000000000000000 | [Eat_75!=0.000000000000000 | [Eat_186!=0.000000000000000 | [Eat_38!=0.000000000000000 | [Eat_52!=0.000000000000000 | [Eat_89!=0.000000000000000 | [Eat_50!=0.000000000000000 | [Eat_133!=0.000000000000000 | [Eat_61!=0.000000000000000 | [Eat_194!=0.000000000000000 | [Eat_7!=0.000000000000000 | [Eat_6!=0.000000000000000 | [Eat_99!=0.000000000000000 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [1.000000000000000
-> the formula is FALSE

FORMULA p_32_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[Eat_10!=0.000000000000000 | [[[[[[[[[[[[[[[[[Eat_195!=0.000000000000000 | [[[[[[[[Eat_104!=0.000000000000000 | [[[[Eat_11!=0.000000000000000 | [[[[[[[[[[[[Eat_57!=0.000000000000000 | [[[[[[[[[[[[[[[Eat_147!=0.000000000000000 | [[[[[[[[[[[Eat_134!=0.000000000000000 | [[[[[[[[[[[[[[Eat_46!=0.000000000000000 | [[[[[[[[[[[[[[Eat_66!=0.000000000000000 | [[[[[[[Eat_65!=0.000000000000000 | [[[Eat_40!=0.000000000000000 | [[[[[[[Eat_51!=0.000000000000000 | [[[[[[[[[[[[[Eat_127!=0.000000000000000 | [[[[[[[[[[Eat_18!=0.000000000000000 | [[[Eat_178!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[Eat_8!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Eat_99!=0.000000000000000] | Eat_6!=0.000000000000000] | Eat_7!=0.000000000000000] | Eat_194!=0.000000000000000] | Eat_61!=0.000000000000000] | Eat_133!=0.000000000000000] | Eat_50!=0.000000000000000] | Eat_89!=0.000000000000000] | Eat_52!=0.000000000000000] | Eat_38!=0.000000000000000] | Eat_186!=0.000000000000000] | Eat_75!=0.000000000000000] | Eat_27!=0.000000000000000] | Eat_181!=0.000000000000000] | Eat_19!=0.000000000000000] | Eat_164!=0.000000000000000] | Eat_144!=0.000000000000000] | Eat_91!=0.000000000000000] | Eat_13!=0.000000000000000] | Eat_131!=0.000000000000000] | Eat_168!=0.000000000000000] | Eat_169!=0.000000000000000] | Eat_34!=0.000000000000000] | Eat_189!=0.000000000000000] | Eat_114!=0.000000000000000] | Eat_155!=0.000000000000000] | Eat_24!=0.000000000000000] | Eat_188!=0.000000000000000] | Eat_199!=0.000000000000000] | Eat_93!=0.000000000000000] | Eat_109!=0.000000000000000] | Eat_29!=0.000000000000000] | Eat_60!=0.000000000000000] | Eat_146!=0.000000000000000] | Eat_182!=0.000000000000000]] | Eat_148!=0.000000000000000] | Eat_74!=0.000000000000000] | Eat_106!=0.000000000000000] | Eat_105!=0.000000000000000] | Eat_126!=0.000000000000000] | Eat_175!=0.000000000000000] | Eat_78!=0.000000000000000] | Eat_21!=0.000000000000000] | Eat_149!=0.000000000000000] | Eat_197!=0.000000000000000] | Eat_42!=0.000000000000000] | Eat_113!=0.000000000000000] | Eat_136!=0.000000000000000] | Eat_82!=0.000000000000000] | Eat_39!=0.000000000000000] | Eat_68!=0.000000000000000] | Eat_3!=0.000000000000000] | Eat_47!=0.000000000000000]] | Eat_191!=0.000000000000000] | Eat_5!=0.000000000000000]] | Eat_125!=0.000000000000000] | Eat_26!=0.000000000000000] | Eat_55!=0.000000000000000] | Eat_160!=0.000000000000000] | Eat_53!=0.000000000000000] | Eat_137!=0.000000000000000] | Eat_183!=0.000000000000000] | Eat_14!=0.000000000000000] | Eat_111!=0.000000000000000]] | Eat_64!=0.000000000000000] | Eat_132!=0.000000000000000] | Eat_171!=0.000000000000000] | Eat_77!=0.000000000000000] | Eat_200!=0.000000000000000] | Eat_94!=0.000000000000000] | Eat_22!=0.000000000000000] | Eat_117!=0.000000000000000] | Eat_12!=0.000000000000000] | Eat_172!=0.000000000000000] | Eat_17!=0.000000000000000] | Eat_161!=0.000000000000000]] | Eat_157!=0.000000000000000] | Eat_88!=0.000000000000000] | Eat_4!=0.000000000000000] | Eat_23!=0.000000000000000] | Eat_79!=0.000000000000000] | Eat_187!=0.000000000000000]] | Eat_123!=0.000000000000000] | Eat_141!=0.000000000000000]] | Eat_31!=0.000000000000000] | Eat_156!=0.000000000000000] | Eat_100!=0.000000000000000] | Eat_107!=0.000000000000000] | Eat_86!=0.000000000000000] | Eat_87!=0.000000000000000]] | Eat_124!=0.000000000000000] | Eat_45!=0.000000000000000] | Eat_41!=0.000000000000000] | Eat_108!=0.000000000000000] | Eat_37!=0.000000000000000] | Eat_143!=0.000000000000000] | Eat_177!=0.000000000000000] | Eat_49!=0.000000000000000] | Eat_119!=0.000000000000000] | Eat_16!=0.000000000000000] | Eat_98!=0.000000000000000] | Eat_145!=0.000000000000000] | Eat_159!=0.000000000000000]] | Eat_142!=0.000000000000000] | Eat_174!=0.000000000000000] | Eat_120!=0.000000000000000] | Eat_115!=0.000000000000000] | Eat_112!=0.000000000000000] | Eat_20!=0.000000000000000] | Eat_73!=0.000000000000000] | Eat_95!=0.000000000000000] | Eat_63!=0.000000000000000] | Eat_54!=0.000000000000000] | Eat_135!=0.000000000000000] | Eat_44!=0.000000000000000] | Eat_90!=0.000000000000000]] | Eat_192!=0.000000000000000] | Eat_43!=0.000000000000000] | Eat_48!=0.000000000000000] | Eat_56!=0.000000000000000] | Eat_35!=0.000000000000000] | Eat_58!=0.000000000000000] | Eat_190!=0.000000000000000] | Eat_25!=0.000000000000000] | Eat_184!=0.000000000000000] | Eat_96!=0.000000000000000]] | Eat_162!=0.000000000000000] | Eat_33!=0.000000000000000] | Eat_118!=0.000000000000000] | Eat_152!=0.000000000000000] | Eat_85!=0.000000000000000] | Eat_167!=0.000000000000000] | Eat_139!=0.000000000000000] | Eat_102!=0.000000000000000] | Eat_129!=0.000000000000000] | Eat_36!=0.000000000000000] | Eat_15!=0.000000000000000] | Eat_163!=0.000000000000000] | Eat_166!=0.000000000000000] | Eat_1!=0.000000000000000]] | Eat_28!=0.000000000000000] | Eat_116!=0.000000000000000] | Eat_62!=0.000000000000000] | Eat_138!=0.000000000000000] | Eat_103!=0.000000000000000] | Eat_30!=0.000000000000000] | Eat_121!=0.000000000000000] | Eat_84!=0.000000000000000] | Eat_9!=0.000000000000000] | Eat_130!=0.000000000000000] | Eat_196!=0.000000000000000]] | Eat_179!=0.000000000000000] | Eat_158!=0.000000000000000] | Eat_128!=0.000000000000000]] | Eat_71!=0.000000000000000] | Eat_150!=0.000000000000000] | Eat_153!=0.000000000000000] | Eat_140!=0.000000000000000] | Eat_110!=0.000000000000000] | Eat_185!=0.000000000000000] | Eat_32!=0.000000000000000]] | Eat_67!=0.000000000000000] | Eat_70!=0.000000000000000] | Eat_198!=0.000000000000000] | Eat_122!=0.000000000000000] | Eat_83!=0.000000000000000] | Eat_80!=0.000000000000000] | Eat_59!=0.000000000000000] | Eat_180!=0.000000000000000] | Eat_101!=0.000000000000000] | Eat_170!=0.000000000000000] | Eat_2!=0.000000000000000] | Eat_76!=0.000000000000000] | Eat_154!=0.000000000000000] | Eat_72!=0.000000000000000] | Eat_92!=0.000000000000000] | Eat_151!=0.000000000000000]] | Eat_81!=0.000000000000000] | Eat_97!=0.000000000000000] | Eat_193!=0.000000000000000] | Eat_69!=0.000000000000000] | Eat_165!=0.000000000000000] | Eat_176!=0.000000000000000] | [false | 1.000000000000000 normalized: ~ [E [true U ~ [[[Eat_176=0.000000000000000 & [Eat_165=0.000000000000000 & [Eat_69=0.000000000000000 & [Eat_193=0.000000000000000 & [Eat_97=0.000000000000000 & [Eat_81=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_151=0.000000000000000 & [Eat_92=0.000000000000000 & [Eat_72=0.000000000000000 & [Eat_154=0.000000000000000 & [Eat_76=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_170=0.000000000000000 & [Eat_101=0.000000000000000 & [Eat_180=0.000000000000000 & [Eat_59=0.000000000000000 & [Eat_80=0.000000000000000 & [Eat_83=0.000000000000000 & [Eat_122=0.000000000000000 & [Eat_198=0.000000000000000 & [Eat_70=0.000000000000000 & [Eat_67=0.000000000000000 & [Eat_195=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_185=0.000000000000000 & [Eat_110=0.000000000000000 & [Eat_140=0.000000000000000 & [Eat_153=0.000000000000000 & [Eat_150=0.000000000000000 & [Eat_71=0.000000000000000 & [Eat_104=0.000000000000000 & [Eat_128=0.000000000000000 & [Eat_158=0.000000000000000 & [Eat_179=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_196=0.000000000000000 & [Eat_130=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_84=0.000000000000000 & [Eat_121=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_103=0.000000000000000 & [Eat_138=0.000000000000000 & [Eat_62=0.000000000000000 & [Eat_116=0.000000000000000 & [Eat_173=0.000000000000000 & [Eat_28=0.000000000000000 & [Eat_57=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_166=0.000000000000000 & [Eat_163=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_129=0.000000000000000 & [Eat_102=0.000000000000000 & [Eat_139=0.000000000000000 & [Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_40=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_17 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [[[1.000000000000000<=Eat_173 & true] & true] & [[1.000000000000000
-> the formula is FALSE

FORMULA p_33_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_167!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Eat_99!=0.000000000000000] | Eat_6!=0.000000000000000] | Eat_7!=0.000000000000000] | Eat_194!=0.000000000000000] | Eat_61!=0.000000000000000] | Eat_133!=0.000000000000000] | Eat_50!=0.000000000000000] | Eat_89!=0.000000000000000] | Eat_52!=0.000000000000000] | Eat_38!=0.000000000000000] | Eat_186!=0.000000000000000] | Eat_75!=0.000000000000000] | Eat_27!=0.000000000000000] | Eat_181!=0.000000000000000] | Eat_19!=0.000000000000000] | Eat_164!=0.000000000000000] | Eat_144!=0.000000000000000] | Eat_91!=0.000000000000000] | Eat_13!=0.000000000000000] | Eat_131!=0.000000000000000] | Eat_168!=0.000000000000000] | Eat_169!=0.000000000000000] | Eat_34!=0.000000000000000] | Eat_189!=0.000000000000000] | Eat_114!=0.000000000000000] | Eat_155!=0.000000000000000] | Eat_24!=0.000000000000000] | Eat_188!=0.000000000000000] | Eat_199!=0.000000000000000] | Eat_93!=0.000000000000000] | Eat_109!=0.000000000000000] | Eat_29!=0.000000000000000] | Eat_60!=0.000000000000000] | Eat_146!=0.000000000000000] | Eat_182!=0.000000000000000] | Eat_8!=0.000000000000000] | Eat_148!=0.000000000000000] | Eat_74!=0.000000000000000] | Eat_106!=0.000000000000000] | Eat_105!=0.000000000000000] | Eat_126!=0.000000000000000] | Eat_175!=0.000000000000000] | Eat_78!=0.000000000000000] | Eat_21!=0.000000000000000] | Eat_149!=0.000000000000000] | Eat_197!=0.000000000000000] | Eat_42!=0.000000000000000] | Eat_113!=0.000000000000000] | Eat_136!=0.000000000000000] | Eat_82!=0.000000000000000] | Eat_39!=0.000000000000000] | Eat_68!=0.000000000000000] | Eat_3!=0.000000000000000] | Eat_47!=0.000000000000000] | Eat_178!=0.000000000000000] | Eat_191!=0.000000000000000] | Eat_5!=0.000000000000000] | Eat_18!=0.000000000000000] | Eat_125!=0.000000000000000] | Eat_26!=0.000000000000000] | Eat_55!=0.000000000000000] | Eat_160!=0.000000000000000] | Eat_53!=0.000000000000000] | Eat_137!=0.000000000000000] | Eat_183!=0.000000000000000] | Eat_14!=0.000000000000000] | Eat_111!=0.000000000000000] | Eat_127!=0.000000000000000] | Eat_64!=0.000000000000000] | Eat_132!=0.000000000000000] | Eat_171!=0.000000000000000] | Eat_77!=0.000000000000000] | Eat_200!=0.000000000000000] | Eat_94!=0.000000000000000] | Eat_22!=0.000000000000000] | Eat_117!=0.000000000000000] | Eat_12!=0.000000000000000] | Eat_172!=0.000000000000000] | Eat_17!=0.000000000000000] | Eat_161!=0.000000000000000] | Eat_51!=0.000000000000000] | Eat_157!=0.000000000000000] | Eat_88!=0.000000000000000] | Eat_4!=0.000000000000000] | Eat_23!=0.000000000000000] | Eat_79!=0.000000000000000] | Eat_187!=0.000000000000000] | Eat_40!=0.000000000000000] | Eat_123!=0.000000000000000] | Eat_141!=0.000000000000000] | Eat_65!=0.000000000000000] | Eat_31!=0.000000000000000] | Eat_156!=0.000000000000000] | Eat_100!=0.000000000000000] | Eat_107!=0.000000000000000] | Eat_86!=0.000000000000000] | Eat_87!=0.000000000000000] | Eat_66!=0.000000000000000] | Eat_124!=0.000000000000000] | Eat_45!=0.000000000000000] | Eat_41!=0.000000000000000] | Eat_108!=0.000000000000000] | Eat_37!=0.000000000000000] | Eat_143!=0.000000000000000] | Eat_177!=0.000000000000000] | Eat_49!=0.000000000000000] | Eat_119!=0.000000000000000] | Eat_16!=0.000000000000000] | Eat_98!=0.000000000000000] | Eat_145!=0.000000000000000] | Eat_159!=0.000000000000000] | Eat_46!=0.000000000000000] | Eat_142!=0.000000000000000] | Eat_174!=0.000000000000000] | Eat_120!=0.000000000000000] | Eat_115!=0.000000000000000] | Eat_112!=0.000000000000000] | Eat_20!=0.000000000000000] | Eat_73!=0.000000000000000] | Eat_95!=0.000000000000000] | Eat_63!=0.000000000000000] | Eat_54!=0.000000000000000] | Eat_135!=0.000000000000000] | Eat_44!=0.000000000000000] | Eat_90!=0.000000000000000] | Eat_134!=0.000000000000000] | Eat_192!=0.000000000000000] | Eat_43!=0.000000000000000] | Eat_48!=0.000000000000000] | Eat_56!=0.000000000000000] | Eat_35!=0.000000000000000] | Eat_58!=0.000000000000000] | Eat_190!=0.000000000000000] | Eat_25!=0.000000000000000] | Eat_184!=0.000000000000000] | Eat_96!=0.000000000000000] | Eat_147!=0.000000000000000] | Eat_162!=0.000000000000000] | Eat_33!=0.000000000000000] | Eat_118!=0.000000000000000] | Eat_152!=0.000000000000000] | Eat_85!=0.000000000000000]] | Eat_139!=0.000000000000000] | Eat_102!=0.000000000000000] | Eat_129!=0.000000000000000] | Eat_36!=0.000000000000000] | Eat_15!=0.000000000000000] | Eat_163!=0.000000000000000] | Eat_166!=0.000000000000000] | Eat_1!=0.000000000000000] | Eat_57!=0.000000000000000] | Eat_28!=0.000000000000000] | Eat_116!=0.000000000000000] | Eat_62!=0.000000000000000] | Eat_138!=0.000000000000000] | Eat_103!=0.000000000000000] | Eat_30!=0.000000000000000] | Eat_121!=0.000000000000000] | Eat_84!=0.000000000000000] | Eat_9!=0.000000000000000] | Eat_130!=0.000000000000000] | Eat_196!=0.000000000000000] | Eat_11!=0.000000000000000] | Eat_179!=0.000000000000000] | Eat_158!=0.000000000000000] | Eat_128!=0.000000000000000] | Eat_104!=0.000000000000000] | Eat_71!=0.000000000000000] | Eat_150!=0.000000000000000] | Eat_153!=0.000000000000000] | Eat_140!=0.000000000000000] | Eat_110!=0.000000000000000] | Eat_185!=0.000000000000000] | Eat_32!=0.000000000000000] | Eat_195!=0.000000000000000] | Eat_67!=0.000000000000000] | Eat_70!=0.000000000000000] | Eat_198!=0.000000000000000] | Eat_122!=0.000000000000000] | Eat_83!=0.000000000000000] | Eat_80!=0.000000000000000] | Eat_59!=0.000000000000000] | Eat_180!=0.000000000000000] | Eat_101!=0.000000000000000] | Eat_170!=0.000000000000000] | Eat_2!=0.000000000000000] | Eat_76!=0.000000000000000] | Eat_154!=0.000000000000000] | Eat_72!=0.000000000000000] | Eat_92!=0.000000000000000] | Eat_151!=0.000000000000000] | Eat_10!=0.000000000000000] | Eat_81!=0.000000000000000] | Eat_97!=0.000000000000000] | Eat_193!=0.000000000000000] | Eat_69!=0.000000000000000] | Eat_165!=0.000000000000000] | Eat_176!=0.000000000000000] | [false | 1.000000000000000 normalized: ~ [E [true U ~ [[~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_167=0.000000000000000 & [Eat_85=0.000000000000000 & [Eat_152=0.000000000000000 & [Eat_118=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_162=0.000000000000000 & [Eat_147=0.000000000000000 & [Eat_96=0.000000000000000 & [Eat_184=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_190=0.000000000000000 & [Eat_58=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_56=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_192=0.000000000000000 & [Eat_134=0.000000000000000 & [Eat_90=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_135=0.000000000000000 & [Eat_54=0.000000000000000 & [Eat_63=0.000000000000000 & [Eat_95=0.000000000000000 & [Eat_73=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_112=0.000000000000000 & [Eat_115=0.000000000000000 & [Eat_120=0.000000000000000 & [Eat_174=0.000000000000000 & [Eat_142=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_159=0.000000000000000 & [Eat_145=0.000000000000000 & [Eat_98=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_119=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_177=0.000000000000000 & [Eat_143=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_108=0.000000000000000 & [Eat_41=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_124=0.000000000000000 & [Eat_66=0.000000000000000 & [Eat_87=0.000000000000000 & [Eat_86=0.000000000000000 & [Eat_107=0.000000000000000 & [Eat_100=0.000000000000000 & [Eat_156=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_65=0.000000000000000 & [Eat_141=0.000000000000000 & [Eat_123=0.000000000000000 & [Eat_40=0.000000000000000 & [Eat_187=0.000000000000000 & [Eat_79=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_88=0.000000000000000 & [Eat_157=0.000000000000000 & [Eat_51=0.000000000000000 & [Eat_161=0.000000000000000 & [Eat_172=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_117=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_94=0.000000000000000 & [Eat_200=0.000000000000000 & [Eat_77=0.000000000000000 & [Eat_171=0.000000000000000 & [Eat_132=0.000000000000000 & [Eat_64=0.000000000000000 & [Eat_127=0.000000000000000 & [Eat_111=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_183=0.000000000000000 & [Eat_137=0.000000000000000 & [Eat_53=0.000000000000000 & [Eat_160=0.000000000000000 & [Eat_55=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_125=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_191=0.000000000000000 & [Eat_178=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_68=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_82=0.000000000000000 & [Eat_136=0.000000000000000 & [Eat_113=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_197=0.000000000000000 & [Eat_149=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_78=0.000000000000000 & [Eat_175=0.000000000000000 & [Eat_126=0.000000000000000 & [Eat_105=0.000000000000000 & [Eat_106=0.000000000000000 & [Eat_74=0.000000000000000 & [Eat_148=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_182=0.000000000000000 & [Eat_146=0.000000000000000 & [Eat_60=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_109=0.000000000000000 & [Eat_93=0.000000000000000 & [Eat_199=0.000000000000000 & [Eat_188=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_155=0.000000000000000 & [Eat_114=0.000000000000000 & [Eat_189=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_169=0.000000000000000 & [Eat_168=0.000000000000000 & [Eat_131=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_91=0.000000000000000 & [Eat_144=0.000000000000000 & [Eat_164=0.000000000000000 & [Eat_19=0.000000000000000 & [Eat_181=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_75=0.000000000000000 & [Eat_186=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_52=0.000000000000000 & [Eat_89=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_133=0.000000000000000 & [Eat_61=0.000000000000000 & [Eat_194=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_99=0.000000000000000 & [1.000000000000000=Eat_17 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Eat_139=0.000000000000000] & Eat_102=0.000000000000000] & Eat_129=0.000000000000000] & Eat_36=0.000000000000000] & Eat_15=0.000000000000000] & Eat_163=0.000000000000000] & Eat_166=0.000000000000000] & Eat_1=0.000000000000000] & Eat_57=0.000000000000000] & Eat_28=0.000000000000000] & Eat_173=0.000000000000000] & Eat_116=0.000000000000000] & Eat_62=0.000000000000000] & Eat_138=0.000000000000000] & Eat_103=0.000000000000000] & Eat_30=0.000000000000000] & Eat_121=0.000000000000000] & Eat_84=0.000000000000000] & Eat_9=0.000000000000000] & Eat_130=0.000000000000000] & Eat_196=0.000000000000000] & Eat_11=0.000000000000000] & Eat_179=0.000000000000000] & Eat_158=0.000000000000000] & Eat_128=0.000000000000000] & Eat_104=0.000000000000000] & Eat_71=0.000000000000000] & Eat_150=0.000000000000000] & Eat_153=0.000000000000000] & Eat_140=0.000000000000000] & Eat_110=0.000000000000000] & Eat_185=0.000000000000000] & Eat_32=0.000000000000000] & Eat_195=0.000000000000000] & Eat_67=0.000000000000000] & Eat_70=0.000000000000000] & Eat_198=0.000000000000000] & Eat_122=0.000000000000000] & Eat_83=0.000000000000000] & Eat_80=0.000000000000000] & Eat_59=0.000000000000000] & Eat_180=0.000000000000000] & Eat_101=0.000000000000000] & Eat_170=0.000000000000000] & Eat_2=0.000000000000000] & Eat_76=0.000000000000000] & Eat_154=0.000000000000000] & Eat_72=0.000000000000000] & Eat_92=0.000000000000000] & Eat_151=0.000000000000000] & Eat_10=0.000000000000000] & Eat_81=0.000000000000000] & Eat_97=0.000000000000000] & Eat_193=0.000000000000000] & Eat_69=0.000000000000000] & Eat_165=0.000000000000000] & Eat_176=0.000000000000000]] & [[[true & 1.000000000000000<=Eat_173] & true] & [[false | 1.000000000000000
-> the formula is FALSE

FORMULA p_34_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m19sec

STOP 1369705487

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

1496 1940 4292 4465
iterations count:4592 (4), effective:600 (0)

initing FirstDep: 0m0sec

5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)
5180
iterations count:1000 (1), effective:0 (0)

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