Introduction

This page shows the outputs produced by the execution of marcie on Philosophers/000200 (P/T). We provide:

A short summary,
the execution chart (evolution of CPU and memory over the execution),
the sequence of actions to be executed by the VM,
the results of these actions.

About the Execution

Execution Summary
Memory (MB)	CPU (s)	End
735.54	8.92	normal

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

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

START 1369698890

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=ReachabilityPlaceComparison.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: 0m3sec

-> 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 [[[[Think_9=Catch1_9 & [[[Think_138=Catch1_138 & [Think_90=Catch1_90 & [[Think_82=Catch1_82 & [[Think_57=Catch1_57 & [[Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [[Think_160=Catch1_160 & [Think_34=Catch1_34 & [[[Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [[Think_12=Catch1_12 & [[Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [[Think_156=Catch1_156 & [[Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [[[Think_106=Catch1_106 & [[Think_14=Catch1_14 & [[[[Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [[[[Think_110=Catch1_110 & [[[[Think_20=Catch1_20 & [Think_88=Catch1_88 & [[Think_103=Catch1_103 & [[Think_150=Catch1_150 & [[Think_76=Catch1_76 & [[Think_28=Catch1_28 & [[Think_149=Catch1_149 & [[[Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [[[Think_155=Catch1_155 & [[[[Think_178=Catch1_178 & [[Think_54=Catch1_54 & [Think_96=Catch1_96 & [[Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [[Think_122=Catch1_122 & [[[Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [[[[Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [[Think_129=Catch1_129 & [Think_167=Catch1_167 & [[Think_120=Catch1_120 & [Think_92=Catch1_92 & [[Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [[Think_118=Catch1_118 & [[Think_62=Catch1_62 & [[Think_5=Catch1_5 & [Think_79=Catch1_79 & [[Think_186=Catch1_186 & [[Think_43=Catch1_43 & [[[[Think_38=Catch1_38 & [Think_74=Catch1_74 & [[Think_141=Catch1_141 & [[[[Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [[Think_177=Catch1_177 & [Think_104=Catch1_104 & [[[[Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [[Think_190=Catch1_190 & [[[[Think_102=Catch1_102 & [[Think_115=Catch1_115 & [[[Think_65=Catch1_65 & [Think_86=Catch1_86 & [[[Think_135=Catch1_135 & [Think_183=Catch1_183 & [[[[Think_21=Catch1_21 & [[[Think_113=Catch1_113 & [[Think_116=Catch1_116 & [[Think_95=Catch1_95 & [[[Think_44=Catch1_44 & [[[[Think_148=Catch1_148 & [Think_85=Catch1_85 & [[[[Think_39=Catch1_39 & [[[[[true & Think_130=Catch1_130] & Think_78=Catch1_78] & Think_161=Catch1_161] & Think_66=Catch1_66] & Think_77=Catch1_77]] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125]]] & Think_15=Catch1_15] & Think_83=Catch1_83] & Think_159=Catch1_159]] & Think_55=Catch1_55] & Think_64=Catch1_64]] & Think_7=Catch1_7]] & Think_136=Catch1_136]] & Think_200=Catch1_200] & Think_68=Catch1_68]] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42]]] & Think_36=Catch1_36] & Think_25=Catch1_25]]] & Think_16=Catch1_16] & Think_163=Catch1_163]] & Think_73=Catch1_73]] & Think_114=Catch1_114] & Think_23=Catch1_23] & Think_108=Catch1_108]] & Think_80=Catch1_80]]]]]] & Think_33=Catch1_33] & Think_22=Catch1_22] & Think_187=Catch1_187]]] & Think_191=Catch1_191]]]] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71]] & Think_193=Catch1_193]]] & Think_51=Catch1_51] & Think_59=Catch1_59] & Think_188=Catch1_188]] & Think_56=Catch1_56]] & Think_32=Catch1_32]]] & Think_173=Catch1_173]] & Think_26=Catch1_26]] & Think_63=Catch1_63]]]]]]]]]] & Think_175=Catch1_175]]] & Think_89=Catch1_89]]] & Think_196=Catch1_196]]]]]] & Think_124=Catch1_124] & Think_45=Catch1_45] & Think_153=Catch1_153]]]] & Think_3=Catch1_3] & Think_81=Catch1_81]] & Think_117=Catch1_117]]]]]]] & Think_197=Catch1_197]]] & Think_164=Catch1_164]] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58]] & Think_184=Catch1_184] & Think_170=Catch1_170]]]] & Think_181=Catch1_181] & Think_30=Catch1_30]] & Think_142=Catch1_142]] & Think_194=Catch1_194]] & Think_10=Catch1_10]] & Think_40=Catch1_40]] & Think_91=Catch1_91]]] & Think_101=Catch1_101] & Think_100=Catch1_100] & Think_48=Catch1_48]] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152]]]] & Think_182=Catch1_182] & Think_72=Catch1_72] & Think_128=Catch1_128]] & Think_199=Catch1_199]] & Think_154=Catch1_154] & Think_18=Catch1_18]]]] & Think_189=Catch1_189]] & Think_123=Catch1_123]]]]]] & Think_146=Catch1_146]] & Think_145=Catch1_145]]]] & Think_131=Catch1_131] & Think_6=Catch1_6]]] & Think_11=Catch1_11]]]]]] & Think_111=Catch1_111]] & Think_134=Catch1_134]] & Think_144=Catch1_144]]] & Think_168=Catch1_168] & Think_121=Catch1_121]] & Think_127=Catch1_127] & [[[[[[[[[[[Eat_136!=Catch1_136 & [[[[[[[[[[[[Eat_29!=Catch1_29 & [[[Eat_144!=Catch1_144 & [[[[[[[[[Eat_70!=Catch1_70 & [[[[[[[[[[[[[[[Eat_80!=Catch1_80 & [[[[[[Eat_119!=Catch1_119 & [[[[[[[[[Eat_99!=Catch1_99 & [[[Eat_42!=Catch1_42 & [[[Eat_85!=Catch1_85 & [[[Eat_19!=Catch1_19 & [[[Eat_163!=Catch1_163 & [[[Eat_124!=Catch1_124 & [[[[[[[[[[[[[[[Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [[Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [[[[[[[[[[[Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [[Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [[[Eat_60!=Catch1_60 & [[Eat_150!=Catch1_150 & [[[[[[[[[[[[[Eat_166!=Catch1_166 & [[[[[[[Eat_111!=Catch1_111 & [[Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [[Eat_61!=Catch1_61 & [[[[[Eat_121!=Catch1_121 & [[Eat_53!=Catch1_53 & [[[[[[[[[[[[[[Eat_137!=Catch1_137 & [[[[Eat_190!=Catch1_190 & [[[[[[Eat_183!=Catch1_183 & [[[[[[Eat_153!=Catch1_153 & [[[Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [[Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [[Eat_147!=Catch1_147 & [[Eat_62!=Catch1_62 & true] & Eat_67!=Catch1_67]] & Eat_142!=Catch1_142]]]]]]]]] & Eat_49!=Catch1_49]]]] & Eat_107!=Catch1_107] & Eat_174!=Catch1_174]] & Eat_91!=Catch1_91] & Eat_109!=Catch1_109] & Eat_68!=Catch1_68] & Eat_200!=Catch1_200] & Eat_195!=Catch1_195]] & Eat_7!=Catch1_7] & Eat_164!=Catch1_164] & Eat_45!=Catch1_45] & Eat_2!=Catch1_2] & Eat_191!=Catch1_191]] & Eat_37!=Catch1_37] & Eat_96!=Catch1_96] & Eat_138!=Catch1_138]] & Eat_181!=Catch1_181] & Eat_170!=Catch1_170] & Eat_127!=Catch1_127] & Eat_24!=Catch1_24] & Eat_162!=Catch1_162] & Eat_69!=Catch1_69] & Eat_139!=Catch1_139] & Eat_198!=Catch1_198] & Eat_87!=Catch1_87] & Eat_172!=Catch1_172] & Eat_4!=Catch1_4] & Eat_14!=Catch1_14] & Eat_113!=Catch1_113]] & Eat_92!=Catch1_92]] & Eat_184!=Catch1_184] & Eat_5!=Catch1_5] & Eat_86!=Catch1_86] & Eat_11!=Catch1_11]] & Eat_168!=Catch1_168]]] & Eat_44!=Catch1_44]] & Eat_64!=Catch1_64] & Eat_100!=Catch1_100] & Eat_101!=Catch1_101] & Eat_120!=Catch1_120] & Eat_20!=Catch1_20] & Eat_46!=Catch1_46]] & Eat_89!=Catch1_89] & Eat_50!=Catch1_50] & Eat_98!=Catch1_98] & Eat_131!=Catch1_131] & Eat_132!=Catch1_132] & Eat_17!=Catch1_17] & Eat_106!=Catch1_106] & Eat_156!=Catch1_156] & Eat_178!=Catch1_178] & Eat_47!=Catch1_47] & Eat_71!=Catch1_71] & Eat_21!=Catch1_21]] & Eat_160!=Catch1_160]] & Eat_48!=Catch1_48] & Eat_72!=Catch1_72]]] & Eat_128!=Catch1_128]]]] & Eat_140!=Catch1_140] & Eat_152!=Catch1_152] & Eat_141!=Catch1_141] & Eat_12!=Catch1_12] & Eat_123!=Catch1_123] & Eat_93!=Catch1_93] & Eat_143!=Catch1_143] & Eat_56!=Catch1_56] & Eat_75!=Catch1_75] & Eat_16!=Catch1_16]]] & Eat_114!=Catch1_114]]] & Eat_197!=Catch1_197] & Eat_81!=Catch1_81] & Eat_159!=Catch1_159] & Eat_32!=Catch1_32] & Eat_36!=Catch1_36] & Eat_192!=Catch1_192] & Eat_13!=Catch1_13] & Eat_165!=Catch1_165] & Eat_194!=Catch1_194] & Eat_25!=Catch1_25] & Eat_185!=Catch1_185] & Eat_23!=Catch1_23] & Eat_105!=Catch1_105] & Eat_145!=Catch1_145]] & Eat_180!=Catch1_180] & Eat_102!=Catch1_102]] & Eat_41!=Catch1_41] & Eat_134!=Catch1_134]] & Eat_94!=Catch1_94] & Eat_108!=Catch1_108]] & Eat_110!=Catch1_110] & Eat_118!=Catch1_118]] & Eat_149!=Catch1_149] & Eat_28!=Catch1_28]] & Eat_30!=Catch1_30] & Eat_199!=Catch1_199] & Eat_31!=Catch1_31] & Eat_135!=Catch1_135] & Eat_103!=Catch1_103] & Eat_90!=Catch1_90] & Eat_34!=Catch1_34] & Eat_167!=Catch1_167]] & Eat_82!=Catch1_82] & Eat_52!=Catch1_52] & Eat_40!=Catch1_40] & Eat_133!=Catch1_133] & Eat_173!=Catch1_173]] & Eat_112!=Catch1_112] & Eat_79!=Catch1_79] & Eat_57!=Catch1_57] & Eat_161!=Catch1_161] & Eat_186!=Catch1_186] & Eat_65!=Catch1_65] & Eat_146!=Catch1_146] & Eat_76!=Catch1_76] & Eat_51!=Catch1_51] & Eat_154!=Catch1_154] & Eat_193!=Catch1_193] & Eat_1!=Catch1_1] & Eat_117!=Catch1_117] & Eat_177!=Catch1_177]] & Eat_26!=Catch1_26] & Eat_78!=Catch1_78] & Eat_43!=Catch1_43] & Eat_18!=Catch1_18] & Eat_126!=Catch1_126] & Eat_189!=Catch1_189] & Eat_104!=Catch1_104] & Eat_179!=Catch1_179]] & Eat_175!=Catch1_175] & Eat_27!=Catch1_27]] & Eat_63!=Catch1_63] & Eat_38!=Catch1_38] & Eat_97!=Catch1_97] & Eat_9!=Catch1_9] & Eat_84!=Catch1_84] & Eat_158!=Catch1_158] & Eat_196!=Catch1_196] & Eat_35!=Catch1_35] & Eat_116!=Catch1_116] & Eat_15!=Catch1_15] & Eat_187!=Catch1_187]] & Eat_33!=Catch1_33] & Eat_66!=Catch1_66] & Eat_59!=Catch1_59] & Eat_130!=Catch1_130] & Eat_73!=Catch1_73] & Eat_22!=Catch1_22] & Eat_55!=Catch1_55] & Eat_169!=Catch1_169] & Eat_95!=Catch1_95] & Eat_58!=Catch1_58]]]
normalized: ~ [E [true U ~ [[[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_7_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m2sec

checking: AG [[[[Think_9=Catch1_9 & [[[Think_138=Catch1_138 & [[[[[Think_57=Catch1_57 & [[[[[[Think_19=Catch1_19 & [[[[[[[[[Think_145=Catch1_145 & [Think_12=Catch1_12 & [[[Think_157=Catch1_157 & [[Think_52=Catch1_52 & [Think_75=Catch1_75 & [[[[[Think_61=Catch1_61 & [[Think_18=Catch1_18 & [[[[Think_14=Catch1_14 & [Think_128=Catch1_128 & [[[[[Think_195=Catch1_195 & [[[[[[Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [[[[[[Think_10=Catch1_10 & [[[[Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [[[[Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [[[[Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [[[[Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [[[[Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [[[[Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [[[[Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [[[[Think_89=Catch1_89 & [[[[[Think_70=Catch1_70 & [Think_98=Catch1_98 & [[[Think_162=Catch1_162 & [[Think_37=Catch1_37 & [Think_99=Catch1_99 & [[[Think_26=Catch1_26 & [Think_62=Catch1_62 & [[[Think_79=Catch1_79 & [Think_32=Catch1_32 & [[[[[[[[[[[Think_71=Catch1_71 & [[[[[[[[[[[Think_33=Catch1_33 & [[Think_53=Catch1_53 & [Think_140=Catch1_140 & [[[Think_80=Catch1_80 & [[[Think_23=Catch1_23 & [[[Think_73=Catch1_73 & [Think_115=Catch1_115 & [[[Think_65=Catch1_65 & [Think_86=Catch1_86 & [[[[[[[[Think_21=Catch1_21 & [[[[Think_136=Catch1_136 & [[[[[[Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [[Think_148=Catch1_148 & [[[[[[[Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]] & Think_77=Catch1_77] & Think_39=Catch1_39] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85]] & Think_15=Catch1_15]]]] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95] & Think_7=Catch1_7] & Think_116=Catch1_116]] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68]] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36] & Think_25=Catch1_25]]] & Think_16=Catch1_16] & Think_163=Catch1_163]]] & Think_102=Catch1_102] & Think_114=Catch1_114]] & Think_108=Catch1_108] & Think_190=Catch1_190]] & Think_13=Catch1_13] & Think_41=Catch1_41]]] & Think_179=Catch1_179]] & Think_22=Catch1_22] & Think_187=Catch1_187] & Think_104=Catch1_104] & Think_177=Catch1_177] & Think_191=Catch1_191] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84] & Think_185=Catch1_185]] & Think_141=Catch1_141] & Think_193=Catch1_193] & Think_74=Catch1_74] & Think_38=Catch1_38] & Think_51=Catch1_51] & Think_59=Catch1_59] & Think_188=Catch1_188] & Think_43=Catch1_43] & Think_56=Catch1_56] & Think_186=Catch1_186]]] & Think_5=Catch1_5] & Think_173=Catch1_173]]] & Think_118=Catch1_118] & Think_63=Catch1_63]]] & Think_60=Catch1_60]] & Think_166=Catch1_166] & Think_93=Catch1_93]]] & Think_4=Catch1_4] & Think_175=Catch1_175] & Think_92=Catch1_92] & Think_120=Catch1_120]] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196]]]] & Think_133=Catch1_133] & Think_49=Catch1_49] & Think_124=Catch1_124]]]] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3]]]] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180]]]] & Think_197=Catch1_197] & Think_96=Catch1_96] & Think_54=Catch1_54]]]] & Think_174=Catch1_174] & Think_58=Catch1_58] & Think_155=Catch1_155]]]] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181]]]] & Think_28=Catch1_28] & Think_194=Catch1_194] & Think_76=Catch1_76]] & Think_150=Catch1_150] & Think_40=Catch1_40] & Think_103=Catch1_103] & Think_91=Catch1_91] & Think_88=Catch1_88]]]] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152]] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72]]] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154]] & Think_46=Catch1_46]] & Think_143=Catch1_143] & Think_189=Catch1_189] & Think_156=Catch1_156] & Think_123=Catch1_123]]] & Think_198=Catch1_198]] & Think_112=Catch1_112] & Think_146=Catch1_146]]] & Think_172=Catch1_172] & Think_87=Catch1_87] & Think_1=Catch1_1] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34] & Think_160=Catch1_160] & Think_11=Catch1_11]] & Think_139=Catch1_139] & Think_50=Catch1_50] & Think_2=Catch1_2] & Think_17=Catch1_17] & Think_111=Catch1_111]] & Think_134=Catch1_134] & Think_82=Catch1_82] & Think_144=Catch1_144] & Think_90=Catch1_90]] & Think_168=Catch1_168] & Think_121=Catch1_121]] & Think_127=Catch1_127] | [[[[[[[[[[[[[Eat_15!=Catch1_15 & [[Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [[Eat_9!=Catch1_9 & [[[[Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [[[[[[[[[[[[Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [[[Eat_154!=Catch1_154 & [[Eat_76!=Catch1_76 & [[Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [[[[[Eat_80!=Catch1_80 & [[[[[Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [[[Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [[[[[[Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [[[[[[[Eat_102!=Catch1_102 & [[[[Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [[Eat_25!=Catch1_25 & [[[Eat_13!=Catch1_13 & [[[[Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [[[[Eat_114!=Catch1_114 & [[Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [[[Eat_143!=Catch1_143 & [[[[[[[[Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [[Eat_157!=Catch1_157 & [[Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [[Eat_156!=Catch1_156 & [[Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [[Eat_20!=Catch1_20 & [[Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [[Eat_61!=Catch1_61 & [[Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [[Eat_4!=Catch1_4 & [[Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [[Eat_181!=Catch1_181 & [[Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [[[[[Eat_183!=Catch1_183 & [[[Eat_68!=Catch1_68 & [[[[[[[[[Eat_49!=Catch1_49 & [[[[Eat_83!=Catch1_83 & [[[[[[Eat_147!=Catch1_147 & [[true & Eat_62!=Catch1_62] & Eat_67!=Catch1_67]] & Eat_142!=Catch1_142] & Eat_188!=Catch1_188] & Eat_182!=Catch1_182] & Eat_125!=Catch1_125] & Eat_10!=Catch1_10]] & Eat_171!=Catch1_171] & Eat_77!=Catch1_77] & Eat_6!=Catch1_6]] & Eat_176!=Catch1_176] & Eat_129!=Catch1_129] & Eat_148!=Catch1_148] & Eat_107!=Catch1_107] & Eat_174!=Catch1_174] & Eat_153!=Catch1_153] & Eat_91!=Catch1_91] & Eat_109!=Catch1_109]] & Eat_200!=Catch1_200] & Eat_195!=Catch1_195]] & Eat_7!=Catch1_7] & Eat_164!=Catch1_164] & Eat_45!=Catch1_45] & Eat_2!=Catch1_2]]]]]] & Eat_137!=Catch1_137]] & Eat_170!=Catch1_170]]]]]]]] & Eat_172!=Catch1_172]] & Eat_14!=Catch1_14]]]]]]]] & Eat_11!=Catch1_11]] & Eat_168!=Catch1_168]]]]]]]] & Eat_120!=Catch1_120]] & Eat_46!=Catch1_46]]]]]]]] & Eat_106!=Catch1_106]] & Eat_178!=Catch1_178]]]]]]]] & Eat_72!=Catch1_72]] & Eat_74!=Catch1_74]]]] & Eat_122!=Catch1_122] & Eat_140!=Catch1_140] & Eat_152!=Catch1_152] & Eat_141!=Catch1_141] & Eat_12!=Catch1_12] & Eat_123!=Catch1_123] & Eat_93!=Catch1_93]] & Eat_56!=Catch1_56] & Eat_75!=Catch1_75]]] & Eat_88!=Catch1_88]] & Eat_151!=Catch1_151] & Eat_115!=Catch1_115] & Eat_197!=Catch1_197]]] & Eat_32!=Catch1_32] & Eat_36!=Catch1_36] & Eat_192!=Catch1_192]] & Eat_165!=Catch1_165] & Eat_194!=Catch1_194]] & Eat_185!=Catch1_185]]] & Eat_145!=Catch1_145] & Eat_124!=Catch1_124] & Eat_180!=Catch1_180]] & Eat_163!=Catch1_163] & Eat_41!=Catch1_41] & Eat_134!=Catch1_134] & Eat_19!=Catch1_19] & Eat_94!=Catch1_94] & Eat_108!=Catch1_108]]]]]]] & Eat_99!=Catch1_99] & Eat_30!=Catch1_30] & Eat_199!=Catch1_199] & Eat_31!=Catch1_31] & Eat_135!=Catch1_135]]] & Eat_34!=Catch1_34] & Eat_167!=Catch1_167]]] & Eat_52!=Catch1_52] & Eat_40!=Catch1_40] & Eat_133!=Catch1_133] & Eat_173!=Catch1_173]] & Eat_112!=Catch1_112] & Eat_79!=Catch1_79] & Eat_57!=Catch1_57] & Eat_161!=Catch1_161]]] & Eat_146!=Catch1_146]] & Eat_51!=Catch1_51]] & Eat_193!=Catch1_193] & Eat_1!=Catch1_1]]] & Eat_70!=Catch1_70] & Eat_26!=Catch1_26] & Eat_78!=Catch1_78] & Eat_43!=Catch1_43] & Eat_18!=Catch1_18] & Eat_126!=Catch1_126] & Eat_189!=Catch1_189] & Eat_104!=Catch1_104] & Eat_179!=Catch1_179] & Eat_144!=Catch1_144] & Eat_175!=Catch1_175]]] & Eat_63!=Catch1_63] & Eat_38!=Catch1_38] & Eat_97!=Catch1_97]] & Eat_84!=Catch1_84]]]] & Eat_116!=Catch1_116]] & Eat_187!=Catch1_187] & Eat_136!=Catch1_136] & Eat_33!=Catch1_33] & Eat_66!=Catch1_66] & Eat_59!=Catch1_59] & Eat_130!=Catch1_130] & Eat_73!=Catch1_73] & Eat_22!=Catch1_22] & Eat_55!=Catch1_55] & Eat_169!=Catch1_169] & Eat_95!=Catch1_95] & Eat_58!=Catch1_58]]]
normalized: ~ [E [true U ~ [[[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_8_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Think_9=Catch1_9 & [[[[Think_90=Catch1_90 & [[[[Think_57=Catch1_57 & [[[[Think_50=Catch1_50 & [[[[Think_160=Catch1_160 & [[[[Think_1=Catch1_1 & [[[[Think_12=Catch1_12 & [[[[Think_198=Catch1_198 & [[[[Think_156=Catch1_156 & [[[[Think_46=Catch1_46 & [[[[Think_199=Catch1_199 & [[[[Think_182=Catch1_182 & [[[[Think_152=Catch1_152 & [[[[Think_48=Catch1_48 & [[[[Think_88=Catch1_88 & [[[[Think_150=Catch1_150 & [[[[Think_28=Catch1_28 & [[[[Think_181=Catch1_181 & [[[Think_158=Catch1_158 & [Think_170=Catch1_170 & [[[Think_58=Catch1_58 & [[[[[Think_54=Catch1_54 & [[[Think_176=Catch1_176 & [Think_137=Catch1_137 & [[[[[[[[Think_3=Catch1_3 & [Think_109=Catch1_109 & [[[[[Think_124=Catch1_124 & [[[[Think_97=Catch1_97 & [[[[[[[[[Think_4=Catch1_4 & [[[[[[[[[[[Think_26=Catch1_26 & [[[[Think_79=Catch1_79 & [Think_32=Catch1_32 & [[[[[Think_59=Catch1_59 & [Think_51=Catch1_51 & [[[[[[Think_185=Catch1_185 & [[[[[Think_191=Catch1_191 & [Think_177=Catch1_177 & [[[[Think_33=Catch1_33 & [[[[[[[[Think_108=Catch1_108 & [[[Think_102=Catch1_102 & [[[[[[[Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [[[[[[[[[Think_116=Catch1_116 & [[[[[Think_44=Catch1_44 & [[Think_83=Catch1_83 & [Think_15=Catch1_15 & [[[[[[Think_39=Catch1_39 & [[[[[true & Think_130=Catch1_130] & Think_78=Catch1_78] & Think_161=Catch1_161] & Think_66=Catch1_66] & Think_77=Catch1_77]] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148]]] & Think_159=Catch1_159]] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95] & Think_7=Catch1_7]] & Think_136=Catch1_136] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68] & Think_21=Catch1_21] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42]]]]] & Think_86=Catch1_86] & Think_65=Catch1_65] & Think_16=Catch1_16] & Think_163=Catch1_163] & Think_115=Catch1_115] & Think_73=Catch1_73]] & Think_114=Catch1_114] & Think_23=Catch1_23]] & Think_190=Catch1_190] & Think_80=Catch1_80] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140] & Think_53=Catch1_53] & Think_179=Catch1_179]] & Think_22=Catch1_22] & Think_187=Catch1_187] & Think_104=Catch1_104]]] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84]] & Think_71=Catch1_71] & Think_141=Catch1_141] & Think_193=Catch1_193] & Think_74=Catch1_74] & Think_38=Catch1_38]]] & Think_188=Catch1_188] & Think_43=Catch1_43] & Think_56=Catch1_56] & Think_186=Catch1_186]]] & Think_5=Catch1_5] & Think_173=Catch1_173] & Think_62=Catch1_62]] & Think_118=Catch1_118] & Think_63=Catch1_63] & Think_99=Catch1_99] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162] & Think_166=Catch1_166] & Think_93=Catch1_93] & Think_98=Catch1_98] & Think_70=Catch1_70]] & Think_175=Catch1_175] & Think_92=Catch1_92] & Think_120=Catch1_120] & Think_89=Catch1_89] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31]] & Think_119=Catch1_119] & Think_133=Catch1_133] & Think_49=Catch1_49]] & Think_45=Catch1_45] & Think_153=Catch1_153] & Think_94=Catch1_94] & Think_126=Catch1_126]]] & Think_81=Catch1_81] & Think_122=Catch1_122] & Think_117=Catch1_117] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27]]] & Think_197=Catch1_197] & Think_96=Catch1_96]] & Think_164=Catch1_164] & Think_178=Catch1_178] & Think_132=Catch1_132] & Think_174=Catch1_174]] & Think_155=Catch1_155] & Think_184=Catch1_184]]] & Think_147=Catch1_147] & Think_24=Catch1_24]] & Think_30=Catch1_30] & Think_149=Catch1_149] & Think_142=Catch1_142]] & Think_194=Catch1_194] & Think_76=Catch1_76] & Think_10=Catch1_10]] & Think_40=Catch1_40] & Think_103=Catch1_103] & Think_91=Catch1_91]] & Think_20=Catch1_20] & Think_101=Catch1_101] & Think_100=Catch1_100]] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47]] & Think_195=Catch1_195] & Think_151=Catch1_151] & Think_165=Catch1_165]] & Think_72=Catch1_72] & Think_128=Catch1_128] & Think_14=Catch1_14]] & Think_106=Catch1_106] & Think_154=Catch1_154] & Think_18=Catch1_18]] & Think_61=Catch1_61] & Think_143=Catch1_143] & Think_189=Catch1_189]] & Think_123=Catch1_123] & Think_75=Catch1_75] & Think_52=Catch1_52]] & Think_157=Catch1_157] & Think_112=Catch1_112] & Think_146=Catch1_146]] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87]] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34]] & Think_11=Catch1_11] & Think_19=Catch1_19] & Think_139=Catch1_139]] & Think_2=Catch1_2] & Think_17=Catch1_17] & Think_111=Catch1_111]] & Think_134=Catch1_134] & Think_82=Catch1_82] & Think_144=Catch1_144]] & Think_138=Catch1_138] & Think_168=Catch1_168] & Think_121=Catch1_121]] & Think_127=Catch1_127] & [[[Eat_169!=Catch1_169 & [[[Eat_73!=Catch1_73 & [[[Eat_66!=Catch1_66 & [[[Eat_187!=Catch1_187 & [[[[[[[[Eat_97!=Catch1_97 & [[[[[[Eat_144!=Catch1_144 & [[[Eat_189!=Catch1_189 & [[[[[[[[[Eat_1!=Catch1_1 & [[[[[Eat_146!=Catch1_146 & [[[[[[[[[Eat_133!=Catch1_133 & [[[[Eat_119!=Catch1_119 & [[Eat_34!=Catch1_34 & [[[Eat_135!=Catch1_135 & [[[[Eat_99!=Catch1_99 & [[[[[[[Eat_108!=Catch1_108 & [[[[[Eat_163!=Catch1_163 & [[[Eat_124!=Catch1_124 & [[[[[[[[Eat_13!=Catch1_13 & [[[Eat_32!=Catch1_32 & [[[[Eat_115!=Catch1_115 & [[[[[[Eat_75!=Catch1_75 & [[[[Eat_123!=Catch1_123 & [[[Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [[[Eat_155!=Catch1_155 & [[[[Eat_72!=Catch1_72 & [[[[Eat_150!=Catch1_150 & [[[[Eat_178!=Catch1_178 & [[[[[[[[[[[[Eat_120!=Catch1_120 & [[[[Eat_111!=Catch1_111 & [[[[Eat_168!=Catch1_168 & [[[[Eat_5!=Catch1_5 & [[[[Eat_53!=Catch1_53 & [[[[Eat_172!=Catch1_172 & [[[[Eat_69!=Catch1_69 & [[[[Eat_170!=Catch1_170 & [[[[Eat_96!=Catch1_96 & [[[[Eat_2!=Catch1_2 & [[[[Eat_183!=Catch1_183 & [[[[Eat_109!=Catch1_109 & [[[[Eat_107!=Catch1_107 & [[[[Eat_49!=Catch1_49 & [[[[Eat_83!=Catch1_83 & [[[[Eat_188!=Catch1_188 & [[[[true & Eat_62!=Catch1_62] & Eat_67!=Catch1_67] & Eat_147!=Catch1_147] & Eat_142!=Catch1_142]] & Eat_182!=Catch1_182] & Eat_125!=Catch1_125] & Eat_10!=Catch1_10]] & Eat_171!=Catch1_171] & Eat_77!=Catch1_77] & Eat_6!=Catch1_6]] & Eat_176!=Catch1_176] & Eat_129!=Catch1_129] & Eat_148!=Catch1_148]] & Eat_174!=Catch1_174] & Eat_153!=Catch1_153] & Eat_91!=Catch1_91]] & Eat_68!=Catch1_68] & Eat_200!=Catch1_200] & Eat_195!=Catch1_195]] & Eat_7!=Catch1_7] & Eat_164!=Catch1_164] & Eat_45!=Catch1_45]] & Eat_191!=Catch1_191] & Eat_190!=Catch1_190] & Eat_37!=Catch1_37]] & Eat_138!=Catch1_138] & Eat_137!=Catch1_137] & Eat_181!=Catch1_181]] & Eat_127!=Catch1_127] & Eat_24!=Catch1_24] & Eat_162!=Catch1_162]] & Eat_139!=Catch1_139] & Eat_198!=Catch1_198] & Eat_87!=Catch1_87]] & Eat_4!=Catch1_4] & Eat_14!=Catch1_14] & Eat_113!=Catch1_113]] & Eat_92!=Catch1_92] & Eat_121!=Catch1_121] & Eat_184!=Catch1_184]] & Eat_86!=Catch1_86] & Eat_11!=Catch1_11] & Eat_61!=Catch1_61]] & Eat_39!=Catch1_39] & Eat_54!=Catch1_54] & Eat_44!=Catch1_44]] & Eat_64!=Catch1_64] & Eat_100!=Catch1_100] & Eat_101!=Catch1_101]] & Eat_20!=Catch1_20] & Eat_46!=Catch1_46] & Eat_166!=Catch1_166] & Eat_89!=Catch1_89] & Eat_50!=Catch1_50] & Eat_98!=Catch1_98] & Eat_131!=Catch1_131] & Eat_132!=Catch1_132] & Eat_17!=Catch1_17] & Eat_106!=Catch1_106] & Eat_156!=Catch1_156]] & Eat_47!=Catch1_47] & Eat_71!=Catch1_71] & Eat_21!=Catch1_21]] & Eat_160!=Catch1_160] & Eat_60!=Catch1_60] & Eat_48!=Catch1_48]] & Eat_157!=Catch1_157] & Eat_74!=Catch1_74] & Eat_128!=Catch1_128]] & Eat_8!=Catch1_8] & Eat_122!=Catch1_122]]] & Eat_141!=Catch1_141] & Eat_12!=Catch1_12]] & Eat_93!=Catch1_93] & Eat_143!=Catch1_143] & Eat_56!=Catch1_56]] & Eat_16!=Catch1_16] & Eat_3!=Catch1_3] & Eat_88!=Catch1_88] & Eat_114!=Catch1_114] & Eat_151!=Catch1_151]] & Eat_197!=Catch1_197] & Eat_81!=Catch1_81] & Eat_159!=Catch1_159]] & Eat_36!=Catch1_36] & Eat_192!=Catch1_192]] & Eat_165!=Catch1_165] & Eat_194!=Catch1_194] & Eat_25!=Catch1_25] & Eat_185!=Catch1_185] & Eat_23!=Catch1_23] & Eat_105!=Catch1_105] & Eat_145!=Catch1_145]] & Eat_180!=Catch1_180] & Eat_102!=Catch1_102]] & Eat_41!=Catch1_41] & Eat_134!=Catch1_134] & Eat_19!=Catch1_19] & Eat_94!=Catch1_94]] & Eat_85!=Catch1_85] & Eat_110!=Catch1_110] & Eat_118!=Catch1_118] & Eat_42!=Catch1_42] & Eat_149!=Catch1_149] & Eat_28!=Catch1_28]] & Eat_30!=Catch1_30] & Eat_199!=Catch1_199] & Eat_31!=Catch1_31]] & Eat_103!=Catch1_103] & Eat_90!=Catch1_90]] & Eat_167!=Catch1_167]] & Eat_82!=Catch1_82] & Eat_52!=Catch1_52] & Eat_40!=Catch1_40]] & Eat_173!=Catch1_173] & Eat_80!=Catch1_80] & Eat_112!=Catch1_112] & Eat_79!=Catch1_79] & Eat_57!=Catch1_57] & Eat_161!=Catch1_161] & Eat_186!=Catch1_186] & Eat_65!=Catch1_65]] & Eat_76!=Catch1_76] & Eat_51!=Catch1_51] & Eat_154!=Catch1_154] & Eat_193!=Catch1_193]] & Eat_117!=Catch1_117] & Eat_177!=Catch1_177] & Eat_70!=Catch1_70] & Eat_26!=Catch1_26] & Eat_78!=Catch1_78] & Eat_43!=Catch1_43] & Eat_18!=Catch1_18] & Eat_126!=Catch1_126]] & Eat_104!=Catch1_104] & Eat_179!=Catch1_179]] & Eat_175!=Catch1_175] & Eat_27!=Catch1_27] & Eat_29!=Catch1_29] & Eat_63!=Catch1_63] & Eat_38!=Catch1_38]] & Eat_9!=Catch1_9] & Eat_84!=Catch1_84] & Eat_158!=Catch1_158] & Eat_196!=Catch1_196] & Eat_35!=Catch1_35] & Eat_116!=Catch1_116] & Eat_15!=Catch1_15]] & Eat_136!=Catch1_136] & Eat_33!=Catch1_33]] & Eat_59!=Catch1_59] & Eat_130!=Catch1_130]] & Eat_22!=Catch1_22] & Eat_55!=Catch1_55]] & Eat_95!=Catch1_95] & Eat_58!=Catch1_58]]]
normalized: ~ [E [true U ~ [[[Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_9_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Eat_95!=Catch1_95 & [[[[[Eat_130!=Catch1_130 & [[[[[[[[[[[[Eat_9!=Catch1_9 & [[[[[Eat_27!=Catch1_27 & [[[[[[[Eat_18!=Catch1_18 & [[[[[Eat_177!=Catch1_177 & [[[[[[[Eat_146!=Catch1_146 & [[[[[Eat_79!=Catch1_79 & [[Eat_80!=Catch1_80 & [[[[[Eat_82!=Catch1_82 & [[[[[Eat_103!=Catch1_103 & [[[[[[[[[[[[[[Eat_19!=Catch1_19 & [[[[[[[[[[Eat_185!=Catch1_185 & [[[[[[[[[[[[[[[[[[[[[[[[[[Eat_122!=Catch1_122 & [[[[[[[[[[[[[[[[[[[[[[Eat_89!=Catch1_89 & [[Eat_46!=Catch1_46 & [[[[[[[[[[[[[[[[[[[[[[Eat_172!=Catch1_172 & [[[[[[[[[[[[[[[[[[[[[[[[[[Eat_153!=Catch1_153 & [[[[[[[[[[[[[[[[[Eat_67!=Catch1_67 & [true & Eat_62!=Catch1_62]] & Eat_147!=Catch1_147] & Eat_142!=Catch1_142] & Eat_188!=Catch1_188] & Eat_182!=Catch1_182] & Eat_125!=Catch1_125] & Eat_10!=Catch1_10] & Eat_83!=Catch1_83] & Eat_171!=Catch1_171] & Eat_77!=Catch1_77] & Eat_6!=Catch1_6] & Eat_49!=Catch1_49] & Eat_176!=Catch1_176] & Eat_129!=Catch1_129] & Eat_148!=Catch1_148] & Eat_107!=Catch1_107] & Eat_174!=Catch1_174]] & Eat_91!=Catch1_91] & Eat_109!=Catch1_109] & Eat_68!=Catch1_68] & Eat_200!=Catch1_200] & Eat_195!=Catch1_195] & Eat_183!=Catch1_183] & Eat_7!=Catch1_7] & Eat_164!=Catch1_164] & Eat_45!=Catch1_45] & Eat_2!=Catch1_2] & Eat_191!=Catch1_191] & Eat_190!=Catch1_190] & Eat_37!=Catch1_37] & Eat_96!=Catch1_96] & Eat_138!=Catch1_138] & Eat_137!=Catch1_137] & Eat_181!=Catch1_181] & Eat_170!=Catch1_170] & Eat_127!=Catch1_127] & Eat_24!=Catch1_24] & Eat_162!=Catch1_162] & Eat_69!=Catch1_69] & Eat_139!=Catch1_139] & Eat_198!=Catch1_198] & Eat_87!=Catch1_87]] & Eat_4!=Catch1_4] & Eat_14!=Catch1_14] & Eat_113!=Catch1_113] & Eat_53!=Catch1_53] & Eat_92!=Catch1_92] & Eat_121!=Catch1_121] & Eat_184!=Catch1_184] & Eat_5!=Catch1_5] & Eat_86!=Catch1_86] & Eat_11!=Catch1_11] & Eat_61!=Catch1_61] & Eat_168!=Catch1_168] & Eat_39!=Catch1_39] & Eat_54!=Catch1_54] & Eat_44!=Catch1_44] & Eat_111!=Catch1_111] & Eat_64!=Catch1_64] & Eat_100!=Catch1_100] & Eat_101!=Catch1_101] & Eat_120!=Catch1_120] & Eat_20!=Catch1_20]] & Eat_166!=Catch1_166]] & Eat_50!=Catch1_50] & Eat_98!=Catch1_98] & Eat_131!=Catch1_131] & Eat_132!=Catch1_132] & Eat_17!=Catch1_17] & Eat_106!=Catch1_106] & Eat_156!=Catch1_156] & Eat_178!=Catch1_178] & Eat_47!=Catch1_47] & Eat_71!=Catch1_71] & Eat_21!=Catch1_21] & Eat_150!=Catch1_150] & Eat_160!=Catch1_160] & Eat_60!=Catch1_60] & Eat_48!=Catch1_48] & Eat_72!=Catch1_72] & Eat_157!=Catch1_157] & Eat_74!=Catch1_74] & Eat_128!=Catch1_128] & Eat_155!=Catch1_155] & Eat_8!=Catch1_8]] & Eat_140!=Catch1_140] & Eat_152!=Catch1_152] & Eat_141!=Catch1_141] & Eat_12!=Catch1_12] & Eat_123!=Catch1_123] & Eat_93!=Catch1_93] & Eat_143!=Catch1_143] & Eat_56!=Catch1_56] & Eat_75!=Catch1_75] & Eat_16!=Catch1_16] & Eat_3!=Catch1_3] & Eat_88!=Catch1_88] & Eat_114!=Catch1_114] & Eat_151!=Catch1_151] & Eat_115!=Catch1_115] & Eat_197!=Catch1_197] & Eat_81!=Catch1_81] & Eat_159!=Catch1_159] & Eat_32!=Catch1_32] & Eat_36!=Catch1_36] & Eat_192!=Catch1_192] & Eat_13!=Catch1_13] & Eat_165!=Catch1_165] & Eat_194!=Catch1_194] & Eat_25!=Catch1_25]] & Eat_23!=Catch1_23] & Eat_105!=Catch1_105] & Eat_145!=Catch1_145] & Eat_124!=Catch1_124] & Eat_180!=Catch1_180] & Eat_102!=Catch1_102] & Eat_163!=Catch1_163] & Eat_41!=Catch1_41] & Eat_134!=Catch1_134]] & Eat_94!=Catch1_94] & Eat_108!=Catch1_108] & Eat_85!=Catch1_85] & Eat_110!=Catch1_110] & Eat_118!=Catch1_118] & Eat_42!=Catch1_42] & Eat_149!=Catch1_149] & Eat_28!=Catch1_28] & Eat_99!=Catch1_99] & Eat_30!=Catch1_30] & Eat_199!=Catch1_199] & Eat_31!=Catch1_31] & Eat_135!=Catch1_135]] & Eat_90!=Catch1_90] & Eat_34!=Catch1_34] & Eat_167!=Catch1_167] & Eat_119!=Catch1_119]] & Eat_52!=Catch1_52] & Eat_40!=Catch1_40] & Eat_133!=Catch1_133] & Eat_173!=Catch1_173]] & Eat_112!=Catch1_112]] & Eat_57!=Catch1_57] & Eat_161!=Catch1_161] & Eat_186!=Catch1_186] & Eat_65!=Catch1_65]] & Eat_76!=Catch1_76] & Eat_51!=Catch1_51] & Eat_154!=Catch1_154] & Eat_193!=Catch1_193] & Eat_1!=Catch1_1] & Eat_117!=Catch1_117]] & Eat_70!=Catch1_70] & Eat_26!=Catch1_26] & Eat_78!=Catch1_78] & Eat_43!=Catch1_43]] & Eat_126!=Catch1_126] & Eat_189!=Catch1_189] & Eat_104!=Catch1_104] & Eat_179!=Catch1_179] & Eat_144!=Catch1_144] & Eat_175!=Catch1_175]] & Eat_29!=Catch1_29] & Eat_63!=Catch1_63] & Eat_38!=Catch1_38] & Eat_97!=Catch1_97]] & Eat_84!=Catch1_84] & Eat_158!=Catch1_158] & Eat_196!=Catch1_196] & Eat_35!=Catch1_35] & Eat_116!=Catch1_116] & Eat_15!=Catch1_15] & Eat_187!=Catch1_187] & Eat_136!=Catch1_136] & Eat_33!=Catch1_33] & Eat_66!=Catch1_66] & Eat_59!=Catch1_59]] & Eat_73!=Catch1_73] & Eat_22!=Catch1_22] & Eat_55!=Catch1_55] & Eat_169!=Catch1_169]] & Eat_58!=Catch1_58] | [[Think_9=Catch1_9 & [[[[[Think_144=Catch1_144 & [[[[[[[[[[Think_11=Catch1_11 & [[[[[Think_1=Catch1_1 & [[[[[Think_146=Catch1_146 & [[Think_157=Catch1_157 & [[[Think_75=Catch1_75 & [[[[[[[Think_18=Catch1_18 & [[[[[Think_128=Catch1_128 & [[[[[Think_195=Catch1_195 & [[Think_47=Catch1_47 & [[[[[[[[[[Think_40=Catch1_40 & [[[[[Think_28=Catch1_28 & [[Think_149=Catch1_149 & [[[[[Think_158=Catch1_158 & [[[Think_155=Catch1_155 & [[[[[Think_164=Catch1_164 & [[Think_96=Catch1_96 & [[[[[[[[Think_117=Catch1_117 & [[Think_81=Catch1_81 & [[[[[[[[[[Think_119=Catch1_119 & [[[[[[[[Think_92=Catch1_92 & [[[[[Think_93=Catch1_93 & [[[[[Think_99=Catch1_99 & [[Think_118=Catch1_118 & [[[Think_173=Catch1_173 & [[Think_79=Catch1_79 & [[[Think_56=Catch1_56 & [[Think_188=Catch1_188 & [[[Think_38=Catch1_38 & [[[[[[[[[[Think_191=Catch1_191 & [[Think_104=Catch1_104 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_68=Catch1_68 & [[[Think_136=Catch1_136 & [[Think_7=Catch1_7 & [[[[[[[[[[[[[[[[Think_161=Catch1_161 & [Think_78=Catch1_78 & [true & Think_130=Catch1_130]]] & Think_66=Catch1_66] & Think_77=Catch1_77] & Think_39=Catch1_39] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148] & Think_15=Catch1_15] & Think_83=Catch1_83] & Think_159=Catch1_159] & Think_44=Catch1_44] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95]] & Think_116=Catch1_116]] & Think_113=Catch1_113] & Think_200=Catch1_200]] & Think_21=Catch1_21] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36] & Think_25=Catch1_25] & Think_86=Catch1_86] & Think_65=Catch1_65] & Think_16=Catch1_16] & Think_163=Catch1_163] & Think_115=Catch1_115] & Think_73=Catch1_73] & Think_102=Catch1_102] & Think_114=Catch1_114] & Think_23=Catch1_23] & Think_108=Catch1_108] & Think_190=Catch1_190] & Think_80=Catch1_80] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140] & Think_53=Catch1_53] & Think_179=Catch1_179] & Think_33=Catch1_33] & Think_22=Catch1_22] & Think_187=Catch1_187]] & Think_177=Catch1_177]] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71] & Think_141=Catch1_141] & Think_193=Catch1_193] & Think_74=Catch1_74]] & Think_51=Catch1_51] & Think_59=Catch1_59]] & Think_43=Catch1_43]] & Think_186=Catch1_186] & Think_32=Catch1_32]] & Think_5=Catch1_5]] & Think_62=Catch1_62] & Think_26=Catch1_26]] & Think_63=Catch1_63]] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162] & Think_166=Catch1_166]] & Think_98=Catch1_98] & Think_70=Catch1_70] & Think_4=Catch1_4] & Think_175=Catch1_175]] & Think_120=Catch1_120] & Think_89=Catch1_89] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31] & Think_97=Catch1_97]] & Think_133=Catch1_133] & Think_49=Catch1_49] & Think_124=Catch1_124] & Think_45=Catch1_45] & Think_153=Catch1_153] & Think_94=Catch1_94] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3]] & Think_122=Catch1_122]] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27] & Think_137=Catch1_137] & Think_176=Catch1_176] & Think_197=Catch1_197]] & Think_54=Catch1_54]] & Think_178=Catch1_178] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58]] & Think_184=Catch1_184] & Think_170=Catch1_170]] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181] & Think_30=Catch1_30]] & Think_142=Catch1_142]] & Think_194=Catch1_194] & Think_76=Catch1_76] & Think_10=Catch1_10] & Think_150=Catch1_150]] & Think_103=Catch1_103] & Think_91=Catch1_91] & Think_88=Catch1_88] & Think_20=Catch1_20] & Think_101=Catch1_101] & Think_100=Catch1_100] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171]] & Think_152=Catch1_152]] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72]] & Think_14=Catch1_14] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154]] & Think_46=Catch1_46] & Think_61=Catch1_61] & Think_143=Catch1_143] & Think_189=Catch1_189] & Think_156=Catch1_156] & Think_123=Catch1_123]] & Think_52=Catch1_52] & Think_198=Catch1_198]] & Think_112=Catch1_112]] & Think_12=Catch1_12] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87]] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34] & Think_160=Catch1_160]] & Think_19=Catch1_19] & Think_139=Catch1_139] & Think_50=Catch1_50] & Think_2=Catch1_2] & Think_17=Catch1_17] & Think_111=Catch1_111] & Think_57=Catch1_57] & Think_134=Catch1_134] & Think_82=Catch1_82]] & Think_90=Catch1_90] & Think_138=Catch1_138] & Think_168=Catch1_168] & Think_121=Catch1_121]] & Think_127=Catch1_127]]]
normalized: ~ [E [true U ~ [[[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_10_placecomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[[[[[[[[Think_134=Catch1_134 & [[[[Think_2=Catch1_2 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_107=Catch1_107 & [[[[[[[[[[[[[[[[[[Think_167=Catch1_167 & [[[[Think_175=Catch1_175 & [[[[[[[[[[[[[[[[[[[[[[[[[[[Think_141=Catch1_141 & [[[[[[[[[Think_104=Catch1_104 & [[Think_22=Catch1_22 & [[[[[[[Think_80=Catch1_80 & [[[[[[[Think_115=Catch1_115 & [[Think_16=Catch1_16 & [[[[[[[[[Think_29=Catch1_29 & [[[[[[[[[[[[[[[[[[[[[[[Think_161=Catch1_161 & [[true & Think_130=Catch1_130] & Think_78=Catch1_78]] & Think_66=Catch1_66] & Think_77=Catch1_77] & Think_39=Catch1_39] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148] & Think_15=Catch1_15] & Think_83=Catch1_83] & Think_159=Catch1_159] & Think_44=Catch1_44] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95] & Think_7=Catch1_7] & Think_116=Catch1_116] & Think_136=Catch1_136] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68] & Think_21=Catch1_21]] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36] & Think_25=Catch1_25] & Think_86=Catch1_86] & Think_65=Catch1_65]] & Think_163=Catch1_163]] & Think_73=Catch1_73] & Think_102=Catch1_102] & Think_114=Catch1_114] & Think_23=Catch1_23] & Think_108=Catch1_108] & Think_190=Catch1_190]] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140] & Think_53=Catch1_53] & Think_179=Catch1_179] & Think_33=Catch1_33]] & Think_187=Catch1_187]] & Think_177=Catch1_177] & Think_191=Catch1_191] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71]] & Think_193=Catch1_193] & Think_74=Catch1_74] & Think_38=Catch1_38] & Think_51=Catch1_51] & Think_59=Catch1_59] & Think_188=Catch1_188] & Think_43=Catch1_43] & Think_56=Catch1_56] & Think_186=Catch1_186] & Think_32=Catch1_32] & Think_79=Catch1_79] & Think_5=Catch1_5] & Think_173=Catch1_173] & Think_62=Catch1_62] & Think_26=Catch1_26] & Think_118=Catch1_118] & Think_63=Catch1_63] & Think_99=Catch1_99] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162] & Think_166=Catch1_166] & Think_93=Catch1_93] & Think_98=Catch1_98] & Think_70=Catch1_70] & Think_4=Catch1_4]] & Think_92=Catch1_92] & Think_120=Catch1_120] & Think_89=Catch1_89]] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31] & Think_97=Catch1_97] & Think_119=Catch1_119] & Think_133=Catch1_133] & Think_49=Catch1_49] & Think_124=Catch1_124] & Think_45=Catch1_45] & Think_153=Catch1_153] & Think_94=Catch1_94] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3] & Think_81=Catch1_81] & Think_122=Catch1_122] & Think_117=Catch1_117]] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27] & Think_137=Catch1_137] & Think_176=Catch1_176] & Think_197=Catch1_197] & Think_96=Catch1_96] & Think_54=Catch1_54] & Think_164=Catch1_164] & Think_178=Catch1_178] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58] & Think_155=Catch1_155] & Think_184=Catch1_184] & Think_170=Catch1_170] & Think_158=Catch1_158] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181] & Think_30=Catch1_30] & Think_149=Catch1_149] & Think_142=Catch1_142] & Think_28=Catch1_28] & Think_194=Catch1_194] & Think_76=Catch1_76] & Think_10=Catch1_10] & Think_150=Catch1_150] & Think_40=Catch1_40] & Think_103=Catch1_103] & Think_91=Catch1_91] & Think_88=Catch1_88] & Think_20=Catch1_20] & Think_101=Catch1_101] & Think_100=Catch1_100] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152] & Think_195=Catch1_195] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72] & Think_128=Catch1_128] & Think_14=Catch1_14] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154] & Think_18=Catch1_18] & Think_46=Catch1_46] & Think_61=Catch1_61] & Think_143=Catch1_143] & Think_189=Catch1_189] & Think_156=Catch1_156] & Think_123=Catch1_123] & Think_75=Catch1_75] & Think_52=Catch1_52] & Think_198=Catch1_198] & Think_157=Catch1_157] & Think_112=Catch1_112] & Think_146=Catch1_146] & Think_12=Catch1_12] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87] & Think_1=Catch1_1] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34] & Think_160=Catch1_160] & Think_11=Catch1_11] & Think_19=Catch1_19] & Think_139=Catch1_139] & Think_50=Catch1_50]] & Think_17=Catch1_17] & Think_111=Catch1_111] & Think_57=Catch1_57]] & Think_82=Catch1_82] & Think_144=Catch1_144] & Think_90=Catch1_90] & Think_138=Catch1_138] & Think_168=Catch1_168] & Think_121=Catch1_121] & Think_9=Catch1_9] & Think_127=Catch1_127]] xor ~ [[[[[[[Eat_73!=Catch1_73 & [[Eat_59!=Catch1_59 & [[[[Eat_187!=Catch1_187 & [[[[[Eat_158!=Catch1_158 & [[[[[[[[[[[Eat_104!=Catch1_104 & [[Eat_126!=Catch1_126 & [[[[[[[[[[[Eat_51!=Catch1_51 & [[Eat_146!=Catch1_146 & [[Eat_186!=Catch1_186 & [[[[[Eat_80!=Catch1_80 & [[[[[[[[[[[Eat_135!=Catch1_135 & [[[[Eat_99!=Catch1_99 & [[[[[[[[[Eat_19!=Catch1_19 & [[[[Eat_102!=Catch1_102 & [[[[[Eat_23!=Catch1_23 & [[Eat_25!=Catch1_25 & [[[[Eat_192!=Catch1_192 & [[[[[[[[[Eat_88!=Catch1_88 & [[[[[[[[[[[Eat_140!=Catch1_140 & [[Eat_8!=Catch1_8 & [[[[[Eat_72!=Catch1_72 & [[Eat_60!=Catch1_60 & [[[[Eat_71!=Catch1_71 & [[[[[Eat_17!=Catch1_17 & [[[[Eat_50!=Catch1_50 & [[[[[[[Eat_100!=Catch1_100 & [[[[Eat_54!=Catch1_54 & [[[[[[[Eat_184!=Catch1_184 & [[[[Eat_113!=Catch1_113 & [[[[[[[Eat_69!=Catch1_69 & [[[[Eat_170!=Catch1_170 & [[[[[[[[[Eat_45!=Catch1_45 & [[Eat_7!=Catch1_7 & [[[[[[[Eat_153!=Catch1_153 & [[Eat_107!=Catch1_107 & [[[[[[[Eat_171!=Catch1_171 & [[[[[[[[Eat_67!=Catch1_67 & [true & Eat_62!=Catch1_62]] & Eat_147!=Catch1_147] & Eat_142!=Catch1_142] & Eat_188!=Catch1_188] & Eat_182!=Catch1_182] & Eat_125!=Catch1_125] & Eat_10!=Catch1_10] & Eat_83!=Catch1_83]] & Eat_77!=Catch1_77] & Eat_6!=Catch1_6] & Eat_49!=Catch1_49] & Eat_176!=Catch1_176] & Eat_129!=Catch1_129] & Eat_148!=Catch1_148]] & Eat_174!=Catch1_174]] & Eat_91!=Catch1_91] & Eat_109!=Catch1_109] & Eat_68!=Catch1_68] & Eat_200!=Catch1_200] & Eat_195!=Catch1_195] & Eat_183!=Catch1_183]] & Eat_164!=Catch1_164]] & Eat_2!=Catch1_2] & Eat_191!=Catch1_191] & Eat_190!=Catch1_190] & Eat_37!=Catch1_37] & Eat_96!=Catch1_96] & Eat_138!=Catch1_138] & Eat_137!=Catch1_137] & Eat_181!=Catch1_181]] & Eat_127!=Catch1_127] & Eat_24!=Catch1_24] & Eat_162!=Catch1_162]] & Eat_139!=Catch1_139] & Eat_198!=Catch1_198] & Eat_87!=Catch1_87] & Eat_172!=Catch1_172] & Eat_4!=Catch1_4] & Eat_14!=Catch1_14]] & Eat_53!=Catch1_53] & Eat_92!=Catch1_92] & Eat_121!=Catch1_121]] & Eat_5!=Catch1_5] & Eat_86!=Catch1_86] & Eat_11!=Catch1_11] & Eat_61!=Catch1_61] & Eat_168!=Catch1_168] & Eat_39!=Catch1_39]] & Eat_44!=Catch1_44] & Eat_111!=Catch1_111] & Eat_64!=Catch1_64]] & Eat_101!=Catch1_101] & Eat_120!=Catch1_120] & Eat_20!=Catch1_20] & Eat_46!=Catch1_46] & Eat_166!=Catch1_166] & Eat_89!=Catch1_89]] & Eat_98!=Catch1_98] & Eat_131!=Catch1_131] & Eat_132!=Catch1_132]] & Eat_106!=Catch1_106] & Eat_156!=Catch1_156] & Eat_178!=Catch1_178] & Eat_47!=Catch1_47]] & Eat_21!=Catch1_21] & Eat_150!=Catch1_150] & Eat_160!=Catch1_160]] & Eat_48!=Catch1_48]] & Eat_157!=Catch1_157] & Eat_74!=Catch1_74] & Eat_128!=Catch1_128] & Eat_155!=Catch1_155]] & Eat_122!=Catch1_122]] & Eat_152!=Catch1_152] & Eat_141!=Catch1_141] & Eat_12!=Catch1_12] & Eat_123!=Catch1_123] & Eat_93!=Catch1_93] & Eat_143!=Catch1_143] & Eat_56!=Catch1_56] & Eat_75!=Catch1_75] & Eat_16!=Catch1_16] & Eat_3!=Catch1_3]] & Eat_114!=Catch1_114] & Eat_151!=Catch1_151] & Eat_115!=Catch1_115] & Eat_197!=Catch1_197] & Eat_81!=Catch1_81] & Eat_159!=Catch1_159] & Eat_32!=Catch1_32] & Eat_36!=Catch1_36]] & Eat_13!=Catch1_13] & Eat_165!=Catch1_165] & Eat_194!=Catch1_194]] & Eat_185!=Catch1_185]] & Eat_105!=Catch1_105] & Eat_145!=Catch1_145] & Eat_124!=Catch1_124] & Eat_180!=Catch1_180]] & Eat_163!=Catch1_163] & Eat_41!=Catch1_41] & Eat_134!=Catch1_134]] & Eat_94!=Catch1_94] & Eat_108!=Catch1_108] & Eat_85!=Catch1_85] & Eat_110!=Catch1_110] & Eat_118!=Catch1_118] & Eat_42!=Catch1_42] & Eat_149!=Catch1_149] & Eat_28!=Catch1_28]] & Eat_30!=Catch1_30] & Eat_199!=Catch1_199] & Eat_31!=Catch1_31]] & Eat_103!=Catch1_103] & Eat_90!=Catch1_90] & Eat_34!=Catch1_34] & Eat_167!=Catch1_167] & Eat_119!=Catch1_119] & Eat_82!=Catch1_82] & Eat_52!=Catch1_52] & Eat_40!=Catch1_40] & Eat_133!=Catch1_133] & Eat_173!=Catch1_173]] & Eat_112!=Catch1_112] & Eat_79!=Catch1_79] & Eat_57!=Catch1_57] & Eat_161!=Catch1_161]] & Eat_65!=Catch1_65]] & Eat_76!=Catch1_76]] & Eat_154!=Catch1_154] & Eat_193!=Catch1_193] & Eat_1!=Catch1_1] & Eat_117!=Catch1_117] & Eat_177!=Catch1_177] & Eat_70!=Catch1_70] & Eat_26!=Catch1_26] & Eat_78!=Catch1_78] & Eat_43!=Catch1_43] & Eat_18!=Catch1_18]] & Eat_189!=Catch1_189]] & Eat_179!=Catch1_179] & Eat_144!=Catch1_144] & Eat_175!=Catch1_175] & Eat_27!=Catch1_27] & Eat_29!=Catch1_29] & Eat_63!=Catch1_63] & Eat_38!=Catch1_38] & Eat_97!=Catch1_97] & Eat_9!=Catch1_9] & Eat_84!=Catch1_84]] & Eat_196!=Catch1_196] & Eat_35!=Catch1_35] & Eat_116!=Catch1_116] & Eat_15!=Catch1_15]] & Eat_136!=Catch1_136] & Eat_33!=Catch1_33] & Eat_66!=Catch1_66]] & Eat_130!=Catch1_130]] & Eat_22!=Catch1_22] & Eat_55!=Catch1_55] & Eat_169!=Catch1_169] & Eat_95!=Catch1_95] & Eat_58!=Catch1_58]]]]
normalized: ~ [E [true U ~ [[[[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [[Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [~ [[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Eat_58!=Catch1_58 & [Eat_95!=Catch1_95 & [Eat_169!=Catch1_169 & [Eat_55!=Catch1_55 & [Eat_22!=Catch1_22 & [Eat_73!=Catch1_73 & [Eat_130!=Catch1_130 & [Eat_59!=Catch1_59 & [Eat_66!=Catch1_66 & [Eat_33!=Catch1_33 & [Eat_136!=Catch1_136 & [Eat_187!=Catch1_187 & [Eat_15!=Catch1_15 & [Eat_116!=Catch1_116 & [Eat_35!=Catch1_35 & [Eat_196!=Catch1_196 & [Eat_158!=Catch1_158 & [Eat_84!=Catch1_84 & [Eat_9!=Catch1_9 & [Eat_97!=Catch1_97 & [Eat_38!=Catch1_38 & [Eat_63!=Catch1_63 & [Eat_29!=Catch1_29 & [Eat_27!=Catch1_27 & [Eat_175!=Catch1_175 & [Eat_144!=Catch1_144 & [Eat_179!=Catch1_179 & [Eat_104!=Catch1_104 & [Eat_189!=Catch1_189 & [Eat_126!=Catch1_126 & [Eat_18!=Catch1_18 & [Eat_43!=Catch1_43 & [Eat_78!=Catch1_78 & [Eat_26!=Catch1_26 & [Eat_70!=Catch1_70 & [Eat_177!=Catch1_177 & [Eat_117!=Catch1_117 & [Eat_1!=Catch1_1 & [Eat_193!=Catch1_193 & [Eat_154!=Catch1_154 & [Eat_51!=Catch1_51 & [Eat_76!=Catch1_76 & [Eat_146!=Catch1_146 & [Eat_65!=Catch1_65 & [Eat_186!=Catch1_186 & [Eat_161!=Catch1_161 & [Eat_57!=Catch1_57 & [Eat_79!=Catch1_79 & [Eat_112!=Catch1_112 & [Eat_80!=Catch1_80 & [Eat_173!=Catch1_173 & [Eat_133!=Catch1_133 & [Eat_40!=Catch1_40 & [Eat_52!=Catch1_52 & [Eat_82!=Catch1_82 & [Eat_119!=Catch1_119 & [Eat_167!=Catch1_167 & [Eat_34!=Catch1_34 & [Eat_90!=Catch1_90 & [Eat_103!=Catch1_103 & [Eat_135!=Catch1_135 & [Eat_31!=Catch1_31 & [Eat_199!=Catch1_199 & [Eat_30!=Catch1_30 & [Eat_99!=Catch1_99 & [Eat_28!=Catch1_28 & [Eat_149!=Catch1_149 & [Eat_42!=Catch1_42 & [Eat_118!=Catch1_118 & [Eat_110!=Catch1_110 & [Eat_85!=Catch1_85 & [Eat_108!=Catch1_108 & [Eat_94!=Catch1_94 & [Eat_19!=Catch1_19 & [Eat_134!=Catch1_134 & [Eat_41!=Catch1_41 & [Eat_163!=Catch1_163 & [Eat_102!=Catch1_102 & [Eat_180!=Catch1_180 & [Eat_124!=Catch1_124 & [Eat_145!=Catch1_145 & [Eat_105!=Catch1_105 & [Eat_23!=Catch1_23 & [Eat_185!=Catch1_185 & [Eat_25!=Catch1_25 & [Eat_194!=Catch1_194 & [Eat_165!=Catch1_165 & [Eat_13!=Catch1_13 & [Eat_192!=Catch1_192 & [Eat_36!=Catch1_36 & [Eat_32!=Catch1_32 & [Eat_159!=Catch1_159 & [Eat_81!=Catch1_81 & [Eat_197!=Catch1_197 & [Eat_115!=Catch1_115 & [Eat_151!=Catch1_151 & [Eat_114!=Catch1_114 & [Eat_88!=Catch1_88 & [Eat_3!=Catch1_3 & [Eat_16!=Catch1_16 & [Eat_75!=Catch1_75 & [Eat_56!=Catch1_56 & [Eat_143!=Catch1_143 & [Eat_93!=Catch1_93 & [Eat_123!=Catch1_123 & [Eat_12!=Catch1_12 & [Eat_141!=Catch1_141 & [Eat_152!=Catch1_152 & [Eat_140!=Catch1_140 & [Eat_122!=Catch1_122 & [Eat_8!=Catch1_8 & [Eat_155!=Catch1_155 & [Eat_128!=Catch1_128 & [Eat_74!=Catch1_74 & [Eat_157!=Catch1_157 & [Eat_72!=Catch1_72 & [Eat_48!=Catch1_48 & [Eat_60!=Catch1_60 & [Eat_160!=Catch1_160 & [Eat_150!=Catch1_150 & [Eat_21!=Catch1_21 & [Eat_71!=Catch1_71 & [Eat_47!=Catch1_47 & [Eat_178!=Catch1_178 & [Eat_156!=Catch1_156 & [Eat_106!=Catch1_106 & [Eat_17!=Catch1_17 & [Eat_132!=Catch1_132 & [Eat_131!=Catch1_131 & [Eat_98!=Catch1_98 & [Eat_50!=Catch1_50 & [Eat_89!=Catch1_89 & [Eat_166!=Catch1_166 & [Eat_46!=Catch1_46 & [Eat_20!=Catch1_20 & [Eat_120!=Catch1_120 & [Eat_101!=Catch1_101 & [Eat_100!=Catch1_100 & [Eat_64!=Catch1_64 & [Eat_111!=Catch1_111 & [Eat_44!=Catch1_44 & [Eat_54!=Catch1_54 & [Eat_39!=Catch1_39 & [Eat_168!=Catch1_168 & [Eat_61!=Catch1_61 & [Eat_11!=Catch1_11 & [Eat_86!=Catch1_86 & [Eat_5!=Catch1_5 & [Eat_184!=Catch1_184 & [Eat_121!=Catch1_121 & [Eat_92!=Catch1_92 & [Eat_53!=Catch1_53 & [Eat_113!=Catch1_113 & [Eat_14!=Catch1_14 & [Eat_4!=Catch1_4 & [Eat_172!=Catch1_172 & [Eat_87!=Catch1_87 & [Eat_198!=Catch1_198 & [Eat_139!=Catch1_139 & [Eat_69!=Catch1_69 & [Eat_162!=Catch1_162 & [Eat_24!=Catch1_24 & [Eat_127!=Catch1_127 & [Eat_170!=Catch1_170 & [Eat_181!=Catch1_181 & [Eat_137!=Catch1_137 & [Eat_138!=Catch1_138 & [Eat_96!=Catch1_96 & [Eat_37!=Catch1_37 & [Eat_190!=Catch1_190 & [Eat_191!=Catch1_191 & [Eat_2!=Catch1_2 & [Eat_45!=Catch1_45 & [Eat_164!=Catch1_164 & [Eat_7!=Catch1_7 & [Eat_183!=Catch1_183 & [Eat_195!=Catch1_195 & [Eat_200!=Catch1_200 & [Eat_68!=Catch1_68 & [Eat_109!=Catch1_109 & [Eat_91!=Catch1_91 & [Eat_153!=Catch1_153 & [Eat_174!=Catch1_174 & [Eat_107!=Catch1_107 & [Eat_148!=Catch1_148 & [Eat_129!=Catch1_129 & [Eat_176!=Catch1_176 & [Eat_49!=Catch1_49 & [Eat_6!=Catch1_6 & [Eat_77!=Catch1_77 & [Eat_171!=Catch1_171 & [Eat_83!=Catch1_83 & [Eat_10!=Catch1_10 & [Eat_125!=Catch1_125 & [Eat_182!=Catch1_182 & [Eat_188!=Catch1_188 & [Eat_142!=Catch1_142 & [Eat_147!=Catch1_147 & [Eat_67!=Catch1_67 & [Eat_62!=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_11_placecomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[Eat_59=Catch1_59 & [[[[[[[[[[[[[Eat_38=Catch1_38 & [[[[[[[[Eat_189=Catch1_189 & [[[[[[[[[[[[[Eat_76=Catch1_76 & [[[Eat_186=Catch1_186 & [[[[[[[[[[[[[[[[[[[[[[[[[[Eat_85=Catch1_85 & [[[[[[[[[[[[[Eat_185=Catch1_185 & [[[[[Eat_192=Catch1_192 & [[[Eat_159=Catch1_159 & [[Eat_197=Catch1_197 & [[[[[[[[[[[Eat_123=Catch1_123 & [[[[[Eat_122=Catch1_122 & [[[[[[[[[[[[[[[[[[[[[[[[[Eat_20=Catch1_20 & [[[[[Eat_111=Catch1_111 & [[[[[Eat_61=Catch1_61 & [[[[[[[[[[[[[[Eat_139=Catch1_139 & [[[[[[[[[Eat_96=Catch1_96 & [[[[[Eat_45=Catch1_45 & [[Eat_7=Catch1_7 & [[[[[Eat_109=Catch1_109 & [[[[[[[[[[[[[[[[Eat_188=Catch1_188 & [[[[true & Eat_62=Catch1_62] & Eat_67=Catch1_67] & Eat_147=Catch1_147] & Eat_142=Catch1_142]] & Eat_182=Catch1_182] & Eat_125=Catch1_125] & Eat_10=Catch1_10] & Eat_83=Catch1_83] & Eat_171=Catch1_171] & Eat_77=Catch1_77] & Eat_6=Catch1_6] & Eat_49=Catch1_49] & Eat_176=Catch1_176] & Eat_129=Catch1_129] & Eat_148=Catch1_148] & Eat_107=Catch1_107] & Eat_174=Catch1_174] & Eat_153=Catch1_153] & Eat_91=Catch1_91]] & Eat_68=Catch1_68] & Eat_200=Catch1_200] & Eat_195=Catch1_195] & Eat_183=Catch1_183]] & Eat_164=Catch1_164]] & Eat_2=Catch1_2] & Eat_191=Catch1_191] & Eat_190=Catch1_190] & Eat_37=Catch1_37]] & Eat_138=Catch1_138] & Eat_137=Catch1_137] & Eat_181=Catch1_181] & Eat_170=Catch1_170] & Eat_127=Catch1_127] & Eat_24=Catch1_24] & Eat_162=Catch1_162] & Eat_69=Catch1_69]] & Eat_198=Catch1_198] & Eat_87=Catch1_87] & Eat_172=Catch1_172] & Eat_4=Catch1_4] & Eat_14=Catch1_14] & Eat_113=Catch1_113] & Eat_53=Catch1_53] & Eat_92=Catch1_92] & Eat_121=Catch1_121] & Eat_184=Catch1_184] & Eat_5=Catch1_5] & Eat_86=Catch1_86] & Eat_11=Catch1_11]] & Eat_168=Catch1_168] & Eat_39=Catch1_39] & Eat_54=Catch1_54] & Eat_44=Catch1_44]] & Eat_64=Catch1_64] & Eat_100=Catch1_100] & Eat_101=Catch1_101] & Eat_120=Catch1_120]] & Eat_46=Catch1_46] & Eat_166=Catch1_166] & Eat_89=Catch1_89] & Eat_50=Catch1_50] & Eat_98=Catch1_98] & Eat_131=Catch1_131] & Eat_132=Catch1_132] & Eat_17=Catch1_17] & Eat_106=Catch1_106] & Eat_156=Catch1_156] & Eat_178=Catch1_178] & Eat_47=Catch1_47] & Eat_71=Catch1_71] & Eat_21=Catch1_21] & Eat_150=Catch1_150] & Eat_160=Catch1_160] & Eat_60=Catch1_60] & Eat_48=Catch1_48] & Eat_72=Catch1_72] & Eat_157=Catch1_157] & Eat_74=Catch1_74] & Eat_128=Catch1_128] & Eat_155=Catch1_155] & Eat_8=Catch1_8]] & Eat_140=Catch1_140] & Eat_152=Catch1_152] & Eat_141=Catch1_141] & Eat_12=Catch1_12]] & Eat_93=Catch1_93] & Eat_143=Catch1_143] & Eat_56=Catch1_56] & Eat_75=Catch1_75] & Eat_16=Catch1_16] & Eat_3=Catch1_3] & Eat_88=Catch1_88] & Eat_114=Catch1_114] & Eat_151=Catch1_151] & Eat_115=Catch1_115]] & Eat_81=Catch1_81]] & Eat_32=Catch1_32] & Eat_36=Catch1_36]] & Eat_13=Catch1_13] & Eat_165=Catch1_165] & Eat_194=Catch1_194] & Eat_25=Catch1_25]] & Eat_23=Catch1_23] & Eat_105=Catch1_105] & Eat_145=Catch1_145] & Eat_124=Catch1_124] & Eat_180=Catch1_180] & Eat_102=Catch1_102] & Eat_163=Catch1_163] & Eat_41=Catch1_41] & Eat_134=Catch1_134] & Eat_19=Catch1_19] & Eat_94=Catch1_94] & Eat_108=Catch1_108]] & Eat_110=Catch1_110] & Eat_118=Catch1_118] & Eat_42=Catch1_42] & Eat_149=Catch1_149] & Eat_28=Catch1_28] & Eat_99=Catch1_99] & Eat_30=Catch1_30] & Eat_199=Catch1_199] & Eat_31=Catch1_31] & Eat_135=Catch1_135] & Eat_103=Catch1_103] & Eat_90=Catch1_90] & Eat_34=Catch1_34] & Eat_167=Catch1_167] & Eat_119=Catch1_119] & Eat_82=Catch1_82] & Eat_52=Catch1_52] & Eat_40=Catch1_40] & Eat_133=Catch1_133] & Eat_173=Catch1_173] & Eat_80=Catch1_80] & Eat_112=Catch1_112] & Eat_79=Catch1_79] & Eat_57=Catch1_57] & Eat_161=Catch1_161]] & Eat_65=Catch1_65] & Eat_146=Catch1_146]] & Eat_51=Catch1_51] & Eat_154=Catch1_154] & Eat_193=Catch1_193] & Eat_1=Catch1_1] & Eat_117=Catch1_117] & Eat_177=Catch1_177] & Eat_70=Catch1_70] & Eat_26=Catch1_26] & Eat_78=Catch1_78] & Eat_43=Catch1_43] & Eat_18=Catch1_18] & Eat_126=Catch1_126]] & Eat_104=Catch1_104] & Eat_179=Catch1_179] & Eat_144=Catch1_144] & Eat_175=Catch1_175] & Eat_27=Catch1_27] & Eat_29=Catch1_29] & Eat_63=Catch1_63]] & Eat_97=Catch1_97] & Eat_9=Catch1_9] & Eat_84=Catch1_84] & Eat_158=Catch1_158] & Eat_196=Catch1_196] & Eat_35=Catch1_35] & Eat_116=Catch1_116] & Eat_15=Catch1_15] & Eat_187=Catch1_187] & Eat_136=Catch1_136] & Eat_33=Catch1_33] & Eat_66=Catch1_66]] & Eat_130=Catch1_130] & Eat_73=Catch1_73] & Eat_22=Catch1_22] & Eat_55=Catch1_55] & Eat_169=Catch1_169] & Eat_95=Catch1_95] & Eat_58=Catch1_58] & [[Think_9=Catch1_9 & [[[[[Think_144=Catch1_144 & [[[[Think_111=Catch1_111 & [[[[[[[Think_160=Catch1_160 & [[Think_6=Catch1_6 & [[[[[[[[[[[Think_52=Catch1_52 & [[[[[[[[[[[[[Think_128=Catch1_128 & [[[[[[[[[[[[[[[Think_91=Catch1_91 & [[Think_40=Catch1_40 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_5=Catch1_5 & [[Think_32=Catch1_32 & [[[[Think_188=Catch1_188 & [[[[Think_74=Catch1_74 & [[[[[[[[[[[[[Think_22=Catch1_22 & [[Think_179=Catch1_179 & [[[[[[[[[[[Think_73=Catch1_73 & [[[[Think_65=Catch1_65 & [[Think_25=Catch1_25 & [[[[[[[[[[[Think_136=Catch1_136 & [[Think_7=Catch1_7 & [[[[[[[[[[[[[Think_39=Catch1_39 & [[[Think_161=Catch1_161 & [[true & Think_130=Catch1_130] & Think_78=Catch1_78]] & Think_66=Catch1_66] & Think_77=Catch1_77]] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148] & Think_15=Catch1_15] & Think_83=Catch1_83] & Think_159=Catch1_159] & Think_44=Catch1_44] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95]] & Think_116=Catch1_116]] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68] & Think_21=Catch1_21] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36]] & Think_86=Catch1_86]] & Think_16=Catch1_16] & Think_163=Catch1_163] & Think_115=Catch1_115]] & Think_102=Catch1_102] & Think_114=Catch1_114] & Think_23=Catch1_23] & Think_108=Catch1_108] & Think_190=Catch1_190] & Think_80=Catch1_80] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140] & Think_53=Catch1_53]] & Think_33=Catch1_33]] & Think_187=Catch1_187] & Think_104=Catch1_104] & Think_177=Catch1_177] & Think_191=Catch1_191] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71] & Think_141=Catch1_141] & Think_193=Catch1_193]] & Think_38=Catch1_38] & Think_51=Catch1_51] & Think_59=Catch1_59]] & Think_43=Catch1_43] & Think_56=Catch1_56] & Think_186=Catch1_186]] & Think_79=Catch1_79]] & Think_173=Catch1_173] & Think_62=Catch1_62] & Think_26=Catch1_26] & Think_118=Catch1_118] & Think_63=Catch1_63] & Think_99=Catch1_99] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162] & Think_166=Catch1_166] & Think_93=Catch1_93] & Think_98=Catch1_98] & Think_70=Catch1_70] & Think_4=Catch1_4] & Think_175=Catch1_175] & Think_92=Catch1_92] & Think_120=Catch1_120] & Think_89=Catch1_89] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31] & Think_97=Catch1_97] & Think_119=Catch1_119] & Think_133=Catch1_133] & Think_49=Catch1_49] & Think_124=Catch1_124] & Think_45=Catch1_45] & Think_153=Catch1_153] & Think_94=Catch1_94] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3] & Think_81=Catch1_81] & Think_122=Catch1_122] & Think_117=Catch1_117] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27] & Think_137=Catch1_137] & Think_176=Catch1_176] & Think_197=Catch1_197] & Think_96=Catch1_96] & Think_54=Catch1_54] & Think_164=Catch1_164] & Think_178=Catch1_178] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58] & Think_155=Catch1_155] & Think_184=Catch1_184] & Think_170=Catch1_170] & Think_158=Catch1_158] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181] & Think_30=Catch1_30] & Think_149=Catch1_149] & Think_142=Catch1_142] & Think_28=Catch1_28] & Think_194=Catch1_194] & Think_76=Catch1_76] & Think_10=Catch1_10] & Think_150=Catch1_150]] & Think_103=Catch1_103]] & Think_88=Catch1_88] & Think_20=Catch1_20] & Think_101=Catch1_101] & Think_100=Catch1_100] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152] & Think_195=Catch1_195] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72]] & Think_14=Catch1_14] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154] & Think_18=Catch1_18] & Think_46=Catch1_46] & Think_61=Catch1_61] & Think_143=Catch1_143] & Think_189=Catch1_189] & Think_156=Catch1_156] & Think_123=Catch1_123] & Think_75=Catch1_75]] & Think_198=Catch1_198] & Think_157=Catch1_157] & Think_112=Catch1_112] & Think_146=Catch1_146] & Think_12=Catch1_12] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87] & Think_1=Catch1_1] & Think_131=Catch1_131]] & Think_34=Catch1_34]] & Think_11=Catch1_11] & Think_19=Catch1_19] & Think_139=Catch1_139] & Think_50=Catch1_50] & Think_2=Catch1_2] & Think_17=Catch1_17]] & Think_57=Catch1_57] & Think_134=Catch1_134] & Think_82=Catch1_82]] & Think_90=Catch1_90] & Think_138=Catch1_138] & Think_168=Catch1_168] & Think_121=Catch1_121]] & Think_127=Catch1_127]]]
normalized: ~ [E [true U ~ [[[Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Eat_58=Catch1_58 & [Eat_95=Catch1_95 & [Eat_169=Catch1_169 & [Eat_55=Catch1_55 & [Eat_22=Catch1_22 & [Eat_73=Catch1_73 & [Eat_130=Catch1_130 & [Eat_59=Catch1_59 & [Eat_66=Catch1_66 & [Eat_33=Catch1_33 & [Eat_136=Catch1_136 & [Eat_187=Catch1_187 & [Eat_15=Catch1_15 & [Eat_116=Catch1_116 & [Eat_35=Catch1_35 & [Eat_196=Catch1_196 & [Eat_158=Catch1_158 & [Eat_84=Catch1_84 & [Eat_9=Catch1_9 & [Eat_97=Catch1_97 & [Eat_38=Catch1_38 & [Eat_63=Catch1_63 & [Eat_29=Catch1_29 & [Eat_27=Catch1_27 & [Eat_175=Catch1_175 & [Eat_144=Catch1_144 & [Eat_179=Catch1_179 & [Eat_104=Catch1_104 & [Eat_189=Catch1_189 & [Eat_126=Catch1_126 & [Eat_18=Catch1_18 & [Eat_43=Catch1_43 & [Eat_78=Catch1_78 & [Eat_26=Catch1_26 & [Eat_70=Catch1_70 & [Eat_177=Catch1_177 & [Eat_117=Catch1_117 & [Eat_1=Catch1_1 & [Eat_193=Catch1_193 & [Eat_154=Catch1_154 & [Eat_51=Catch1_51 & [Eat_76=Catch1_76 & [Eat_146=Catch1_146 & [Eat_65=Catch1_65 & [Eat_186=Catch1_186 & [Eat_161=Catch1_161 & [Eat_57=Catch1_57 & [Eat_79=Catch1_79 & [Eat_112=Catch1_112 & [Eat_80=Catch1_80 & [Eat_173=Catch1_173 & [Eat_133=Catch1_133 & [Eat_40=Catch1_40 & [Eat_52=Catch1_52 & [Eat_82=Catch1_82 & [Eat_119=Catch1_119 & [Eat_167=Catch1_167 & [Eat_34=Catch1_34 & [Eat_90=Catch1_90 & [Eat_103=Catch1_103 & [Eat_135=Catch1_135 & [Eat_31=Catch1_31 & [Eat_199=Catch1_199 & [Eat_30=Catch1_30 & [Eat_99=Catch1_99 & [Eat_28=Catch1_28 & [Eat_149=Catch1_149 & [Eat_42=Catch1_42 & [Eat_118=Catch1_118 & [Eat_110=Catch1_110 & [Eat_85=Catch1_85 & [Eat_108=Catch1_108 & [Eat_94=Catch1_94 & [Eat_19=Catch1_19 & [Eat_134=Catch1_134 & [Eat_41=Catch1_41 & [Eat_163=Catch1_163 & [Eat_102=Catch1_102 & [Eat_180=Catch1_180 & [Eat_124=Catch1_124 & [Eat_145=Catch1_145 & [Eat_105=Catch1_105 & [Eat_23=Catch1_23 & [Eat_185=Catch1_185 & [Eat_25=Catch1_25 & [Eat_194=Catch1_194 & [Eat_165=Catch1_165 & [Eat_13=Catch1_13 & [Eat_192=Catch1_192 & [Eat_36=Catch1_36 & [Eat_32=Catch1_32 & [Eat_159=Catch1_159 & [Eat_81=Catch1_81 & [Eat_197=Catch1_197 & [Eat_115=Catch1_115 & [Eat_151=Catch1_151 & [Eat_114=Catch1_114 & [Eat_88=Catch1_88 & [Eat_3=Catch1_3 & [Eat_16=Catch1_16 & [Eat_75=Catch1_75 & [Eat_56=Catch1_56 & [Eat_143=Catch1_143 & [Eat_93=Catch1_93 & [Eat_123=Catch1_123 & [Eat_12=Catch1_12 & [Eat_141=Catch1_141 & [Eat_152=Catch1_152 & [Eat_140=Catch1_140 & [Eat_122=Catch1_122 & [Eat_8=Catch1_8 & [Eat_155=Catch1_155 & [Eat_128=Catch1_128 & [Eat_74=Catch1_74 & [Eat_157=Catch1_157 & [Eat_72=Catch1_72 & [Eat_48=Catch1_48 & [Eat_60=Catch1_60 & [Eat_160=Catch1_160 & [Eat_150=Catch1_150 & [Eat_21=Catch1_21 & [Eat_71=Catch1_71 & [Eat_47=Catch1_47 & [Eat_178=Catch1_178 & [Eat_156=Catch1_156 & [Eat_106=Catch1_106 & [Eat_17=Catch1_17 & [Eat_132=Catch1_132 & [Eat_131=Catch1_131 & [Eat_98=Catch1_98 & [Eat_50=Catch1_50 & [Eat_89=Catch1_89 & [Eat_166=Catch1_166 & [Eat_46=Catch1_46 & [Eat_20=Catch1_20 & [Eat_120=Catch1_120 & [Eat_101=Catch1_101 & [Eat_100=Catch1_100 & [Eat_64=Catch1_64 & [Eat_111=Catch1_111 & [Eat_44=Catch1_44 & [Eat_54=Catch1_54 & [Eat_39=Catch1_39 & [Eat_168=Catch1_168 & [Eat_61=Catch1_61 & [Eat_11=Catch1_11 & [Eat_86=Catch1_86 & [Eat_5=Catch1_5 & [Eat_184=Catch1_184 & [Eat_121=Catch1_121 & [Eat_92=Catch1_92 & [Eat_53=Catch1_53 & [Eat_113=Catch1_113 & [Eat_14=Catch1_14 & [Eat_4=Catch1_4 & [Eat_172=Catch1_172 & [Eat_87=Catch1_87 & [Eat_198=Catch1_198 & [Eat_139=Catch1_139 & [Eat_69=Catch1_69 & [Eat_162=Catch1_162 & [Eat_24=Catch1_24 & [Eat_127=Catch1_127 & [Eat_170=Catch1_170 & [Eat_181=Catch1_181 & [Eat_137=Catch1_137 & [Eat_138=Catch1_138 & [Eat_96=Catch1_96 & [Eat_37=Catch1_37 & [Eat_190=Catch1_190 & [Eat_191=Catch1_191 & [Eat_2=Catch1_2 & [Eat_45=Catch1_45 & [Eat_164=Catch1_164 & [Eat_7=Catch1_7 & [Eat_183=Catch1_183 & [Eat_195=Catch1_195 & [Eat_200=Catch1_200 & [Eat_68=Catch1_68 & [Eat_109=Catch1_109 & [Eat_91=Catch1_91 & [Eat_153=Catch1_153 & [Eat_174=Catch1_174 & [Eat_107=Catch1_107 & [Eat_148=Catch1_148 & [Eat_129=Catch1_129 & [Eat_176=Catch1_176 & [Eat_49=Catch1_49 & [Eat_6=Catch1_6 & [Eat_77=Catch1_77 & [Eat_171=Catch1_171 & [Eat_83=Catch1_83 & [Eat_10=Catch1_10 & [Eat_125=Catch1_125 & [Eat_182=Catch1_182 & [Eat_188=Catch1_188 & [Eat_142=Catch1_142 & [Eat_147=Catch1_147 & [Eat_67=Catch1_67 & [Eat_62=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_12_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[Think_121=Catch1_121 & [[[[[[[[[Think_17=Catch1_17 & [[[[[[[[[[[[[[[[[[[[Think_75=Catch1_75 & [[[Think_189=Catch1_189 & [[[[[[[[[[[[[[Think_195=Catch1_195 & [[[[[[Think_100=Catch1_100 & [[[[[[[[Think_10=Catch1_10 & [[[Think_28=Catch1_28 & [[[[[[[[[[[[[[Think_178=Catch1_178 & [[[[[[Think_137=Catch1_137 & [[[[[[[[[[[Think_94=Catch1_94 & [[[Think_124=Catch1_124 & [[[Think_119=Catch1_119 & [[[[[[[[Think_92=Catch1_92 & [[[[[[Think_166=Catch1_166 & [[[[[[[[[[[[[[Think_56=Catch1_56 & [[[[[[[[[[[[[[[[[[[[[[Think_53=Catch1_53 & [[[[[[[[Think_114=Catch1_114 & [[[[[[[[[[[[[[[[[[[Think_136=Catch1_136 & [[[[[[[[Think_83=Catch1_83 & [[[[[[[[Think_77=Catch1_77 & [[[[true & Think_130=Catch1_130] & Think_78=Catch1_78] & Think_161=Catch1_161] & Think_66=Catch1_66]] & Think_39=Catch1_39] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148] & Think_15=Catch1_15]] & Think_159=Catch1_159] & Think_44=Catch1_44] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95] & Think_7=Catch1_7] & Think_116=Catch1_116]] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68] & Think_21=Catch1_21] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36] & Think_25=Catch1_25] & Think_86=Catch1_86] & Think_65=Catch1_65] & Think_16=Catch1_16] & Think_163=Catch1_163] & Think_115=Catch1_115] & Think_73=Catch1_73] & Think_102=Catch1_102]] & Think_23=Catch1_23] & Think_108=Catch1_108] & Think_190=Catch1_190] & Think_80=Catch1_80] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140]] & Think_179=Catch1_179] & Think_33=Catch1_33] & Think_22=Catch1_22] & Think_187=Catch1_187] & Think_104=Catch1_104] & Think_177=Catch1_177] & Think_191=Catch1_191] & Think_169=Catch1_169] & Think_192=Catch1_192] & Think_8=Catch1_8] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71] & Think_141=Catch1_141] & Think_193=Catch1_193] & Think_74=Catch1_74] & Think_38=Catch1_38] & Think_51=Catch1_51] & Think_59=Catch1_59] & Think_188=Catch1_188] & Think_43=Catch1_43]] & Think_186=Catch1_186] & Think_32=Catch1_32] & Think_79=Catch1_79] & Think_5=Catch1_5] & Think_173=Catch1_173] & Think_62=Catch1_62] & Think_26=Catch1_26] & Think_118=Catch1_118] & Think_63=Catch1_63] & Think_99=Catch1_99] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162]] & Think_93=Catch1_93] & Think_98=Catch1_98] & Think_70=Catch1_70] & Think_4=Catch1_4] & Think_175=Catch1_175]] & Think_120=Catch1_120] & Think_89=Catch1_89] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31] & Think_97=Catch1_97]] & Think_133=Catch1_133] & Think_49=Catch1_49]] & Think_45=Catch1_45] & Think_153=Catch1_153]] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3] & Think_81=Catch1_81] & Think_122=Catch1_122] & Think_117=Catch1_117] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27]] & Think_176=Catch1_176] & Think_197=Catch1_197] & Think_96=Catch1_96] & Think_54=Catch1_54] & Think_164=Catch1_164]] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58] & Think_155=Catch1_155] & Think_184=Catch1_184] & Think_170=Catch1_170] & Think_158=Catch1_158] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181] & Think_30=Catch1_30] & Think_149=Catch1_149] & Think_142=Catch1_142]] & Think_194=Catch1_194] & Think_76=Catch1_76]] & Think_150=Catch1_150] & Think_40=Catch1_40] & Think_103=Catch1_103] & Think_91=Catch1_91] & Think_88=Catch1_88] & Think_20=Catch1_20] & Think_101=Catch1_101]] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152]] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72] & Think_128=Catch1_128] & Think_14=Catch1_14] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154] & Think_18=Catch1_18] & Think_46=Catch1_46] & Think_61=Catch1_61] & Think_143=Catch1_143]] & Think_156=Catch1_156] & Think_123=Catch1_123]] & Think_52=Catch1_52] & Think_198=Catch1_198] & Think_157=Catch1_157] & Think_112=Catch1_112] & Think_146=Catch1_146] & Think_12=Catch1_12] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87] & Think_1=Catch1_1] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34] & Think_160=Catch1_160] & Think_11=Catch1_11] & Think_19=Catch1_19] & Think_139=Catch1_139] & Think_50=Catch1_50] & Think_2=Catch1_2]] & Think_111=Catch1_111] & Think_57=Catch1_57] & Think_134=Catch1_134] & Think_82=Catch1_82] & Think_144=Catch1_144] & Think_90=Catch1_90] & Think_138=Catch1_138] & Think_168=Catch1_168]] & Think_9=Catch1_9] & Think_127=Catch1_127] | [[[[[[Eat_73=Catch1_73 & [[[[Eat_33=Catch1_33 & [[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_117=Catch1_117 & [[[[[[[[[[[Eat_79=Catch1_79 & [[[[[[[[[[[[[[[[[[Eat_28=Catch1_28 & [[[[[[[[[[[[[[[[[[Eat_185=Catch1_185 & [[[[[[[Eat_32=Catch1_32 & [[[[[[[[[[[Eat_56=Catch1_56 & [[[Eat_123=Catch1_123 & [[[[[[[[[[[[[[Eat_160=Catch1_160 & [[[[[[[[[[Eat_131=Catch1_131 & [[[[[[Eat_20=Catch1_20 & [[[[[[[Eat_54=Catch1_54 & [[[Eat_61=Catch1_61 & [[[Eat_5=Catch1_5 & [[[[[[[[[[[[[Eat_162=Catch1_162 & [[[[[[Eat_138=Catch1_138 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_62=Catch1_62 & true] & Eat_67=Catch1_67] & Eat_147=Catch1_147] & Eat_142=Catch1_142] & Eat_188=Catch1_188] & Eat_182=Catch1_182] & Eat_125=Catch1_125] & Eat_10=Catch1_10] & Eat_83=Catch1_83] & Eat_171=Catch1_171] & Eat_77=Catch1_77] & Eat_6=Catch1_6] & Eat_49=Catch1_49] & Eat_176=Catch1_176] & Eat_129=Catch1_129] & Eat_148=Catch1_148] & Eat_107=Catch1_107] & Eat_174=Catch1_174] & Eat_153=Catch1_153] & Eat_91=Catch1_91] & Eat_109=Catch1_109] & Eat_68=Catch1_68] & Eat_200=Catch1_200] & Eat_195=Catch1_195] & Eat_183=Catch1_183] & Eat_7=Catch1_7] & Eat_164=Catch1_164] & Eat_45=Catch1_45] & Eat_2=Catch1_2] & Eat_191=Catch1_191] & Eat_190=Catch1_190] & Eat_37=Catch1_37] & Eat_96=Catch1_96]] & Eat_137=Catch1_137] & Eat_181=Catch1_181] & Eat_170=Catch1_170] & Eat_127=Catch1_127] & Eat_24=Catch1_24]] & Eat_69=Catch1_69] & Eat_139=Catch1_139] & Eat_198=Catch1_198] & Eat_87=Catch1_87] & Eat_172=Catch1_172] & Eat_4=Catch1_4] & Eat_14=Catch1_14] & Eat_113=Catch1_113] & Eat_53=Catch1_53] & Eat_92=Catch1_92] & Eat_121=Catch1_121] & Eat_184=Catch1_184]] & Eat_86=Catch1_86] & Eat_11=Catch1_11]] & Eat_168=Catch1_168] & Eat_39=Catch1_39]] & Eat_44=Catch1_44] & Eat_111=Catch1_111] & Eat_64=Catch1_64] & Eat_100=Catch1_100] & Eat_101=Catch1_101] & Eat_120=Catch1_120]] & Eat_46=Catch1_46] & Eat_166=Catch1_166] & Eat_89=Catch1_89] & Eat_50=Catch1_50] & Eat_98=Catch1_98]] & Eat_132=Catch1_132] & Eat_17=Catch1_17] & Eat_106=Catch1_106] & Eat_156=Catch1_156] & Eat_178=Catch1_178] & Eat_47=Catch1_47] & Eat_71=Catch1_71] & Eat_21=Catch1_21] & Eat_150=Catch1_150]] & Eat_60=Catch1_60] & Eat_48=Catch1_48] & Eat_72=Catch1_72] & Eat_157=Catch1_157] & Eat_74=Catch1_74] & Eat_128=Catch1_128] & Eat_155=Catch1_155] & Eat_8=Catch1_8] & Eat_122=Catch1_122] & Eat_140=Catch1_140] & Eat_152=Catch1_152] & Eat_141=Catch1_141] & Eat_12=Catch1_12]] & Eat_93=Catch1_93] & Eat_143=Catch1_143]] & Eat_75=Catch1_75] & Eat_16=Catch1_16] & Eat_3=Catch1_3] & Eat_88=Catch1_88] & Eat_114=Catch1_114] & Eat_151=Catch1_151] & Eat_115=Catch1_115] & Eat_197=Catch1_197] & Eat_81=Catch1_81] & Eat_159=Catch1_159]] & Eat_36=Catch1_36] & Eat_192=Catch1_192] & Eat_13=Catch1_13] & Eat_165=Catch1_165] & Eat_194=Catch1_194] & Eat_25=Catch1_25]] & Eat_23=Catch1_23] & Eat_105=Catch1_105] & Eat_145=Catch1_145] & Eat_124=Catch1_124] & Eat_180=Catch1_180] & Eat_102=Catch1_102] & Eat_163=Catch1_163] & Eat_41=Catch1_41] & Eat_134=Catch1_134] & Eat_19=Catch1_19] & Eat_94=Catch1_94] & Eat_108=Catch1_108] & Eat_85=Catch1_85] & Eat_110=Catch1_110] & Eat_118=Catch1_118] & Eat_42=Catch1_42] & Eat_149=Catch1_149]] & Eat_99=Catch1_99] & Eat_30=Catch1_30] & Eat_199=Catch1_199] & Eat_31=Catch1_31] & Eat_135=Catch1_135] & Eat_103=Catch1_103] & Eat_90=Catch1_90] & Eat_34=Catch1_34] & Eat_167=Catch1_167] & Eat_119=Catch1_119] & Eat_82=Catch1_82] & Eat_52=Catch1_52] & Eat_40=Catch1_40] & Eat_133=Catch1_133] & Eat_173=Catch1_173] & Eat_80=Catch1_80] & Eat_112=Catch1_112]] & Eat_57=Catch1_57] & Eat_161=Catch1_161] & Eat_186=Catch1_186] & Eat_65=Catch1_65] & Eat_146=Catch1_146] & Eat_76=Catch1_76] & Eat_51=Catch1_51] & Eat_154=Catch1_154] & Eat_193=Catch1_193] & Eat_1=Catch1_1]] & Eat_177=Catch1_177] & Eat_70=Catch1_70] & Eat_26=Catch1_26] & Eat_78=Catch1_78] & Eat_43=Catch1_43] & Eat_18=Catch1_18] & Eat_126=Catch1_126] & Eat_189=Catch1_189] & Eat_104=Catch1_104] & Eat_179=Catch1_179] & Eat_144=Catch1_144] & Eat_175=Catch1_175] & Eat_27=Catch1_27] & Eat_29=Catch1_29] & Eat_63=Catch1_63] & Eat_38=Catch1_38] & Eat_97=Catch1_97] & Eat_9=Catch1_9] & Eat_84=Catch1_84] & Eat_158=Catch1_158] & Eat_196=Catch1_196] & Eat_35=Catch1_35] & Eat_116=Catch1_116] & Eat_15=Catch1_15] & Eat_187=Catch1_187] & Eat_136=Catch1_136]] & Eat_66=Catch1_66] & Eat_59=Catch1_59] & Eat_130=Catch1_130]] & Eat_22=Catch1_22] & Eat_55=Catch1_55] & Eat_169=Catch1_169] & Eat_95=Catch1_95] & Eat_58=Catch1_58]]]
normalized: ~ [E [true U ~ [[[Eat_58=Catch1_58 & [Eat_95=Catch1_95 & [Eat_169=Catch1_169 & [Eat_55=Catch1_55 & [Eat_22=Catch1_22 & [Eat_73=Catch1_73 & [Eat_130=Catch1_130 & [Eat_59=Catch1_59 & [Eat_66=Catch1_66 & [Eat_33=Catch1_33 & [Eat_136=Catch1_136 & [Eat_187=Catch1_187 & [Eat_15=Catch1_15 & [Eat_116=Catch1_116 & [Eat_35=Catch1_35 & [Eat_196=Catch1_196 & [Eat_158=Catch1_158 & [Eat_84=Catch1_84 & [Eat_9=Catch1_9 & [Eat_97=Catch1_97 & [Eat_38=Catch1_38 & [Eat_63=Catch1_63 & [Eat_29=Catch1_29 & [Eat_27=Catch1_27 & [Eat_175=Catch1_175 & [Eat_144=Catch1_144 & [Eat_179=Catch1_179 & [Eat_104=Catch1_104 & [Eat_189=Catch1_189 & [Eat_126=Catch1_126 & [Eat_18=Catch1_18 & [Eat_43=Catch1_43 & [Eat_78=Catch1_78 & [Eat_26=Catch1_26 & [Eat_70=Catch1_70 & [Eat_177=Catch1_177 & [Eat_117=Catch1_117 & [Eat_1=Catch1_1 & [Eat_193=Catch1_193 & [Eat_154=Catch1_154 & [Eat_51=Catch1_51 & [Eat_76=Catch1_76 & [Eat_146=Catch1_146 & [Eat_65=Catch1_65 & [Eat_186=Catch1_186 & [Eat_161=Catch1_161 & [Eat_57=Catch1_57 & [Eat_79=Catch1_79 & [Eat_112=Catch1_112 & [Eat_80=Catch1_80 & [Eat_173=Catch1_173 & [Eat_133=Catch1_133 & [Eat_40=Catch1_40 & [Eat_52=Catch1_52 & [Eat_82=Catch1_82 & [Eat_119=Catch1_119 & [Eat_167=Catch1_167 & [Eat_34=Catch1_34 & [Eat_90=Catch1_90 & [Eat_103=Catch1_103 & [Eat_135=Catch1_135 & [Eat_31=Catch1_31 & [Eat_199=Catch1_199 & [Eat_30=Catch1_30 & [Eat_99=Catch1_99 & [Eat_28=Catch1_28 & [Eat_149=Catch1_149 & [Eat_42=Catch1_42 & [Eat_118=Catch1_118 & [Eat_110=Catch1_110 & [Eat_85=Catch1_85 & [Eat_108=Catch1_108 & [Eat_94=Catch1_94 & [Eat_19=Catch1_19 & [Eat_134=Catch1_134 & [Eat_41=Catch1_41 & [Eat_163=Catch1_163 & [Eat_102=Catch1_102 & [Eat_180=Catch1_180 & [Eat_124=Catch1_124 & [Eat_145=Catch1_145 & [Eat_105=Catch1_105 & [Eat_23=Catch1_23 & [Eat_185=Catch1_185 & [Eat_25=Catch1_25 & [Eat_194=Catch1_194 & [Eat_165=Catch1_165 & [Eat_13=Catch1_13 & [Eat_192=Catch1_192 & [Eat_36=Catch1_36 & [Eat_32=Catch1_32 & [Eat_159=Catch1_159 & [Eat_81=Catch1_81 & [Eat_197=Catch1_197 & [Eat_115=Catch1_115 & [Eat_151=Catch1_151 & [Eat_114=Catch1_114 & [Eat_88=Catch1_88 & [Eat_3=Catch1_3 & [Eat_16=Catch1_16 & [Eat_75=Catch1_75 & [Eat_56=Catch1_56 & [Eat_143=Catch1_143 & [Eat_93=Catch1_93 & [Eat_123=Catch1_123 & [Eat_12=Catch1_12 & [Eat_141=Catch1_141 & [Eat_152=Catch1_152 & [Eat_140=Catch1_140 & [Eat_122=Catch1_122 & [Eat_8=Catch1_8 & [Eat_155=Catch1_155 & [Eat_128=Catch1_128 & [Eat_74=Catch1_74 & [Eat_157=Catch1_157 & [Eat_72=Catch1_72 & [Eat_48=Catch1_48 & [Eat_60=Catch1_60 & [Eat_160=Catch1_160 & [Eat_150=Catch1_150 & [Eat_21=Catch1_21 & [Eat_71=Catch1_71 & [Eat_47=Catch1_47 & [Eat_178=Catch1_178 & [Eat_156=Catch1_156 & [Eat_106=Catch1_106 & [Eat_17=Catch1_17 & [Eat_132=Catch1_132 & [Eat_131=Catch1_131 & [Eat_98=Catch1_98 & [Eat_50=Catch1_50 & [Eat_89=Catch1_89 & [Eat_166=Catch1_166 & [Eat_46=Catch1_46 & [Eat_20=Catch1_20 & [Eat_120=Catch1_120 & [Eat_101=Catch1_101 & [Eat_100=Catch1_100 & [Eat_64=Catch1_64 & [Eat_111=Catch1_111 & [Eat_44=Catch1_44 & [Eat_54=Catch1_54 & [Eat_39=Catch1_39 & [Eat_168=Catch1_168 & [Eat_61=Catch1_61 & [Eat_11=Catch1_11 & [Eat_86=Catch1_86 & [Eat_5=Catch1_5 & [Eat_184=Catch1_184 & [Eat_121=Catch1_121 & [Eat_92=Catch1_92 & [Eat_53=Catch1_53 & [Eat_113=Catch1_113 & [Eat_14=Catch1_14 & [Eat_4=Catch1_4 & [Eat_172=Catch1_172 & [Eat_87=Catch1_87 & [Eat_198=Catch1_198 & [Eat_139=Catch1_139 & [Eat_69=Catch1_69 & [Eat_162=Catch1_162 & [Eat_24=Catch1_24 & [Eat_127=Catch1_127 & [Eat_170=Catch1_170 & [Eat_181=Catch1_181 & [Eat_137=Catch1_137 & [Eat_138=Catch1_138 & [Eat_96=Catch1_96 & [Eat_37=Catch1_37 & [Eat_190=Catch1_190 & [Eat_191=Catch1_191 & [Eat_2=Catch1_2 & [Eat_45=Catch1_45 & [Eat_164=Catch1_164 & [Eat_7=Catch1_7 & [Eat_183=Catch1_183 & [Eat_195=Catch1_195 & [Eat_200=Catch1_200 & [Eat_68=Catch1_68 & [Eat_109=Catch1_109 & [Eat_91=Catch1_91 & [Eat_153=Catch1_153 & [Eat_174=Catch1_174 & [Eat_107=Catch1_107 & [Eat_148=Catch1_148 & [Eat_129=Catch1_129 & [Eat_176=Catch1_176 & [Eat_49=Catch1_49 & [Eat_6=Catch1_6 & [Eat_77=Catch1_77 & [Eat_171=Catch1_171 & [Eat_83=Catch1_83 & [Eat_10=Catch1_10 & [Eat_125=Catch1_125 & [Eat_182=Catch1_182 & [Eat_188=Catch1_188 & [Eat_142=Catch1_142 & [Eat_147=Catch1_147 & [Eat_67=Catch1_67 & [Eat_62=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_13_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_92=Catch1_92 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_8=Catch1_8 & [[[[[Think_104=Catch1_104 & [[[[[Think_53=Catch1_53 & [[[[[Think_190=Catch1_190 & [[[[[Think_73=Catch1_73 & [[[[[[[[[[[[[[[[[[[Think_7=Catch1_7 & [[[[[[[[[[[[[[[[[Think_78=Catch1_78 & [true & Think_130=Catch1_130]] & Think_161=Catch1_161] & Think_66=Catch1_66] & Think_77=Catch1_77] & Think_39=Catch1_39] & Think_67=Catch1_67] & Think_35=Catch1_35] & Think_125=Catch1_125] & Think_85=Catch1_85] & Think_148=Catch1_148] & Think_15=Catch1_15] & Think_83=Catch1_83] & Think_159=Catch1_159] & Think_44=Catch1_44] & Think_55=Catch1_55] & Think_64=Catch1_64] & Think_95=Catch1_95]] & Think_116=Catch1_116] & Think_136=Catch1_136] & Think_113=Catch1_113] & Think_200=Catch1_200] & Think_68=Catch1_68] & Think_21=Catch1_21] & Think_29=Catch1_29] & Think_69=Catch1_69] & Think_42=Catch1_42] & Think_183=Catch1_183] & Think_135=Catch1_135] & Think_36=Catch1_36] & Think_25=Catch1_25] & Think_86=Catch1_86] & Think_65=Catch1_65] & Think_16=Catch1_16] & Think_163=Catch1_163] & Think_115=Catch1_115]] & Think_102=Catch1_102] & Think_114=Catch1_114] & Think_23=Catch1_23] & Think_108=Catch1_108]] & Think_80=Catch1_80] & Think_13=Catch1_13] & Think_41=Catch1_41] & Think_140=Catch1_140]] & Think_179=Catch1_179] & Think_33=Catch1_33] & Think_22=Catch1_22] & Think_187=Catch1_187]] & Think_177=Catch1_177] & Think_191=Catch1_191] & Think_169=Catch1_169] & Think_192=Catch1_192]] & Think_84=Catch1_84] & Think_185=Catch1_185] & Think_71=Catch1_71] & Think_141=Catch1_141] & Think_193=Catch1_193] & Think_74=Catch1_74] & Think_38=Catch1_38] & Think_51=Catch1_51] & Think_59=Catch1_59] & Think_188=Catch1_188] & Think_43=Catch1_43] & Think_56=Catch1_56] & Think_186=Catch1_186] & Think_32=Catch1_32] & Think_79=Catch1_79] & Think_5=Catch1_5] & Think_173=Catch1_173] & Think_62=Catch1_62] & Think_26=Catch1_26] & Think_118=Catch1_118] & Think_63=Catch1_63] & Think_99=Catch1_99] & Think_37=Catch1_37] & Think_60=Catch1_60] & Think_162=Catch1_162] & Think_166=Catch1_166] & Think_93=Catch1_93] & Think_98=Catch1_98] & Think_70=Catch1_70] & Think_4=Catch1_4] & Think_175=Catch1_175]] & Think_120=Catch1_120] & Think_89=Catch1_89] & Think_167=Catch1_167] & Think_129=Catch1_129] & Think_196=Catch1_196] & Think_31=Catch1_31] & Think_97=Catch1_97] & Think_119=Catch1_119] & Think_133=Catch1_133] & Think_49=Catch1_49] & Think_124=Catch1_124] & Think_45=Catch1_45] & Think_153=Catch1_153] & Think_94=Catch1_94] & Think_126=Catch1_126] & Think_109=Catch1_109] & Think_3=Catch1_3] & Think_81=Catch1_81] & Think_122=Catch1_122] & Think_117=Catch1_117] & Think_107=Catch1_107] & Think_105=Catch1_105] & Think_180=Catch1_180] & Think_27=Catch1_27] & Think_137=Catch1_137] & Think_176=Catch1_176] & Think_197=Catch1_197] & Think_96=Catch1_96] & Think_54=Catch1_54] & Think_164=Catch1_164] & Think_178=Catch1_178] & Think_132=Catch1_132] & Think_174=Catch1_174] & Think_58=Catch1_58] & Think_155=Catch1_155] & Think_184=Catch1_184] & Think_170=Catch1_170] & Think_158=Catch1_158] & Think_147=Catch1_147] & Think_24=Catch1_24] & Think_181=Catch1_181] & Think_30=Catch1_30] & Think_149=Catch1_149] & Think_142=Catch1_142] & Think_28=Catch1_28] & Think_194=Catch1_194] & Think_76=Catch1_76] & Think_10=Catch1_10] & Think_150=Catch1_150] & Think_40=Catch1_40] & Think_103=Catch1_103] & Think_91=Catch1_91] & Think_88=Catch1_88] & Think_20=Catch1_20] & Think_101=Catch1_101] & Think_100=Catch1_100] & Think_48=Catch1_48] & Think_110=Catch1_110] & Think_171=Catch1_171] & Think_47=Catch1_47] & Think_152=Catch1_152] & Think_195=Catch1_195] & Think_151=Catch1_151] & Think_165=Catch1_165] & Think_182=Catch1_182] & Think_72=Catch1_72] & Think_128=Catch1_128] & Think_14=Catch1_14] & Think_199=Catch1_199] & Think_106=Catch1_106] & Think_154=Catch1_154] & Think_18=Catch1_18] & Think_46=Catch1_46] & Think_61=Catch1_61] & Think_143=Catch1_143] & Think_189=Catch1_189] & Think_156=Catch1_156] & Think_123=Catch1_123] & Think_75=Catch1_75] & Think_52=Catch1_52] & Think_198=Catch1_198] & Think_157=Catch1_157] & Think_112=Catch1_112] & Think_146=Catch1_146] & Think_12=Catch1_12] & Think_145=Catch1_145] & Think_172=Catch1_172] & Think_87=Catch1_87] & Think_1=Catch1_1] & Think_131=Catch1_131] & Think_6=Catch1_6] & Think_34=Catch1_34] & Think_160=Catch1_160] & Think_11=Catch1_11] & Think_19=Catch1_19] & Think_139=Catch1_139] & Think_50=Catch1_50] & Think_2=Catch1_2] & Think_17=Catch1_17] & Think_111=Catch1_111] & Think_57=Catch1_57] & Think_134=Catch1_134] & Think_82=Catch1_82] & Think_144=Catch1_144] & Think_90=Catch1_90] & Think_138=Catch1_138] & Think_168=Catch1_168] & Think_121=Catch1_121] & Think_9=Catch1_9] & Think_127=Catch1_127] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_77=Catch1_77 & [[[[[[[[[[true & Eat_62=Catch1_62] & Eat_67=Catch1_67] & Eat_147=Catch1_147] & Eat_142=Catch1_142] & Eat_188=Catch1_188] & Eat_182=Catch1_182] & Eat_125=Catch1_125] & Eat_10=Catch1_10] & Eat_83=Catch1_83] & Eat_171=Catch1_171]] & Eat_6=Catch1_6] & Eat_49=Catch1_49] & Eat_176=Catch1_176] & Eat_129=Catch1_129] & Eat_148=Catch1_148] & Eat_107=Catch1_107] & Eat_174=Catch1_174] & Eat_153=Catch1_153] & Eat_91=Catch1_91] & Eat_109=Catch1_109] & Eat_68=Catch1_68] & Eat_200=Catch1_200] & Eat_195=Catch1_195] & Eat_183=Catch1_183] & Eat_7=Catch1_7] & Eat_164=Catch1_164] & Eat_45=Catch1_45] & Eat_2=Catch1_2] & Eat_191=Catch1_191] & Eat_190=Catch1_190] & Eat_37=Catch1_37] & Eat_96=Catch1_96] & Eat_138=Catch1_138] & Eat_137=Catch1_137] & Eat_181=Catch1_181] & Eat_170=Catch1_170] & Eat_127=Catch1_127] & Eat_24=Catch1_24] & Eat_162=Catch1_162] & Eat_69=Catch1_69] & Eat_139=Catch1_139] & Eat_198=Catch1_198] & Eat_87=Catch1_87] & Eat_172=Catch1_172] & Eat_4=Catch1_4] & Eat_14=Catch1_14] & Eat_113=Catch1_113] & Eat_53=Catch1_53] & Eat_92=Catch1_92] & Eat_121=Catch1_121] & Eat_184=Catch1_184] & Eat_5=Catch1_5] & Eat_86=Catch1_86] & Eat_11=Catch1_11] & Eat_61=Catch1_61] & Eat_168=Catch1_168] & Eat_39=Catch1_39] & Eat_54=Catch1_54] & Eat_44=Catch1_44] & Eat_111=Catch1_111] & Eat_64=Catch1_64] & Eat_100=Catch1_100] & Eat_101=Catch1_101] & Eat_120=Catch1_120] & Eat_20=Catch1_20] & Eat_46=Catch1_46] & Eat_166=Catch1_166] & Eat_89=Catch1_89] & Eat_50=Catch1_50] & Eat_98=Catch1_98] & Eat_131=Catch1_131] & Eat_132=Catch1_132] & Eat_17=Catch1_17] & Eat_106=Catch1_106] & Eat_156=Catch1_156] & Eat_178=Catch1_178] & Eat_47=Catch1_47] & Eat_71=Catch1_71] & Eat_21=Catch1_21] & Eat_150=Catch1_150] & Eat_160=Catch1_160] & Eat_60=Catch1_60] & Eat_48=Catch1_48] & Eat_72=Catch1_72] & Eat_157=Catch1_157] & Eat_74=Catch1_74] & Eat_128=Catch1_128] & Eat_155=Catch1_155] & Eat_8=Catch1_8] & Eat_122=Catch1_122] & Eat_140=Catch1_140] & Eat_152=Catch1_152] & Eat_141=Catch1_141] & Eat_12=Catch1_12] & Eat_123=Catch1_123] & Eat_93=Catch1_93] & Eat_143=Catch1_143] & Eat_56=Catch1_56] & Eat_75=Catch1_75] & Eat_16=Catch1_16] & Eat_3=Catch1_3] & Eat_88=Catch1_88] & Eat_114=Catch1_114] & Eat_151=Catch1_151] & Eat_115=Catch1_115] & Eat_197=Catch1_197] & Eat_81=Catch1_81] & Eat_159=Catch1_159] & Eat_32=Catch1_32] & Eat_36=Catch1_36] & Eat_192=Catch1_192] & Eat_13=Catch1_13] & Eat_165=Catch1_165] & Eat_194=Catch1_194] & Eat_25=Catch1_25] & Eat_185=Catch1_185] & Eat_23=Catch1_23] & Eat_105=Catch1_105] & Eat_145=Catch1_145] & Eat_124=Catch1_124] & Eat_180=Catch1_180] & Eat_102=Catch1_102] & Eat_163=Catch1_163] & Eat_41=Catch1_41] & Eat_134=Catch1_134] & Eat_19=Catch1_19] & Eat_94=Catch1_94] & Eat_108=Catch1_108] & Eat_85=Catch1_85] & Eat_110=Catch1_110] & Eat_118=Catch1_118] & Eat_42=Catch1_42] & Eat_149=Catch1_149] & Eat_28=Catch1_28] & Eat_99=Catch1_99] & Eat_30=Catch1_30] & Eat_199=Catch1_199] & Eat_31=Catch1_31] & Eat_135=Catch1_135] & Eat_103=Catch1_103] & Eat_90=Catch1_90] & Eat_34=Catch1_34] & Eat_167=Catch1_167] & Eat_119=Catch1_119] & Eat_82=Catch1_82] & Eat_52=Catch1_52] & Eat_40=Catch1_40] & Eat_133=Catch1_133] & Eat_173=Catch1_173] & Eat_80=Catch1_80] & Eat_112=Catch1_112] & Eat_79=Catch1_79] & Eat_57=Catch1_57] & Eat_161=Catch1_161] & Eat_186=Catch1_186] & Eat_65=Catch1_65] & Eat_146=Catch1_146] & Eat_76=Catch1_76] & Eat_51=Catch1_51] & Eat_154=Catch1_154] & Eat_193=Catch1_193] & Eat_1=Catch1_1] & Eat_117=Catch1_117] & Eat_177=Catch1_177] & Eat_70=Catch1_70] & Eat_26=Catch1_26] & Eat_78=Catch1_78] & Eat_43=Catch1_43] & Eat_18=Catch1_18] & Eat_126=Catch1_126] & Eat_189=Catch1_189] & Eat_104=Catch1_104] & Eat_179=Catch1_179] & Eat_144=Catch1_144] & Eat_175=Catch1_175] & Eat_27=Catch1_27] & Eat_29=Catch1_29] & Eat_63=Catch1_63] & Eat_38=Catch1_38] & Eat_97=Catch1_97] & Eat_9=Catch1_9] & Eat_84=Catch1_84] & Eat_158=Catch1_158] & Eat_196=Catch1_196] & Eat_35=Catch1_35] & Eat_116=Catch1_116] & Eat_15=Catch1_15] & Eat_187=Catch1_187] & Eat_136=Catch1_136] & Eat_33=Catch1_33] & Eat_66=Catch1_66] & Eat_59=Catch1_59] & Eat_130=Catch1_130] & Eat_73=Catch1_73] & Eat_22=Catch1_22] & Eat_55=Catch1_55] & Eat_169=Catch1_169] & Eat_95=Catch1_95] & Eat_58=Catch1_58]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_65=Catch1_65 & [Eat_186=Catch1_186 & [Eat_161=Catch1_161 & [Eat_57=Catch1_57 & [Eat_79=Catch1_79 & [Eat_112=Catch1_112 & [Eat_80=Catch1_80 & [Eat_173=Catch1_173 & [Eat_133=Catch1_133 & [Eat_40=Catch1_40 & [Eat_52=Catch1_52 & [Eat_82=Catch1_82 & [Eat_119=Catch1_119 & [Eat_167=Catch1_167 & [Eat_34=Catch1_34 & [Eat_90=Catch1_90 & [Eat_103=Catch1_103 & [Eat_135=Catch1_135 & [Eat_31=Catch1_31 & [Eat_199=Catch1_199 & [Eat_30=Catch1_30 & [Eat_99=Catch1_99 & [Eat_28=Catch1_28 & [Eat_149=Catch1_149 & [Eat_42=Catch1_42 & [Eat_118=Catch1_118 & [Eat_110=Catch1_110 & [Eat_85=Catch1_85 & [Eat_108=Catch1_108 & [Eat_94=Catch1_94 & [Eat_19=Catch1_19 & [Eat_134=Catch1_134 & [Eat_41=Catch1_41 & [Eat_163=Catch1_163 & [Eat_102=Catch1_102 & [Eat_180=Catch1_180 & [Eat_124=Catch1_124 & [Eat_145=Catch1_145 & [Eat_105=Catch1_105 & [Eat_23=Catch1_23 & [Eat_185=Catch1_185 & [Eat_25=Catch1_25 & [Eat_194=Catch1_194 & [Eat_165=Catch1_165 & [Eat_13=Catch1_13 & [Eat_192=Catch1_192 & [Eat_36=Catch1_36 & [Eat_32=Catch1_32 & [Eat_159=Catch1_159 & [Eat_81=Catch1_81 & [Eat_197=Catch1_197 & [Eat_115=Catch1_115 & [Eat_151=Catch1_151 & [Eat_114=Catch1_114 & [Eat_88=Catch1_88 & [Eat_3=Catch1_3 & [Eat_16=Catch1_16 & [Eat_75=Catch1_75 & [Eat_56=Catch1_56 & [Eat_143=Catch1_143 & [Eat_93=Catch1_93 & [Eat_123=Catch1_123 & [Eat_12=Catch1_12 & [Eat_141=Catch1_141 & [Eat_152=Catch1_152 & [Eat_140=Catch1_140 & [Eat_122=Catch1_122 & [Eat_8=Catch1_8 & [Eat_155=Catch1_155 & [Eat_128=Catch1_128 & [Eat_74=Catch1_74 & [Eat_157=Catch1_157 & [Eat_72=Catch1_72 & [Eat_48=Catch1_48 & [Eat_60=Catch1_60 & [Eat_160=Catch1_160 & [Eat_150=Catch1_150 & [Eat_21=Catch1_21 & [Eat_71=Catch1_71 & [Eat_47=Catch1_47 & [Eat_178=Catch1_178 & [Eat_156=Catch1_156 & [Eat_106=Catch1_106 & [Eat_17=Catch1_17 & [Eat_132=Catch1_132 & [Eat_131=Catch1_131 & [Eat_98=Catch1_98 & [Eat_50=Catch1_50 & [Eat_89=Catch1_89 & [Eat_166=Catch1_166 & [Eat_46=Catch1_46 & [Eat_20=Catch1_20 & [Eat_120=Catch1_120 & [Eat_101=Catch1_101 & [Eat_100=Catch1_100 & [Eat_64=Catch1_64 & [Eat_111=Catch1_111 & [Eat_44=Catch1_44 & [Eat_54=Catch1_54 & [Eat_39=Catch1_39 & [Eat_168=Catch1_168 & [Eat_61=Catch1_61 & [Eat_11=Catch1_11 & [Eat_86=Catch1_86 & [Eat_5=Catch1_5 & [Eat_184=Catch1_184 & [Eat_121=Catch1_121 & [Eat_92=Catch1_92 & [Eat_53=Catch1_53 & [Eat_113=Catch1_113 & [Eat_14=Catch1_14 & [Eat_4=Catch1_4 & [Eat_172=Catch1_172 & [Eat_87=Catch1_87 & [Eat_198=Catch1_198 & [Eat_139=Catch1_139 & [Eat_69=Catch1_69 & [Eat_162=Catch1_162 & [Eat_24=Catch1_24 & [Eat_127=Catch1_127 & [Eat_170=Catch1_170 & [Eat_181=Catch1_181 & [Eat_137=Catch1_137 & [Eat_138=Catch1_138 & [Eat_96=Catch1_96 & [Eat_37=Catch1_37 & [Eat_190=Catch1_190 & [Eat_191=Catch1_191 & [Eat_2=Catch1_2 & [Eat_45=Catch1_45 & [Eat_164=Catch1_164 & [Eat_7=Catch1_7 & [Eat_183=Catch1_183 & [Eat_195=Catch1_195 & [Eat_200=Catch1_200 & [Eat_68=Catch1_68 & [Eat_109=Catch1_109 & [Eat_91=Catch1_91 & [Eat_153=Catch1_153 & [Eat_174=Catch1_174 & [Eat_107=Catch1_107 & [Eat_148=Catch1_148 & [Eat_129=Catch1_129 & [Eat_176=Catch1_176 & [Eat_49=Catch1_49 & [Eat_6=Catch1_6 & [Eat_77=Catch1_77 & [Eat_171=Catch1_171 & [Eat_83=Catch1_83 & [Eat_10=Catch1_10 & [Eat_125=Catch1_125 & [Eat_182=Catch1_182 & [Eat_188=Catch1_188 & [Eat_142=Catch1_142 & [Eat_147=Catch1_147 & [Eat_67=Catch1_67 & [Eat_62=Catch1_62 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Eat_146=Catch1_146] & Eat_76=Catch1_76] & Eat_51=Catch1_51] & Eat_154=Catch1_154] & Eat_193=Catch1_193] & Eat_1=Catch1_1] & Eat_117=Catch1_117] & Eat_177=Catch1_177] & Eat_70=Catch1_70] & Eat_26=Catch1_26] & Eat_78=Catch1_78] & Eat_43=Catch1_43] & Eat_18=Catch1_18] & Eat_126=Catch1_126] & Eat_189=Catch1_189] & Eat_104=Catch1_104] & Eat_179=Catch1_179] & Eat_144=Catch1_144] & Eat_175=Catch1_175] & Eat_27=Catch1_27] & Eat_29=Catch1_29] & Eat_63=Catch1_63] & Eat_38=Catch1_38] & Eat_97=Catch1_97] & Eat_9=Catch1_9] & Eat_84=Catch1_84] & Eat_158=Catch1_158] & Eat_196=Catch1_196] & Eat_35=Catch1_35] & Eat_116=Catch1_116] & Eat_15=Catch1_15] & Eat_187=Catch1_187] & Eat_136=Catch1_136] & Eat_33=Catch1_33] & Eat_66=Catch1_66] & Eat_59=Catch1_59] & Eat_130=Catch1_130] & Eat_73=Catch1_73] & Eat_22=Catch1_22] & Eat_55=Catch1_55] & Eat_169=Catch1_169] & Eat_95=Catch1_95] & Eat_58=Catch1_58] & [Think_127=Catch1_127 & [Think_9=Catch1_9 & [Think_121=Catch1_121 & [Think_168=Catch1_168 & [Think_138=Catch1_138 & [Think_90=Catch1_90 & [Think_144=Catch1_144 & [Think_82=Catch1_82 & [Think_134=Catch1_134 & [Think_57=Catch1_57 & [Think_111=Catch1_111 & [Think_17=Catch1_17 & [Think_2=Catch1_2 & [Think_50=Catch1_50 & [Think_139=Catch1_139 & [Think_19=Catch1_19 & [Think_11=Catch1_11 & [Think_160=Catch1_160 & [Think_34=Catch1_34 & [Think_6=Catch1_6 & [Think_131=Catch1_131 & [Think_1=Catch1_1 & [Think_87=Catch1_87 & [Think_172=Catch1_172 & [Think_145=Catch1_145 & [Think_12=Catch1_12 & [Think_146=Catch1_146 & [Think_112=Catch1_112 & [Think_157=Catch1_157 & [Think_198=Catch1_198 & [Think_52=Catch1_52 & [Think_75=Catch1_75 & [Think_123=Catch1_123 & [Think_156=Catch1_156 & [Think_189=Catch1_189 & [Think_143=Catch1_143 & [Think_61=Catch1_61 & [Think_46=Catch1_46 & [Think_18=Catch1_18 & [Think_154=Catch1_154 & [Think_106=Catch1_106 & [Think_199=Catch1_199 & [Think_14=Catch1_14 & [Think_128=Catch1_128 & [Think_72=Catch1_72 & [Think_182=Catch1_182 & [Think_165=Catch1_165 & [Think_151=Catch1_151 & [Think_195=Catch1_195 & [Think_152=Catch1_152 & [Think_47=Catch1_47 & [Think_171=Catch1_171 & [Think_110=Catch1_110 & [Think_48=Catch1_48 & [Think_100=Catch1_100 & [Think_101=Catch1_101 & [Think_20=Catch1_20 & [Think_88=Catch1_88 & [Think_91=Catch1_91 & [Think_103=Catch1_103 & [Think_40=Catch1_40 & [Think_150=Catch1_150 & [Think_10=Catch1_10 & [Think_76=Catch1_76 & [Think_194=Catch1_194 & [Think_28=Catch1_28 & [Think_142=Catch1_142 & [Think_149=Catch1_149 & [Think_30=Catch1_30 & [Think_181=Catch1_181 & [Think_24=Catch1_24 & [Think_147=Catch1_147 & [Think_158=Catch1_158 & [Think_170=Catch1_170 & [Think_184=Catch1_184 & [Think_155=Catch1_155 & [Think_58=Catch1_58 & [Think_174=Catch1_174 & [Think_132=Catch1_132 & [Think_178=Catch1_178 & [Think_164=Catch1_164 & [Think_54=Catch1_54 & [Think_96=Catch1_96 & [Think_197=Catch1_197 & [Think_176=Catch1_176 & [Think_137=Catch1_137 & [Think_27=Catch1_27 & [Think_180=Catch1_180 & [Think_105=Catch1_105 & [Think_107=Catch1_107 & [Think_117=Catch1_117 & [Think_122=Catch1_122 & [Think_81=Catch1_81 & [Think_3=Catch1_3 & [Think_109=Catch1_109 & [Think_126=Catch1_126 & [Think_94=Catch1_94 & [Think_153=Catch1_153 & [Think_45=Catch1_45 & [Think_124=Catch1_124 & [Think_49=Catch1_49 & [Think_133=Catch1_133 & [Think_119=Catch1_119 & [Think_97=Catch1_97 & [Think_31=Catch1_31 & [Think_196=Catch1_196 & [Think_129=Catch1_129 & [Think_167=Catch1_167 & [Think_89=Catch1_89 & [Think_120=Catch1_120 & [Think_92=Catch1_92 & [Think_175=Catch1_175 & [Think_4=Catch1_4 & [Think_70=Catch1_70 & [Think_98=Catch1_98 & [Think_93=Catch1_93 & [Think_166=Catch1_166 & [Think_162=Catch1_162 & [Think_60=Catch1_60 & [Think_37=Catch1_37 & [Think_99=Catch1_99 & [Think_63=Catch1_63 & [Think_118=Catch1_118 & [Think_26=Catch1_26 & [Think_62=Catch1_62 & [Think_173=Catch1_173 & [Think_5=Catch1_5 & [Think_79=Catch1_79 & [Think_32=Catch1_32 & [Think_186=Catch1_186 & [Think_56=Catch1_56 & [Think_43=Catch1_43 & [Think_188=Catch1_188 & [Think_59=Catch1_59 & [Think_51=Catch1_51 & [Think_38=Catch1_38 & [Think_74=Catch1_74 & [Think_193=Catch1_193 & [Think_141=Catch1_141 & [Think_71=Catch1_71 & [Think_185=Catch1_185 & [Think_84=Catch1_84 & [Think_8=Catch1_8 & [Think_192=Catch1_192 & [Think_169=Catch1_169 & [Think_191=Catch1_191 & [Think_177=Catch1_177 & [Think_104=Catch1_104 & [Think_187=Catch1_187 & [Think_22=Catch1_22 & [Think_33=Catch1_33 & [Think_179=Catch1_179 & [Think_53=Catch1_53 & [Think_140=Catch1_140 & [Think_41=Catch1_41 & [Think_13=Catch1_13 & [Think_80=Catch1_80 & [Think_190=Catch1_190 & [Think_108=Catch1_108 & [Think_23=Catch1_23 & [Think_114=Catch1_114 & [Think_102=Catch1_102 & [Think_73=Catch1_73 & [Think_115=Catch1_115 & [Think_163=Catch1_163 & [Think_16=Catch1_16 & [Think_65=Catch1_65 & [Think_86=Catch1_86 & [Think_25=Catch1_25 & [Think_36=Catch1_36 & [Think_135=Catch1_135 & [Think_183=Catch1_183 & [Think_42=Catch1_42 & [Think_69=Catch1_69 & [Think_29=Catch1_29 & [Think_21=Catch1_21 & [Think_68=Catch1_68 & [Think_200=Catch1_200 & [Think_113=Catch1_113 & [Think_136=Catch1_136 & [Think_116=Catch1_116 & [Think_7=Catch1_7 & [Think_95=Catch1_95 & [Think_64=Catch1_64 & [Think_55=Catch1_55 & [Think_44=Catch1_44 & [Think_159=Catch1_159 & [Think_83=Catch1_83 & [Think_15=Catch1_15 & [Think_148=Catch1_148 & [Think_85=Catch1_85 & [Think_125=Catch1_125 & [Think_35=Catch1_35 & [Think_67=Catch1_67 & [Think_39=Catch1_39 & [Think_77=Catch1_77 & [Think_66=Catch1_66 & [Think_161=Catch1_161 & [Think_78=Catch1_78 & [Think_130=Catch1_130 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_14_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

total processing time: 0m21sec

STOP 1369698912

--------------------
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.1654: