Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

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

export BK_INPUT=Philosophers-PT-000200
export BK_EXAMINATION=ReachabilityMix
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1658
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 ReachabilityMix'
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=136968525100163_n_3)
=====================================================================
runnning marcie on Philosophers-PT-000200 (ReachabilityMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Philosophers-PT-000200, examination is ReachabilityMix
=====================================================================

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

START 1369708741

Marcie rev. 1103M (build: rohrch on 2013-02-17)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4 --mcc-file=ReachabilityMix.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 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 [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) & ["Think_139" \in [1, oo) && "Fork_138" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Fork_132" \in [1, oo) && "Think_133" \in [1, oo) | [["Think_173" \in [1, oo) && "Fork_172" \in [1, oo) | [[[[[[[[[["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | [["Fork_155" \in [1, oo) && "Think_156" \in [1, oo) | ["Fork_198" \in [1, oo) && "Think_199" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | [["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_197" \in [1, oo) && "Fork_196" \in [1, oo) | [["Think_171" \in [1, oo) && "Fork_170" \in [1, oo) | [[[["Fork_116" \in [1, oo) && "Think_117" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | [[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | ["Think_140" \in [1, oo) && "Fork_139" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_93" \in [1, oo) && "Think_94" \in [1, oo) | ["Fork_171" \in [1, oo) && "Think_172" \in [1, oo) | [["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [["Think_106" \in [1, oo) && "Fork_105" \in [1, oo) | ["Think_112" \in [1, oo) && "Fork_111" \in [1, oo) | ["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | [["Fork_55" \in [1, oo) && "Think_56" \in [1, oo) | ["Fork_127" \in [1, oo) && "Think_128" \in [1, oo) | ["Fork_82" \in [1, oo) && "Think_83" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | [["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | ["Think_113" \in [1, oo) && "Fork_112" \in [1, oo) | [["Think_110" \in [1, oo) && "Fork_109" \in [1, oo) | ["Think_101" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_131" \in [1, oo) && "Fork_130" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | [["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_196" \in [1, oo) && "Fork_195" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_52" \in [1, oo) && "Think_53" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | [[[["Think_162" \in [1, oo) && "Fork_161" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [[[[["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_192" \in [1, oo) && "Fork_191" \in [1, oo) | ["Think_120" \in [1, oo) && "Fork_119" \in [1, oo) | ["Think_190" \in [1, oo) && "Fork_189" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | [[[["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | [["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Think_105" \in [1, oo) && "Fork_104" \in [1, oo) | [[[[[[[["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | [[[["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | ["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | [[[["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | [["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Think_116" \in [1, oo) && "Fork_115" \in [1, oo) | [[["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | [[["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | [[["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | [["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | ["Think_109" \in [1, oo) && "Fork_108" \in [1, oo) | ["Fork_94" \in [1, oo) && "Think_95" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[[["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Think_145" \in [1, oo) && "Fork_144" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | ["Think_143" \in [1, oo) && "Fork_142" \in [1, oo) | ["Fork_120" \in [1, oo) && "Think_121" \in [1, oo) | [["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | ["Think_127" \in [1, oo) && "Fork_126" \in [1, oo) | ["Think_170" \in [1, oo) && "Fork_169" \in [1, oo) | ["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | [[["Think_161" \in [1, oo) && "Fork_160" \in [1, oo) | [["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | ["Think_187" \in [1, oo) && "Fork_186" \in [1, oo) | ["Fork_106" \in [1, oo) && "Think_107" \in [1, oo) | ["Think_136" \in [1, oo) && "Fork_135" \in [1, oo) | ["Fork_147" \in [1, oo) && "Think_148" \in [1, oo) | ["Think_163" \in [1, oo) && "Fork_162" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | [[["Fork_192" \in [1, oo) && "Think_193" \in [1, oo) | [["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_177" \in [1, oo) && "Fork_176" \in [1, oo) | [[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_67" \in [1, oo) && "Think_68" \in [1, oo) | ["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | [["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Think_165" \in [1, oo) && "Fork_164" \in [1, oo) | [[[["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | [["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | ["Fork_85" \in [1, oo) && "Think_86" \in [1, oo) | [[["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)]]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]] | "Think_194" \in [1, oo) && "Fork_193" \in [1, oo)] | "Fork_65" \in [1, oo) && "Think_66" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)]]] | "Fork_123" \in [1, oo) && "Think_124" \in [1, oo)]]]] | "Fork_118" \in [1, oo) && "Think_119" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)]]] | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)] | "Fork_79" \in [1, oo) && "Think_80" \in [1, oo)]]]]]]]] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)]] | "Think_166" \in [1, oo) && "Fork_165" \in [1, oo)] | "Think_104" \in [1, oo) && "Fork_103" \in [1, oo)]]]]]] | "Fork_124" \in [1, oo) && "Think_125" \in [1, oo)]]]]]]]]] | "Think_186" \in [1, oo) && "Fork_185" \in [1, oo)] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)]]]]] | "Think_146" \in [1, oo) && "Fork_145" \in [1, oo)]] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)]]] | "Think_188" \in [1, oo) && "Fork_187" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)]] | "Think_174" \in [1, oo) && "Fork_173" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]] | "Think_111" \in [1, oo) && "Fork_110" \in [1, oo)]] | "Think_200" \in [1, oo) && "Fork_199" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]]]]] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_114" \in [1, oo) && "Fork_113" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_141" \in [1, oo) && "Fork_140" \in [1, oo)] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_142" \in [1, oo) && "Fork_141" \in [1, oo)] | "Think_184" \in [1, oo) && "Fork_183" \in [1, oo)]]] | "Think_176" \in [1, oo) && "Fork_175" \in [1, oo)]]] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Think_108" \in [1, oo) && "Fork_107" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]]]]]]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_195" \in [1, oo) && "Fork_194" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)] | "Think_167" \in [1, oo) && "Fork_166" \in [1, oo)]] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]]]]]]]]]] | "Think_182" \in [1, oo) && "Fork_181" \in [1, oo)]]]]]]]]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)]]]] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]]]]] | "Think_198" \in [1, oo) && "Fork_197" \in [1, oo)]]]] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]]] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)]]]]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)]]] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)]] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)]]] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)]]]] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)]]]]] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)]] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) & ["Think_139" \in [1, oo) && "Fork_138" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | ["Fork_132" \in [1, oo) && "Think_133" \in [1, oo) | [["Think_173" \in [1, oo) && "Fork_172" \in [1, oo) | [[[[[[[[[["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | [["Fork_155" \in [1, oo) && "Think_156" \in [1, oo) | ["Fork_198" \in [1, oo) && "Think_199" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | [["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_197" \in [1, oo) && "Fork_196" \in [1, oo) | [["Think_171" \in [1, oo) && "Fork_170" \in [1, oo) | [[[["Fork_116" \in [1, oo) && "Think_117" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | [[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | ["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | ["Think_140" \in [1, oo) && "Fork_139" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_93" \in [1, oo) && "Think_94" \in [1, oo) | ["Fork_171" \in [1, oo) && "Think_172" \in [1, oo) | [["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [["Think_106" \in [1, oo) && "Fork_105" \in [1, oo) | ["Think_112" \in [1, oo) && "Fork_111" \in [1, oo) | ["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | [["Fork_55" \in [1, oo) && "Think_56" \in [1, oo) | ["Fork_127" \in [1, oo) && "Think_128" \in [1, oo) | ["Fork_82" \in [1, oo) && "Think_83" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | [["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | ["Think_113" \in [1, oo) && "Fork_112" \in [1, oo) | [["Think_110" \in [1, oo) && "Fork_109" \in [1, oo) | ["Think_101" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_131" \in [1, oo) && "Fork_130" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | [["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_196" \in [1, oo) && "Fork_195" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_52" \in [1, oo) && "Think_53" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [[["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | [[[["Think_162" \in [1, oo) && "Fork_161" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [[[[["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_192" \in [1, oo) && "Fork_191" \in [1, oo) | ["Think_120" \in [1, oo) && "Fork_119" \in [1, oo) | ["Think_190" \in [1, oo) && "Fork_189" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | [[[["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | [["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Think_105" \in [1, oo) && "Fork_104" \in [1, oo) | [[[[[[[["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | [[[["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | ["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | [[[["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | [["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Think_116" \in [1, oo) && "Fork_115" \in [1, oo) | [[["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | [[["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | [[["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | [["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | ["Think_109" \in [1, oo) && "Fork_108" \in [1, oo) | ["Fork_94" \in [1, oo) && "Think_95" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[[["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Think_145" \in [1, oo) && "Fork_144" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | ["Think_143" \in [1, oo) && "Fork_142" \in [1, oo) | ["Fork_120" \in [1, oo) && "Think_121" \in [1, oo) | [["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | ["Think_127" \in [1, oo) && "Fork_126" \in [1, oo) | ["Think_170" \in [1, oo) && "Fork_169" \in [1, oo) | ["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | [[["Think_161" \in [1, oo) && "Fork_160" \in [1, oo) | [["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | ["Think_187" \in [1, oo) && "Fork_186" \in [1, oo) | ["Fork_106" \in [1, oo) && "Think_107" \in [1, oo) | ["Think_136" \in [1, oo) && "Fork_135" \in [1, oo) | ["Fork_147" \in [1, oo) && "Think_148" \in [1, oo) | ["Think_163" \in [1, oo) && "Fork_162" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | [[["Fork_192" \in [1, oo) && "Think_193" \in [1, oo) | [["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_177" \in [1, oo) && "Fork_176" \in [1, oo) | [[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_67" \in [1, oo) && "Think_68" \in [1, oo) | ["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | [["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Think_165" \in [1, oo) && "Fork_164" \in [1, oo) | [[[["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | [["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | ["Fork_85" \in [1, oo) && "Think_86" \in [1, oo) | [[["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)]]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]] | "Think_194" \in [1, oo) && "Fork_193" \in [1, oo)] | "Fork_65" \in [1, oo) && "Think_66" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)]]] | "Fork_123" \in [1, oo) && "Think_124" \in [1, oo)]]]] | "Fork_118" \in [1, oo) && "Think_119" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)]]] | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)] | "Fork_79" \in [1, oo) && "Think_80" \in [1, oo)]]]]]]]] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)]] | "Think_166" \in [1, oo) && "Fork_165" \in [1, oo)] | "Think_104" \in [1, oo) && "Fork_103" \in [1, oo)]]]]]] | "Fork_124" \in [1, oo) && "Think_125" \in [1, oo)]]]]]]]]] | "Think_186" \in [1, oo) && "Fork_185" \in [1, oo)] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)]]]]] | "Think_146" \in [1, oo) && "Fork_145" \in [1, oo)]] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)]]] | "Think_188" \in [1, oo) && "Fork_187" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)]] | "Think_174" \in [1, oo) && "Fork_173" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]] | "Think_111" \in [1, oo) && "Fork_110" \in [1, oo)]] | "Think_200" \in [1, oo) && "Fork_199" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]]]]] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_114" \in [1, oo) && "Fork_113" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_141" \in [1, oo) && "Fork_140" \in [1, oo)] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_142" \in [1, oo) && "Fork_141" \in [1, oo)] | "Think_184" \in [1, oo) && "Fork_183" \in [1, oo)]]] | "Think_176" \in [1, oo) && "Fork_175" \in [1, oo)]]] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Think_108" \in [1, oo) && "Fork_107" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]]]]]]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_195" \in [1, oo) && "Fork_194" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)] | "Think_167" \in [1, oo) && "Fork_166" \in [1, oo)]] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]]]]]]]]]] | "Think_182" \in [1, oo) && "Fork_181" \in [1, oo)]]]]]]]]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)]]]] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]]]]] | "Think_198" \in [1, oo) && "Fork_197" \in [1, oo)]]]] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]]] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)]]]]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)]]] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)]] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)]]] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)]]]] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)]]]]] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)]] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)]]]]]]]]

-> the formula is FALSE

FORMULA p_37_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m5sec

checking: AG [[[["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | [["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_189" \in [1, oo) && "Fork_188" \in [1, oo) | [[[["Think_153" \in [1, oo) && "Fork_152" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | [["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | ["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | [[[["Think_199" \in [1, oo) && "Fork_198" \in [1, oo) | ["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_179" \in [1, oo) && "Fork_178" \in [1, oo) | [[["Think_159" \in [1, oo) && "Fork_158" \in [1, oo) | [[[[["Think_117" \in [1, oo) && "Fork_116" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Think_122" \in [1, oo) && "Fork_121" \in [1, oo) | [[["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | [[[[[["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [[[["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | [[["Think_128" \in [1, oo) && "Fork_127" \in [1, oo) | [["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | [[[[[[["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | [["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | ["Think_182" \in [1, oo) && "Fork_181" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [[["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | [[[["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | ["Fork_166" \in [1, oo) && "Think_167" \in [1, oo) | [["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | [["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Fork_194" \in [1, oo) && "Think_195" \in [1, oo) | [["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | [[[[[[["Think_108" \in [1, oo) && "Fork_107" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | ["Think_176" \in [1, oo) && "Fork_175" \in [1, oo) | ["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Fork_104" \in [1, oo) && "Think_105" \in [1, oo) | ["Think_184" \in [1, oo) && "Fork_183" \in [1, oo) | ["Think_142" \in [1, oo) && "Fork_141" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_141" \in [1, oo) && "Fork_140" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_114" \in [1, oo) && "Fork_113" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | ["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_200" \in [1, oo) && "Fork_199" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_111" \in [1, oo) && "Fork_110" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_174" \in [1, oo) && "Fork_173" \in [1, oo) | ["Fork_115" \in [1, oo) && "Think_116" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_188" \in [1, oo) && "Fork_187" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | ["Think_146" \in [1, oo) && "Fork_145" \in [1, oo) | ["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | ["Fork_108" \in [1, oo) && "Think_109" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | [["Think_186" \in [1, oo) && "Fork_185" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Fork_144" \in [1, oo) && "Think_145" \in [1, oo) | [["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | ["Think_143" \in [1, oo) && "Fork_142" \in [1, oo) | ["Think_121" \in [1, oo) && "Fork_120" \in [1, oo) | [[["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | [[["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | ["Fork_103" \in [1, oo) && "Think_104" \in [1, oo) | ["Think_166" \in [1, oo) && "Fork_165" \in [1, oo) | [[["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | [[[[[[["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | [[[[["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_119" \in [1, oo) && "Fork_118" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | ["Think_124" \in [1, oo) && "Fork_123" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | [[["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | ["Fork_193" \in [1, oo) && "Think_194" \in [1, oo) | ["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | [["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | [["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)]] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)]]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]]]] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_165" \in [1, oo) && "Fork_164" \in [1, oo)]]]]]]]] | "Think_177" \in [1, oo) && "Fork_176" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_193" \in [1, oo) && "Fork_192" \in [1, oo)]]] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_163" \in [1, oo) && "Fork_162" \in [1, oo)] | "Think_148" \in [1, oo) && "Fork_147" \in [1, oo)] | "Think_136" \in [1, oo) && "Fork_135" \in [1, oo)] | "Think_107" \in [1, oo) && "Fork_106" \in [1, oo)] | "Think_187" \in [1, oo) && "Fork_186" \in [1, oo)]] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)] | "Think_161" \in [1, oo) && "Fork_160" \in [1, oo)]]]] | "Think_170" \in [1, oo) && "Fork_169" \in [1, oo)] | "Think_127" \in [1, oo) && "Fork_126" \in [1, oo)]] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_125" \in [1, oo) && "Fork_124" \in [1, oo)]]]]] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)]]]]] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Think_190" \in [1, oo) && "Fork_189" \in [1, oo)] | "Think_120" \in [1, oo) && "Fork_119" \in [1, oo)] | "Think_192" \in [1, oo) && "Fork_191" \in [1, oo)]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)]]] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]] | "Think_162" \in [1, oo) && "Fork_161" \in [1, oo)]] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)]]]]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]]]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Fork_195" \in [1, oo) && "Think_196" \in [1, oo)]]]] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)]]] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_131" \in [1, oo) && "Fork_130" \in [1, oo)] | "Think_101" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_110" \in [1, oo) && "Fork_109" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_113" \in [1, oo) && "Fork_112" \in [1, oo)]]] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)]] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Fork_197" \in [1, oo) && "Think_198" \in [1, oo)]] | "Think_112" \in [1, oo) && "Fork_111" \in [1, oo)] | "Think_106" \in [1, oo) && "Fork_105" \in [1, oo)] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]]]]] | "Think_172" \in [1, oo) && "Fork_171" \in [1, oo)] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)] | "Think_140" \in [1, oo) && "Fork_139" \in [1, oo)]]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)]]]] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_171" \in [1, oo) && "Fork_170" \in [1, oo)]] | "Think_197" \in [1, oo) && "Fork_196" \in [1, oo)] | "Fork_95" \in [1, oo) && "Think_96" \in [1, oo)]]]] | "Think_156" \in [1, oo) && "Fork_155" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)]]]] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)]]] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)]]]] | "Fork_172" \in [1, oo) && "Think_173" \in [1, oo)]] | "Think_133" \in [1, oo) && "Fork_132" \in [1, oo)]] | "Think_139" \in [1, oo) && "Fork_138" \in [1, oo)] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | [[[[[[[["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | [["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | ["Think_182" \in [1, oo) && "Fork_181" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [[["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | ["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | [[[["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | ["Fork_166" \in [1, oo) && "Think_167" \in [1, oo) | [["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | [["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Fork_194" \in [1, oo) && "Think_195" \in [1, oo) | [["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | [[[[[[["Think_108" \in [1, oo) && "Fork_107" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | ["Think_176" \in [1, oo) && "Fork_175" \in [1, oo) | ["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Fork_104" \in [1, oo) && "Think_105" \in [1, oo) | ["Think_184" \in [1, oo) && "Fork_183" \in [1, oo) | ["Think_142" \in [1, oo) && "Fork_141" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | [["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_141" \in [1, oo) && "Fork_140" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_114" \in [1, oo) && "Fork_113" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | ["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_200" \in [1, oo) && "Fork_199" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_111" \in [1, oo) && "Fork_110" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_174" \in [1, oo) && "Fork_173" \in [1, oo) | ["Fork_115" \in [1, oo) && "Think_116" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_188" \in [1, oo) && "Fork_187" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | ["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | ["Think_146" \in [1, oo) && "Fork_145" \in [1, oo) | ["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | ["Fork_108" \in [1, oo) && "Think_109" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | [["Think_186" \in [1, oo) && "Fork_185" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Fork_144" \in [1, oo) && "Think_145" \in [1, oo) | [["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | ["Think_143" \in [1, oo) && "Fork_142" \in [1, oo) | ["Think_121" \in [1, oo) && "Fork_120" \in [1, oo) | [[["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | [[["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | ["Fork_103" \in [1, oo) && "Think_104" \in [1, oo) | ["Think_166" \in [1, oo) && "Fork_165" \in [1, oo) | [[["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | [[[[[[["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | [[[[["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_119" \in [1, oo) && "Fork_118" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Fork_68" \in [1, oo) && "Think_69" \in [1, oo) | ["Think_124" \in [1, oo) && "Fork_123" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | [[["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | ["Fork_193" \in [1, oo) && "Think_194" \in [1, oo) | ["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | [["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | [["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)]] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)]]] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)]]]]] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_165" \in [1, oo) && "Fork_164" \in [1, oo)]]]]]]]] | "Think_177" \in [1, oo) && "Fork_176" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_193" \in [1, oo) && "Fork_192" \in [1, oo)]]] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_163" \in [1, oo) && "Fork_162" \in [1, oo)] | "Think_148" \in [1, oo) && "Fork_147" \in [1, oo)] | "Think_136" \in [1, oo) && "Fork_135" \in [1, oo)] | "Think_107" \in [1, oo) && "Fork_106" \in [1, oo)] | "Think_187" \in [1, oo) && "Fork_186" \in [1, oo)]] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)] | "Think_161" \in [1, oo) && "Fork_160" \in [1, oo)]]]] | "Think_170" \in [1, oo) && "Fork_169" \in [1, oo)] | "Think_127" \in [1, oo) && "Fork_126" \in [1, oo)]] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_125" \in [1, oo) && "Fork_124" \in [1, oo)]]]]] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)]]]]] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)]]]]]]]]]]] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Think_190" \in [1, oo) && "Fork_189" \in [1, oo)] | "Think_120" \in [1, oo) && "Fork_119" \in [1, oo)] | "Think_192" \in [1, oo) && "Fork_191" \in [1, oo)]]] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)]]] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]] | "Think_162" \in [1, oo) && "Fork_161" \in [1, oo)]] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)]]]]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]]]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Fork_195" \in [1, oo) && "Think_196" \in [1, oo)]]]] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)]] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_131" \in [1, oo) && "Fork_130" \in [1, oo)] | "Think_101" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_110" \in [1, oo) && "Fork_109" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_113" \in [1, oo) && "Fork_112" \in [1, oo)]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)] | "Think_128" \in [1, oo) && "Fork_127" \in [1, oo)] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Fork_197" \in [1, oo) && "Think_198" \in [1, oo)] | "Think_180" \in [1, oo) && "Fork_179" \in [1, oo)] | "Think_112" \in [1, oo) && "Fork_111" \in [1, oo)] | "Think_106" \in [1, oo) && "Fork_105" \in [1, oo)] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_134" \in [1, oo) && "Fork_133" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)] | "Think_172" \in [1, oo) && "Fork_171" \in [1, oo)] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)] | "Think_140" \in [1, oo) && "Fork_139" \in [1, oo)] | "Think_135" \in [1, oo) && "Fork_134" \in [1, oo)] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Think_117" \in [1, oo) && "Fork_116" \in [1, oo)] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_171" \in [1, oo) && "Fork_170" \in [1, oo)] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)] | "Think_197" \in [1, oo) && "Fork_196" \in [1, oo)] | "Fork_95" \in [1, oo) && "Think_96" \in [1, oo)] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)] | "Think_199" \in [1, oo) && "Fork_198" \in [1, oo)] | "Think_156" \in [1, oo) && "Fork_155" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Fork_172" \in [1, oo) && "Think_173" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_133" \in [1, oo) && "Fork_132" \in [1, oo)] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_139" \in [1, oo) && "Fork_138" \in [1, oo)]]]]]


before gc: list nodes free: 1942985

after gc: idd nodes used:20380, unused:15979620; list nodes free:71203879

before gc: list nodes free: 2157193

after gc: idd nodes used:19606, unused:15980394; list nodes free:71206982

before gc: list nodes free: 2129769

after gc: idd nodes used:19644, unused:15980356; list nodes free:71206614

before gc: list nodes free: 2094735

after gc: idd nodes used:18788, unused:15981212; list nodes free:71210269

before gc: list nodes free: 2042034

after gc: idd nodes used:17654, unused:15982346; list nodes free:71215143

before gc: list nodes free: 1931402

after gc: idd nodes used:15831, unused:15984169; list nodes free:71223518
-> the formula is FALSE

FORMULA p_38_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 13m29sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) & [[["Think_133" \in [1, oo) && "Fork_132" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Think_173" \in [1, oo) && "Fork_172" \in [1, oo) | [["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_189" \in [1, oo) && "Fork_188" \in [1, oo) | [["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | [[[[[["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | [[[["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_179" \in [1, oo) && "Fork_178" \in [1, oo) | ["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_197" \in [1, oo) && "Fork_196" \in [1, oo) | ["Think_159" \in [1, oo) && "Fork_158" \in [1, oo) | [[[[[["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | [[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | ["Fork_70" \in [1, oo) && "Think_71" \in [1, oo) | ["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | ["Think_140" \in [1, oo) && "Fork_139" \in [1, oo) | [[["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | ["Think_172" \in [1, oo) && "Fork_171" \in [1, oo) | ["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | [[["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [[["Think_112" \in [1, oo) && "Fork_111" \in [1, oo) | [["Think_198" \in [1, oo) && "Fork_197" \in [1, oo) | [[[["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | ["Fork_112" \in [1, oo) && "Think_113" \in [1, oo) | [[[["Think_131" \in [1, oo) && "Fork_130" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | ["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | [[["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_196" \in [1, oo) && "Fork_195" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | ["Fork_56" \in [1, oo) && "Think_57" \in [1, oo) | [["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | [["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | [["Think_167" \in [1, oo) && "Fork_166" \in [1, oo) | ["Think_169" \in [1, oo) && "Fork_168" \in [1, oo) | [[[["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [[["Think_195" \in [1, oo) && "Fork_194" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Fork_191" \in [1, oo) && "Think_192" \in [1, oo) | ["Think_120" \in [1, oo) && "Fork_119" \in [1, oo) | ["Think_190" \in [1, oo) && "Fork_189" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | [[["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | ["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | [["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | [[[[["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | [["Think_141" \in [1, oo) && "Fork_140" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | ["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_114" \in [1, oo) && "Fork_113" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | ["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | ["Fork_16" \in [1, oo) && "Think_17" \in [1, oo) | ["Fork_78" \in [1, oo) && "Think_79" \in [1, oo) | ["Think_200" \in [1, oo) && "Fork_199" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_111" \in [1, oo) && "Fork_110" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_174" \in [1, oo) && "Fork_173" \in [1, oo) | ["Think_116" \in [1, oo) && "Fork_115" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_188" \in [1, oo) && "Fork_187" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | ["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_80" \in [1, oo) && "Think_81" \in [1, oo) | ["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | ["Think_146" \in [1, oo) && "Fork_145" \in [1, oo) | ["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | ["Think_109" \in [1, oo) && "Fork_108" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_102" \in [1, oo) && "Fork_101" \in [1, oo) | ["Think_186" \in [1, oo) && "Fork_185" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Think_145" \in [1, oo) && "Fork_144" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Fork_190" \in [1, oo) && "Think_191" \in [1, oo) | ["Fork_142" \in [1, oo) && "Think_143" \in [1, oo) | ["Think_121" \in [1, oo) && "Fork_120" \in [1, oo) | ["Think_125" \in [1, oo) && "Fork_124" \in [1, oo) | ["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | ["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | ["Think_127" \in [1, oo) && "Fork_126" \in [1, oo) | ["Think_170" \in [1, oo) && "Fork_169" \in [1, oo) | ["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | ["Think_104" \in [1, oo) && "Fork_103" \in [1, oo) | ["Think_166" \in [1, oo) && "Fork_165" \in [1, oo) | ["Think_161" \in [1, oo) && "Fork_160" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | ["Think_187" \in [1, oo) && "Fork_186" \in [1, oo) | ["Think_107" \in [1, oo) && "Fork_106" \in [1, oo) | ["Fork_135" \in [1, oo) && "Think_136" \in [1, oo) | ["Fork_147" \in [1, oo) && "Think_148" \in [1, oo) | ["Think_163" \in [1, oo) && "Fork_162" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_193" \in [1, oo) && "Fork_192" \in [1, oo) | ["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_177" \in [1, oo) && "Fork_176" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_119" \in [1, oo) && "Fork_118" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_124" \in [1, oo) && "Fork_123" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Think_165" \in [1, oo) && "Fork_164" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | ["Think_194" \in [1, oo) && "Fork_193" \in [1, oo) | ["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | ["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | [[["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Think_185" \in [1, oo) && "Fork_184" \in [1, oo) | "Think_151" \in [1, oo) && "Fork_150" \in [1, oo)]] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)]] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_142" \in [1, oo) && "Fork_141" \in [1, oo)] | "Think_184" \in [1, oo) && "Fork_183" \in [1, oo)] | "Think_105" \in [1, oo) && "Fork_104" \in [1, oo)]] | "Think_176" \in [1, oo) && "Fork_175" \in [1, oo)]]]] | "Think_108" \in [1, oo) && "Fork_107" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]]]]]]]]]] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_162" \in [1, oo) && "Fork_161" \in [1, oo)] | "Fork_59" \in [1, oo) && "Think_60" \in [1, oo)]]] | "Think_181" \in [1, oo) && "Fork_180" \in [1, oo)]] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)]] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)]] | "Think_168" \in [1, oo) && "Fork_167" \in [1, oo)]]]]]] | "Think_182" \in [1, oo) && "Fork_181" \in [1, oo)] | "Think_183" \in [1, oo) && "Fork_182" \in [1, oo)]]]]]] | "Think_101" \in [1, oo) && "Fork_100" \in [1, oo)] | "Think_110" \in [1, oo) && "Fork_109" \in [1, oo)] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)]]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)] | "Think_128" \in [1, oo) && "Fork_127" \in [1, oo)] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)]] | "Think_180" \in [1, oo) && "Fork_179" \in [1, oo)]] | "Think_106" \in [1, oo) && "Fork_105" \in [1, oo)] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]] | "Think_134" \in [1, oo) && "Fork_133" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)]]]] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)]]]]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)]] | "Think_117" \in [1, oo) && "Fork_116" \in [1, oo)] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_171" \in [1, oo) && "Fork_170" \in [1, oo)]]]]]] | "Think_199" \in [1, oo) && "Fork_198" \in [1, oo)] | "Think_156" \in [1, oo) && "Fork_155" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)]]]] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)]] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)]]] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)]]]] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_139" \in [1, oo) && "Fork_138" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) & ["Think_139" \in [1, oo) && "Fork_138" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[[["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | [[["Think_150" \in [1, oo) && "Fork_149" \in [1, oo) | [["Think_118" \in [1, oo) && "Fork_117" \in [1, oo) | ["Think_153" \in [1, oo) && "Fork_152" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | ["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | [[[["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_156" \in [1, oo) && "Fork_155" \in [1, oo) | ["Think_199" \in [1, oo) && "Fork_198" \in [1, oo) | [[[[[["Think_171" \in [1, oo) && "Fork_170" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_126" \in [1, oo) && "Fork_125" \in [1, oo) | ["Think_130" \in [1, oo) && "Fork_129" \in [1, oo) | ["Think_117" \in [1, oo) && "Fork_116" \in [1, oo) | [["Think_122" \in [1, oo) && "Fork_121" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | [[[[["Think_152" \in [1, oo) && "Fork_151" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [[[["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | [[["Think_175" \in [1, oo) && "Fork_174" \in [1, oo) | ["Think_106" \in [1, oo) && "Fork_105" \in [1, oo) | [["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | [["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Think_128" \in [1, oo) && "Fork_127" \in [1, oo) | ["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | [[["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | ["Think_110" \in [1, oo) && "Fork_109" \in [1, oo) | ["Think_101" \in [1, oo) && "Fork_100" \in [1, oo) | [[[[[["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | ["Think_182" \in [1, oo) && "Fork_181" \in [1, oo) | [[[[[["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | [["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | [["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | [["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | [[["Fork_59" \in [1, oo) && "Think_60" \in [1, oo) | ["Think_162" \in [1, oo) && "Fork_161" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | [["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | [[[[[[[[[["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | ["Think_108" \in [1, oo) && "Fork_107" \in [1, oo) | [[[["Think_176" \in [1, oo) && "Fork_175" \in [1, oo) | [["Think_105" \in [1, oo) && "Fork_104" \in [1, oo) | ["Think_184" \in [1, oo) && "Fork_183" \in [1, oo) | ["Think_142" \in [1, oo) && "Fork_141" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | [["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Think_155" \in [1, oo) && "Fork_154" \in [1, oo) | [["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)]]] | "Think_115" \in [1, oo) && "Fork_114" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_103" \in [1, oo) && "Fork_102" \in [1, oo)] | "Think_123" \in [1, oo) && "Fork_122" \in [1, oo)] | "Think_194" \in [1, oo) && "Fork_193" \in [1, oo)] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_165" \in [1, oo) && "Fork_164" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)] | "Think_124" \in [1, oo) && "Fork_123" \in [1, oo)] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)] | "Think_119" \in [1, oo) && "Fork_118" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_177" \in [1, oo) && "Fork_176" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_193" \in [1, oo) && "Fork_192" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_163" \in [1, oo) && "Fork_162" \in [1, oo)] | "Fork_147" \in [1, oo) && "Think_148" \in [1, oo)] | "Fork_135" \in [1, oo) && "Think_136" \in [1, oo)] | "Think_107" \in [1, oo) && "Fork_106" \in [1, oo)] | "Think_187" \in [1, oo) && "Fork_186" \in [1, oo)] | "Think_132" \in [1, oo) && "Fork_131" \in [1, oo)] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)] | "Think_161" \in [1, oo) && "Fork_160" \in [1, oo)] | "Think_166" \in [1, oo) && "Fork_165" \in [1, oo)] | "Think_104" \in [1, oo) && "Fork_103" \in [1, oo)] | "Think_157" \in [1, oo) && "Fork_156" \in [1, oo)] | "Think_170" \in [1, oo) && "Fork_169" \in [1, oo)] | "Think_127" \in [1, oo) && "Fork_126" \in [1, oo)] | "Think_149" \in [1, oo) && "Fork_148" \in [1, oo)] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_125" \in [1, oo) && "Fork_124" \in [1, oo)] | "Think_121" \in [1, oo) && "Fork_120" \in [1, oo)] | "Fork_142" \in [1, oo) && "Think_143" \in [1, oo)] | "Fork_190" \in [1, oo) && "Think_191" \in [1, oo)] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)] | "Think_145" \in [1, oo) && "Fork_144" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_200" \in [1, oo)] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_186" \in [1, oo) && "Fork_185" \in [1, oo)] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)] | "Think_109" \in [1, oo) && "Fork_108" \in [1, oo)] | "Think_137" \in [1, oo) && "Fork_136" \in [1, oo)] | "Think_146" \in [1, oo) && "Fork_145" \in [1, oo)] | "Think_160" \in [1, oo) && "Fork_159" \in [1, oo)] | "Fork_80" \in [1, oo) && "Think_81" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Think_129" \in [1, oo) && "Fork_128" \in [1, oo)] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Think_188" \in [1, oo) && "Fork_187" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)] | "Think_116" \in [1, oo) && "Fork_115" \in [1, oo)] | "Think_174" \in [1, oo) && "Fork_173" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_111" \in [1, oo) && "Fork_110" \in [1, oo)] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)] | "Think_200" \in [1, oo) && "Fork_199" \in [1, oo)] | "Fork_78" \in [1, oo) && "Think_79" \in [1, oo)] | "Fork_16" \in [1, oo) && "Think_17" \in [1, oo)] | "Think_147" \in [1, oo) && "Fork_146" \in [1, oo)] | "Think_164" \in [1, oo) && "Fork_163" \in [1, oo)] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_114" \in [1, oo) && "Fork_113" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_141" \in [1, oo) && "Fork_140" \in [1, oo)]] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)]]]]] | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]] | "Think_154" \in [1, oo) && "Fork_153" \in [1, oo)] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)]]] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Think_190" \in [1, oo) && "Fork_189" \in [1, oo)] | "Think_120" \in [1, oo) && "Fork_119" \in [1, oo)] | "Fork_191" \in [1, oo) && "Think_192" \in [1, oo)] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)] | "Think_178" \in [1, oo) && "Fork_177" \in [1, oo)] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_195" \in [1, oo) && "Fork_194" \in [1, oo)]]] | "Think_158" \in [1, oo) && "Fork_157" \in [1, oo)]]]] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)] | "Think_167" \in [1, oo) && "Fork_166" \in [1, oo)]] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)]] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)]] | "Fork_56" \in [1, oo) && "Think_57" \in [1, oo)] | "Think_138" \in [1, oo) && "Fork_137" \in [1, oo)] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Think_196" \in [1, oo) && "Fork_195" \in [1, oo)] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)]]] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_131" \in [1, oo) && "Fork_130" \in [1, oo)]]]] | "Fork_112" \in [1, oo) && "Think_113" \in [1, oo)] | "Think_144" \in [1, oo) && "Fork_143" \in [1, oo)]]] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)]]]] | "Think_198" \in [1, oo) && "Fork_197" \in [1, oo)]] | "Think_112" \in [1, oo) && "Fork_111" \in [1, oo)]]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)]]] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)] | "Think_172" \in [1, oo) && "Fork_171" \in [1, oo)] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]]] | "Think_140" \in [1, oo) && "Fork_139" \in [1, oo)] | "Think_135" \in [1, oo) && "Fork_134" \in [1, oo)] | "Fork_70" \in [1, oo) && "Think_71" \in [1, oo)] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)]]] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)]]]]]] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)] | "Think_197" \in [1, oo) && "Fork_196" \in [1, oo)] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)]]]] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]]]]]] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)]] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)]] | "Think_173" \in [1, oo) && "Fork_172" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_133" \in [1, oo) && "Fork_132" \in [1, oo)]]]]]]]

-> the formula is FALSE

FORMULA p_39_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m4sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) | [["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Think_133" \in [1, oo) && "Fork_132" \in [1, oo) | [[[["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_189" \in [1, oo) && "Fork_188" \in [1, oo) | [[[[[[["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | [[["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_156" \in [1, oo) && "Fork_155" \in [1, oo) | [["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_179" \in [1, oo) && "Fork_178" \in [1, oo) | ["Fork_95" \in [1, oo) && "Think_96" \in [1, oo) | [["Think_159" \in [1, oo) && "Fork_158" \in [1, oo) | [[[[["Think_117" \in [1, oo) && "Fork_116" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | [[[["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | [[[[["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | [[[[[[["Think_175" \in [1, oo) && "Fork_174" \in [1, oo) | [[[[[[["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [[["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | [[[["Think_110" \in [1, oo) && "Fork_109" \in [1, oo) | [[[["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | [[[[[[[["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | [[[[[["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | [[[[["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | [[[["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | [[[[[[[[["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | [[[["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | [[[[["Think_184" \in [1, oo) && "Fork_183" \in [1, oo) | [[[[[[["Think_28" \in [1, oo) && "Fork_27" \in [1, oo) | [[[[[["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | [[[[[["Think_111" \in [1, oo) && "Fork_110" \in [1, oo) | [[[[[[["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | ["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | [[["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | ["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | [["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | [[["Think_109" \in [1, oo) && "Fork_108" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | [["Think_186" \in [1, oo) && "Fork_185" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | [[["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | [["Think_143" \in [1, oo) && "Fork_142" \in [1, oo) | ["Think_121" \in [1, oo) && "Fork_120" \in [1, oo) | [[["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | ["Think_127" \in [1, oo) && "Fork_126" \in [1, oo) | ["Think_170" \in [1, oo) && "Fork_169" \in [1, oo) | ["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | ["Think_104" \in [1, oo) && "Fork_103" \in [1, oo) | [[["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | ["Think_187" \in [1, oo) && "Fork_186" \in [1, oo) | ["Fork_106" \in [1, oo) && "Think_107" \in [1, oo) | [["Think_148" \in [1, oo) && "Fork_147" \in [1, oo) | ["Think_163" \in [1, oo) && "Fork_162" \in [1, oo) | ["Fork_66" \in [1, oo) && "Think_67" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | [[["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | [[[[[[["Think_124" \in [1, oo) && "Fork_123" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_165" \in [1, oo) && "Fork_164" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | ["Think_194" \in [1, oo) && "Fork_193" \in [1, oo) | ["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Fork_102" \in [1, oo) && "Think_103" \in [1, oo) | ["Fork_91" \in [1, oo) && "Think_92" \in [1, oo) | ["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | [[["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_150" \in [1, oo) && "Think_151" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)]] | "Fork_154" \in [1, oo) && "Think_155" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)]]]]]]]]]]] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)] | "Think_119" \in [1, oo) && "Fork_118" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_177" \in [1, oo) && "Fork_176" \in [1, oo)]]] | "Think_193" \in [1, oo) && "Fork_192" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)]]]]] | "Think_136" \in [1, oo) && "Fork_135" \in [1, oo)]]]]] | "Think_161" \in [1, oo) && "Fork_160" \in [1, oo)] | "Think_166" \in [1, oo) && "Fork_165" \in [1, oo)]]]]]] | "Think_44" \in [1, oo) && "Fork_43" \in [1, oo)] | "Think_125" \in [1, oo) && "Fork_124" \in [1, oo)]]] | "Think_191" \in [1, oo) && "Fork_190" \in [1, oo)]]] | "Think_145" \in [1, oo) && "Fork_144" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_200" \in [1, oo)]]] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)]]]]] | "Think_137" \in [1, oo) && "Fork_136" \in [1, oo)] | "Think_146" \in [1, oo) && "Fork_145" \in [1, oo)]] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)]]] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)] | "Think_188" \in [1, oo) && "Fork_187" \in [1, oo)]]] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)] | "Think_116" \in [1, oo) && "Fork_115" \in [1, oo)] | "Think_174" \in [1, oo) && "Fork_173" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)]] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)] | "Think_200" \in [1, oo) && "Fork_199" \in [1, oo)] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_147" \in [1, oo) && "Fork_146" \in [1, oo)]] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_114" \in [1, oo) && "Fork_113" \in [1, oo)] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_141" \in [1, oo) && "Fork_140" \in [1, oo)] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_142" \in [1, oo) && "Fork_141" \in [1, oo)]] | "Think_105" \in [1, oo) && "Fork_104" \in [1, oo)] | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)] | "Think_176" \in [1, oo) && "Fork_175" \in [1, oo)] | "Think_154" \in [1, oo) && "Fork_153" \in [1, oo)]] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Think_108" \in [1, oo) && "Fork_107" \in [1, oo)] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)]] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)] | "Think_190" \in [1, oo) && "Fork_189" \in [1, oo)] | "Think_120" \in [1, oo) && "Fork_119" \in [1, oo)] | "Think_192" \in [1, oo) && "Fork_191" \in [1, oo)] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)] | "Think_178" \in [1, oo) && "Fork_177" \in [1, oo)] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)] | "Think_195" \in [1, oo) && "Fork_194" \in [1, oo)]]] | "Think_158" \in [1, oo) && "Fork_157" \in [1, oo)] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_162" \in [1, oo) && "Fork_161" \in [1, oo)]] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)] | "Think_167" \in [1, oo) && "Fork_166" \in [1, oo)] | "Think_181" \in [1, oo) && "Fork_180" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)]] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)] | "Think_168" \in [1, oo) && "Fork_167" \in [1, oo)] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)]] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Think_196" \in [1, oo) && "Fork_195" \in [1, oo)] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)] | "Think_182" \in [1, oo) && "Fork_181" \in [1, oo)] | "Think_183" \in [1, oo) && "Fork_182" \in [1, oo)] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)]] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_131" \in [1, oo) && "Fork_130" \in [1, oo)] | "Think_101" \in [1, oo) && "Fork_100" \in [1, oo)]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_113" \in [1, oo) && "Fork_112" \in [1, oo)] | "Think_144" \in [1, oo) && "Fork_143" \in [1, oo)]] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)]] | "Think_128" \in [1, oo) && "Fork_127" \in [1, oo)] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Think_198" \in [1, oo) && "Fork_197" \in [1, oo)] | "Think_180" \in [1, oo) && "Fork_179" \in [1, oo)] | "Think_112" \in [1, oo) && "Fork_111" \in [1, oo)] | "Think_106" \in [1, oo) && "Fork_105" \in [1, oo)]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_134" \in [1, oo) && "Fork_133" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)] | "Think_172" \in [1, oo) && "Fork_171" \in [1, oo)]] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)] | "Think_140" \in [1, oo) && "Fork_139" \in [1, oo)] | "Think_135" \in [1, oo) && "Fork_134" \in [1, oo)]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)]]] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)] | "Think_171" \in [1, oo) && "Fork_170" \in [1, oo)]] | "Think_197" \in [1, oo) && "Fork_196" \in [1, oo)]]]] | "Think_199" \in [1, oo) && "Fork_198" \in [1, oo)]]]] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)]]] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)] | "Think_173" \in [1, oo) && "Fork_172" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)]]] | "Think_139" \in [1, oo) && "Fork_138" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) | ["Think_139" \in [1, oo) && "Fork_138" \in [1, oo) | [[["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Think_173" \in [1, oo) && "Fork_172" \in [1, oo) | ["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | [[["Think_150" \in [1, oo) && "Fork_149" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_118" \in [1, oo) && "Fork_117" \in [1, oo) | ["Think_153" \in [1, oo) && "Fork_152" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | [["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | ["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | [[[["Think_199" \in [1, oo) && "Fork_198" \in [1, oo) | [[[["Think_197" \in [1, oo) && "Fork_196" \in [1, oo) | [["Think_171" \in [1, oo) && "Fork_170" \in [1, oo) | ["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | ["Think_126" \in [1, oo) && "Fork_125" \in [1, oo) | ["Think_130" \in [1, oo) && "Fork_129" \in [1, oo) | [[["Think_122" \in [1, oo) && "Fork_121" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | ["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | ["Think_140" \in [1, oo) && "Fork_139" \in [1, oo) | ["Think_152" \in [1, oo) && "Fork_151" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [["Think_172" \in [1, oo) && "Fork_171" \in [1, oo) | ["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [["Think_106" \in [1, oo) && "Fork_105" \in [1, oo) | ["Think_112" \in [1, oo) && "Fork_111" \in [1, oo) | ["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | ["Think_198" \in [1, oo) && "Fork_197" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | ["Think_128" \in [1, oo) && "Fork_127" \in [1, oo) | [["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | [["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | ["Think_113" \in [1, oo) && "Fork_112" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | [["Think_101" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_131" \in [1, oo) && "Fork_130" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | [["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | ["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | ["Think_182" \in [1, oo) && "Fork_181" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | ["Think_196" \in [1, oo) && "Fork_195" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | [["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | ["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | ["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | ["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | [["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | ["Think_167" \in [1, oo) && "Fork_166" \in [1, oo) | ["Think_169" \in [1, oo) && "Fork_168" \in [1, oo) | [["Think_162" \in [1, oo) && "Fork_161" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | ["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [[["Think_195" \in [1, oo) && "Fork_194" \in [1, oo) | ["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Think_178" \in [1, oo) && "Fork_177" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_192" \in [1, oo) && "Fork_191" \in [1, oo) | ["Think_120" \in [1, oo) && "Fork_119" \in [1, oo) | ["Think_190" \in [1, oo) && "Fork_189" \in [1, oo) | ["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | [["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | ["Think_108" \in [1, oo) && "Fork_107" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | [["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | ["Think_176" \in [1, oo) && "Fork_175" \in [1, oo) | ["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Think_105" \in [1, oo) && "Fork_104" \in [1, oo) | [["Think_142" \in [1, oo) && "Fork_141" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | ["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | ["Think_141" \in [1, oo) && "Fork_140" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | [["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | ["Think_114" \in [1, oo) && "Fork_113" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | [["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | ["Think_200" \in [1, oo) && "Fork_199" \in [1, oo) | ["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | [["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_174" \in [1, oo) && "Fork_173" \in [1, oo) | ["Think_116" \in [1, oo) && "Fork_115" \in [1, oo) | ["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | ["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | [[["Think_188" \in [1, oo) && "Fork_187" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | [[["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | [["Think_146" \in [1, oo) && "Fork_145" \in [1, oo) | ["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | [[[[["Think_102" \in [1, oo) && "Fork_101" \in [1, oo) | [[["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Think_145" \in [1, oo) && "Fork_144" \in [1, oo) | [[["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | [[["Think_125" \in [1, oo) && "Fork_124" \in [1, oo) | ["Think_44" \in [1, oo) && "Fork_43" \in [1, oo) | [[[[[["Think_166" \in [1, oo) && "Fork_165" \in [1, oo) | ["Think_161" \in [1, oo) && "Fork_160" \in [1, oo) | [[[[["Think_136" \in [1, oo) && "Fork_135" \in [1, oo) | [[[[["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_193" \in [1, oo) && "Fork_192" \in [1, oo) | [[["Think_177" \in [1, oo) && "Fork_176" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_119" \in [1, oo) && "Fork_118" \in [1, oo) | ["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | ["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | [[[[[[[[[[["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Fork_154" \in [1, oo) && "Think_155" \in [1, oo) | [["Think_185" \in [1, oo) && "Fork_184" \in [1, oo) | "Fork_150" \in [1, oo) && "Think_151" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)]]] | "Think_115" \in [1, oo) && "Fork_114" \in [1, oo)] | "Fork_91" \in [1, oo) && "Think_92" \in [1, oo)] | "Fork_102" \in [1, oo) && "Think_103" \in [1, oo)] | "Think_123" \in [1, oo) && "Fork_122" \in [1, oo)] | "Think_194" \in [1, oo) && "Fork_193" \in [1, oo)] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_165" \in [1, oo) && "Fork_164" \in [1, oo)] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_124" \in [1, oo) && "Fork_123" \in [1, oo)]]]]]]] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)]]] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Fork_66" \in [1, oo) && "Think_67" \in [1, oo)] | "Think_163" \in [1, oo) && "Fork_162" \in [1, oo)] | "Think_148" \in [1, oo) && "Fork_147" \in [1, oo)]] | "Fork_106" \in [1, oo) && "Think_107" \in [1, oo)] | "Think_187" \in [1, oo) && "Fork_186" \in [1, oo)] | "Think_132" \in [1, oo) && "Fork_131" \in [1, oo)] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)]]] | "Think_104" \in [1, oo) && "Fork_103" \in [1, oo)] | "Think_157" \in [1, oo) && "Fork_156" \in [1, oo)] | "Think_170" \in [1, oo) && "Fork_169" \in [1, oo)] | "Think_127" \in [1, oo) && "Fork_126" \in [1, oo)] | "Think_149" \in [1, oo) && "Fork_148" \in [1, oo)]]] | "Think_121" \in [1, oo) && "Fork_120" \in [1, oo)] | "Think_143" \in [1, oo) && "Fork_142" \in [1, oo)]] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)]]] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_186" \in [1, oo) && "Fork_185" \in [1, oo)]] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)] | "Think_109" \in [1, oo) && "Fork_108" \in [1, oo)]]] | "Think_160" \in [1, oo) && "Fork_159" \in [1, oo)]] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)] | "Think_129" \in [1, oo) && "Fork_128" \in [1, oo)]]] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)]]]]]]] | "Think_111" \in [1, oo) && "Fork_110" \in [1, oo)]]]]]] | "Think_164" \in [1, oo) && "Fork_163" \in [1, oo)]]]]]] | "Think_28" \in [1, oo) && "Fork_27" \in [1, oo)]]]]]]] | "Think_184" \in [1, oo) && "Fork_183" \in [1, oo)]]]]] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)]]]] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)]]]]]]]]] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)]]]]] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)]]]]]] | "Think_138" \in [1, oo) && "Fork_137" \in [1, oo)]]]]]]]] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)]]]] | "Think_110" \in [1, oo) && "Fork_109" \in [1, oo)]]]] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)]]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)]]]]]]] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]]]]]] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]]]]] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)]]]] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)] | "Think_117" \in [1, oo) && "Fork_116" \in [1, oo)]]]]] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)]] | "Fork_95" \in [1, oo) && "Think_96" \in [1, oo)] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)]] | "Think_156" \in [1, oo) && "Fork_155" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)]]] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)]]]]]]] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)]]]] | "Think_133" \in [1, oo) && "Fork_132" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)]]]]]]


before gc: list nodes free: 1970087

after gc: idd nodes used:20894, unused:15979106; list nodes free:71202719

before gc: list nodes free: 2162496

after gc: idd nodes used:19866, unused:15980134; list nodes free:71207161

before gc: list nodes free: 2136004

after gc: idd nodes used:19320, unused:15980680; list nodes free:71209499

before gc: list nodes free: 2102535

after gc: idd nodes used:18414, unused:15981586; list nodes free:71213423

before gc: list nodes free: 2053780

after gc: idd nodes used:18212, unused:15981788; list nodes free:71214251

before gc: list nodes free: 1949939

after gc: idd nodes used:17953, unused:15982047; list nodes free:71215306
-> the formula is FALSE

FORMULA p_40_mix_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 16m15sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) | [[["Think_133" \in [1, oo) && "Fork_132" \in [1, oo) | ["Think_72" \in [1, oo) && "Fork_71" \in [1, oo) | ["Fork_172" \in [1, oo) && "Think_173" \in [1, oo) | [["Think_49" \in [1, oo) && "Fork_48" \in [1, oo) | ["Think_189" \in [1, oo) && "Fork_188" \in [1, oo) | [[[["Think_153" \in [1, oo) && "Fork_152" \in [1, oo) | ["Think_87" \in [1, oo) && "Fork_86" \in [1, oo) | ["Think_74" \in [1, oo) && "Fork_73" \in [1, oo) | [["Think_89" \in [1, oo) && "Fork_88" \in [1, oo) | [[[[["Think_199" \in [1, oo) && "Fork_198" \in [1, oo) | [[[[[[["Think_65" \in [1, oo) && "Fork_64" \in [1, oo) | [[["Think_117" \in [1, oo) && "Fork_116" \in [1, oo) | [[[["Think_93" \in [1, oo) && "Fork_92" \in [1, oo) | [[["Think_140" \in [1, oo) && "Fork_139" \in [1, oo) | ["Think_152" \in [1, oo) && "Fork_151" \in [1, oo) | [["Think_94" \in [1, oo) && "Fork_93" \in [1, oo) | ["Think_172" \in [1, oo) && "Fork_171" \in [1, oo) | [[[[[["Think_175" \in [1, oo) && "Fork_174" \in [1, oo) | ["Fork_105" \in [1, oo) && "Think_106" \in [1, oo) | [[[[["Think_128" \in [1, oo) && "Fork_127" \in [1, oo) | ["Think_83" \in [1, oo) && "Fork_82" \in [1, oo) | [[[[["Think_113" \in [1, oo) && "Fork_112" \in [1, oo) | ["Think_15" \in [1, oo) && "Fork_14" \in [1, oo) | [["Think_101" \in [1, oo) && "Fork_100" \in [1, oo) | ["Think_131" \in [1, oo) && "Fork_130" \in [1, oo) | ["Think_42" \in [1, oo) && "Fork_41" \in [1, oo) | [["Think_38" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Think_183" \in [1, oo) && "Fork_182" \in [1, oo) | [[["Think_196" \in [1, oo) && "Fork_195" \in [1, oo) | ["Think_52" \in [1, oo) && "Fork_51" \in [1, oo) | ["Think_138" \in [1, oo) && "Fork_137" \in [1, oo) | [["Think_168" \in [1, oo) && "Fork_167" \in [1, oo) | ["Think_25" \in [1, oo) && "Fork_24" \in [1, oo) | ["Think_53" \in [1, oo) && "Fork_52" \in [1, oo) | [[[[[["Think_169" \in [1, oo) && "Fork_168" \in [1, oo) | ["Think_60" \in [1, oo) && "Fork_59" \in [1, oo) | [[["Think_158" \in [1, oo) && "Fork_157" \in [1, oo) | [[[["Think_45" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_177" \in [1, oo) && "Think_178" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_46" \in [1, oo) | ["Think_192" \in [1, oo) && "Fork_191" \in [1, oo) | ["Think_120" \in [1, oo) && "Fork_119" \in [1, oo) | [["Think_13" \in [1, oo) && "Fork_12" \in [1, oo) | ["Think_34" \in [1, oo) && "Fork_33" \in [1, oo) | ["Think_63" \in [1, oo) && "Fork_62" \in [1, oo) | [[[["Think_154" \in [1, oo) && "Fork_153" \in [1, oo) | ["Think_176" \in [1, oo) && "Fork_175" \in [1, oo) | [[[["Think_142" \in [1, oo) && "Fork_141" \in [1, oo) | ["Think_88" \in [1, oo) && "Fork_87" \in [1, oo) | [[["Think_141" \in [1, oo) && "Fork_140" \in [1, oo) | ["Think_75" \in [1, oo) && "Fork_74" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | [["Think_114" \in [1, oo) && "Fork_113" \in [1, oo) | ["Think_11" \in [1, oo) && "Fork_10" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_17" \in [1, oo) | ["Think_99" \in [1, oo) && "Fork_98" \in [1, oo) | ["Think_164" \in [1, oo) && "Fork_163" \in [1, oo) | [["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Think_79" \in [1, oo) && "Fork_78" \in [1, oo) | [["Think_5" \in [1, oo) && "Fork_4" \in [1, oo) | ["Think_111" \in [1, oo) && "Fork_110" \in [1, oo) | ["Think_51" \in [1, oo) && "Fork_50" \in [1, oo) | [[[["Think_70" \in [1, oo) && "Fork_69" \in [1, oo) | [[["Think_98" \in [1, oo) && "Fork_97" \in [1, oo) | ["Think_188" \in [1, oo) && "Fork_187" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | [["Think_27" \in [1, oo) && "Fork_26" \in [1, oo) | ["Think_81" \in [1, oo) && "Fork_80" \in [1, oo) | [["Think_146" \in [1, oo) && "Fork_145" \in [1, oo) | ["Think_137" \in [1, oo) && "Fork_136" \in [1, oo) | [[[["Think_33" \in [1, oo) && "Fork_32" \in [1, oo) | ["Think_102" \in [1, oo) && "Fork_101" \in [1, oo) | ["Think_186" \in [1, oo) && "Fork_185" \in [1, oo) | ["Think_73" \in [1, oo) && "Fork_72" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_200" \in [1, oo) | ["Think_145" \in [1, oo) && "Fork_144" \in [1, oo) | ["Think_50" \in [1, oo) && "Fork_49" \in [1, oo) | ["Think_31" \in [1, oo) && "Fork_30" \in [1, oo) | ["Think_191" \in [1, oo) && "Fork_190" \in [1, oo) | ["Fork_142" \in [1, oo) && "Think_143" \in [1, oo) | [["Think_125" \in [1, oo) && "Fork_124" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | [[[[[[[[[[["Think_107" \in [1, oo) && "Fork_106" \in [1, oo) | [[[[[[[[[[[[["Think_9" \in [1, oo) && "Fork_8" \in [1, oo) | ["Think_68" \in [1, oo) && "Fork_67" \in [1, oo) | [[[[[[[[[[[[[[["Think_185" \in [1, oo) && "Fork_184" \in [1, oo) | "Think_151" \in [1, oo) && "Fork_150" \in [1, oo)] | "Think_46" \in [1, oo) && "Fork_45" \in [1, oo)] | "Think_155" \in [1, oo) && "Fork_154" \in [1, oo)] | "Think_86" \in [1, oo) && "Fork_85" \in [1, oo)] | "Think_115" \in [1, oo) && "Fork_114" \in [1, oo)] | "Think_92" \in [1, oo) && "Fork_91" \in [1, oo)] | "Think_103" \in [1, oo) && "Fork_102" \in [1, oo)] | "Think_123" \in [1, oo) && "Fork_122" \in [1, oo)] | "Think_194" \in [1, oo) && "Fork_193" \in [1, oo)] | "Think_66" \in [1, oo) && "Fork_65" \in [1, oo)] | "Think_21" \in [1, oo) && "Fork_20" \in [1, oo)] | "Think_165" \in [1, oo) && "Fork_164" \in [1, oo)] | "Think_12" \in [1, oo) && "Fork_11" \in [1, oo)] | "Think_124" \in [1, oo) && "Fork_123" \in [1, oo)] | "Think_69" \in [1, oo) && "Fork_68" \in [1, oo)]]] | "Think_119" \in [1, oo) && "Fork_118" \in [1, oo)] | "Think_82" \in [1, oo) && "Fork_81" \in [1, oo)] | "Think_177" \in [1, oo) && "Fork_176" \in [1, oo)] | "Think_62" \in [1, oo) && "Fork_61" \in [1, oo)] | "Think_6" \in [1, oo) && "Fork_5" \in [1, oo)] | "Think_193" \in [1, oo) && "Fork_192" \in [1, oo)] | "Think_20" \in [1, oo) && "Fork_19" \in [1, oo)] | "Think_80" \in [1, oo) && "Fork_79" \in [1, oo)] | "Think_67" \in [1, oo) && "Fork_66" \in [1, oo)] | "Think_163" \in [1, oo) && "Fork_162" \in [1, oo)] | "Think_148" \in [1, oo) && "Fork_147" \in [1, oo)] | "Think_136" \in [1, oo) && "Fork_135" \in [1, oo)]] | "Think_187" \in [1, oo) && "Fork_186" \in [1, oo)] | "Think_132" \in [1, oo) && "Fork_131" \in [1, oo)] | "Think_39" \in [1, oo) && "Fork_38" \in [1, oo)] | "Think_161" \in [1, oo) && "Fork_160" \in [1, oo)] | "Think_166" \in [1, oo) && "Fork_165" \in [1, oo)] | "Think_104" \in [1, oo) && "Fork_103" \in [1, oo)] | "Think_157" \in [1, oo) && "Fork_156" \in [1, oo)] | "Think_170" \in [1, oo) && "Fork_169" \in [1, oo)] | "Think_127" \in [1, oo) && "Fork_126" \in [1, oo)] | "Think_149" \in [1, oo) && "Fork_148" \in [1, oo)]]] | "Think_121" \in [1, oo) && "Fork_120" \in [1, oo)]]]]]]]]]]] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Think_95" \in [1, oo) && "Fork_94" \in [1, oo)] | "Think_109" \in [1, oo) && "Fork_108" \in [1, oo)]]] | "Think_160" \in [1, oo) && "Fork_159" \in [1, oo)]]] | "Think_129" \in [1, oo) && "Fork_128" \in [1, oo)]]]] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Think_91" \in [1, oo) && "Fork_90" \in [1, oo)]] | "Think_116" \in [1, oo) && "Fork_115" \in [1, oo)] | "Think_174" \in [1, oo) && "Fork_173" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)]]]] | "Think_200" \in [1, oo) && "Fork_199" \in [1, oo)]]] | "Think_147" \in [1, oo) && "Fork_146" \in [1, oo)]]]]]] | "Think_77" \in [1, oo) && "Fork_76" \in [1, oo)]]]] | "Think_22" \in [1, oo) && "Fork_21" \in [1, oo)] | "Think_54" \in [1, oo) && "Fork_53" \in [1, oo)]]] | "Think_184" \in [1, oo) && "Fork_183" \in [1, oo)] | "Think_105" \in [1, oo) && "Fork_104" \in [1, oo)] | "Think_40" \in [1, oo) && "Fork_39" \in [1, oo)]]] | "Think_76" \in [1, oo) && "Fork_75" \in [1, oo)] | "Think_84" \in [1, oo) && "Fork_83" \in [1, oo)] | "Think_108" \in [1, oo) && "Fork_107" \in [1, oo)]]]] | "Think_190" \in [1, oo) && "Fork_189" \in [1, oo)]]]]]] | "Think_195" \in [1, oo) && "Fork_194" \in [1, oo)] | "Think_32" \in [1, oo) && "Fork_31" \in [1, oo)] | "Think_55" \in [1, oo) && "Fork_54" \in [1, oo)]] | "Think_10" \in [1, oo) && "Fork_9" \in [1, oo)] | "Think_162" \in [1, oo) && "Fork_161" \in [1, oo)]]] | "Think_167" \in [1, oo) && "Fork_166" \in [1, oo)] | "Think_181" \in [1, oo) && "Fork_180" \in [1, oo)] | "Think_43" \in [1, oo) && "Fork_42" \in [1, oo)] | "Think_35" \in [1, oo) && "Fork_34" \in [1, oo)] | "Think_14" \in [1, oo) && "Fork_13" \in [1, oo)]]]] | "Think_57" \in [1, oo) && "Fork_56" \in [1, oo)]]]] | "Think_59" \in [1, oo) && "Fork_58" \in [1, oo)] | "Think_182" \in [1, oo) && "Fork_181" \in [1, oo)]]]] | "Think_26" \in [1, oo) && "Fork_25" \in [1, oo)]]]] | "Think_110" \in [1, oo) && "Fork_109" \in [1, oo)]]] | "Think_144" \in [1, oo) && "Fork_143" \in [1, oo)] | "Think_30" \in [1, oo) && "Fork_29" \in [1, oo)] | "Think_58" \in [1, oo) && "Fork_57" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)]]] | "Think_56" \in [1, oo) && "Fork_55" \in [1, oo)] | "Think_198" \in [1, oo) && "Fork_197" \in [1, oo)] | "Think_180" \in [1, oo) && "Fork_179" \in [1, oo)] | "Think_112" \in [1, oo) && "Fork_111" \in [1, oo)]]] | "Think_64" \in [1, oo) && "Fork_63" \in [1, oo)] | "Think_90" \in [1, oo) && "Fork_89" \in [1, oo)] | "Think_134" \in [1, oo) && "Fork_133" \in [1, oo)] | "Think_41" \in [1, oo) && "Fork_40" \in [1, oo)] | "Think_78" \in [1, oo) && "Fork_77" \in [1, oo)]]] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)]]] | "Think_135" \in [1, oo) && "Fork_134" \in [1, oo)] | "Think_71" \in [1, oo) && "Fork_70" \in [1, oo)]] | "Think_48" \in [1, oo) && "Fork_47" \in [1, oo)] | "Think_122" \in [1, oo) && "Fork_121" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_23" \in [1, oo)]] | "Think_130" \in [1, oo) && "Fork_129" \in [1, oo)] | "Think_126" \in [1, oo) && "Fork_125" \in [1, oo)]] | "Think_171" \in [1, oo) && "Fork_170" \in [1, oo)] | "Think_159" \in [1, oo) && "Fork_158" \in [1, oo)] | "Think_197" \in [1, oo) && "Fork_196" \in [1, oo)] | "Think_96" \in [1, oo) && "Fork_95" \in [1, oo)] | "Think_179" \in [1, oo) && "Fork_178" \in [1, oo)] | "Think_85" \in [1, oo) && "Fork_84" \in [1, oo)]] | "Think_156" \in [1, oo) && "Fork_155" \in [1, oo)] | "Think_37" \in [1, oo) && "Fork_36" \in [1, oo)] | "Think_36" \in [1, oo) && "Fork_35" \in [1, oo)] | "Think_61" \in [1, oo) && "Fork_60" \in [1, oo)]] | "Think_97" \in [1, oo) && "Fork_96" \in [1, oo)]]]] | "Think_118" \in [1, oo) && "Fork_117" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_150" \in [1, oo) && "Fork_149" \in [1, oo)]]] | "Think_100" \in [1, oo) && "Fork_99" \in [1, oo)]]]] | "Think_7" \in [1, oo) && "Fork_6" \in [1, oo)] | "Think_139" \in [1, oo) && "Fork_138" \in [1, oo)]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_152 + Eat_143 ) + Eat_189 ) + Eat_200 ) + Eat_197 ) + Eat_95 ) + Eat_193 ) + Eat_92 ) + Eat_26 ) + Eat_141 ) + Eat_64 ) + Eat_31 ) + Eat_83 ) + Eat_196 ) + Eat_96 ) + Eat_175 ) + Eat_162 ) + Eat_100 ) + Eat_108 ) + Eat_97 ) + Eat_199 ) + Eat_118 ) + Eat_76 ) + Eat_50 ) + Eat_177 ) + Eat_43 ) + Eat_53 ) + Eat_15 ) + Eat_68 ) + Eat_190 ) + Eat_156 ) + Eat_19 ) + Eat_168 ) + Eat_106 ) + Eat_28 ) + Eat_37 ) + Eat_181 ) + Eat_110 ) + Eat_25 ) + Eat_150 ) + Eat_29 ) + Eat_23 ) + Eat_72 ) + Eat_129 ) + Eat_20 ) + Eat_60 ) + Eat_144 ) + Eat_178 ) + Eat_134 ) + Eat_11 ) + Eat_84 ) + Eat_35 ) + Eat_18 ) + Eat_195 ) + Eat_69 ) + Eat_145 ) + Eat_130 ) + Eat_126 ) + Eat_121 ) + Eat_140 ) + Eat_52 ) + Eat_109 ) + Eat_98 ) + Eat_147 ) + Eat_38 ) + Eat_27 ) + Eat_24 ) + Eat_81 ) + Eat_74 ) + Eat_165 ) + Eat_164 ) + Eat_191 ) + Eat_159 ) + Eat_14 ) + Eat_40 ) + Eat_49 ) + Eat_107 ) + Eat_116 ) + Eat_176 ) + Eat_66 ) + Eat_87 ) + Eat_67 ) + Eat_46 ) + Eat_70 ) + Eat_34 ) + Eat_185 ) + Eat_65 ) + Eat_153 ) + Eat_115 ) + Eat_103 ) + Eat_101 ) + Eat_63 ) + Eat_80 ) + Eat_88 ) + Eat_61 ) + Eat_149 ) + Eat_90 ) + Eat_94 ) + Eat_6 ) + Eat_112 ) + Eat_36 ) + Eat_120 ) + Eat_59 ) + Eat_170 ) + Eat_186 ) + Eat_45 ) + Eat_16 ) + Eat_123 ) + Eat_2 ) + Eat_137 ) + Eat_55 ) + Eat_138 ) + Eat_184 ) + Eat_157 ) + Eat_30 ) + Eat_3 ) + Eat_124 ) + Eat_21 ) + Eat_146 ) + Eat_167 ) + Eat_132 ) + Eat_82 ) + Eat_179 ) + Eat_17 ) + Eat_85 ) + Eat_99 ) + Eat_161 ) + Eat_13 ) + Eat_79 ) + Eat_54 ) + Eat_160 ) + Eat_169 ) + Eat_114 ) + Eat_155 ) + Eat_119 ) + Eat_91 ) + Eat_105 ) + Eat_33 ) + Eat_75 ) + Eat_51 ) + Eat_10 ) + Eat_122 ) + Eat_174 ) + Eat_71 ) + Eat_133 ) + Eat_166 ) + Eat_104 ) + Eat_58 ) + Eat_48 ) + Eat_171 ) + Eat_148 ) + Eat_192 ) + Eat_131 ) + Eat_7 ) + Eat_78 ) + Eat_125 ) + Eat_5 ) + Eat_86 ) + Eat_142 ) + Eat_42 ) + Eat_172 ) + Eat_158 ) + Eat_22 ) + Eat_198 ) + Eat_41 ) + Eat_113 ) + Eat_117 ) + Eat_194 ) + Eat_180 ) + Eat_128 ) + Eat_151 ) + Eat_32 ) + Eat_182 ) + Eat_47 ) + Eat_136 ) + Eat_57 ) + Eat_44 ) + Eat_163 ) + Eat_12 ) + Eat_187 ) + Eat_4 ) + Eat_135 ) + Eat_139 ) + Eat_39 ) + Eat_89 ) + Eat_77 ) + Eat_173 ) + Eat_102 ) + Eat_93 ) + Eat_56 ) + Eat_73 ) + Eat_9 ) + Eat_154 ) + Eat_188 ) + Eat_1 ) + Eat_111 ) + Eat_127 ) + Eat_8 ) + Eat_62 ) + Eat_183 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_148 + Think_104 ) + Think_90 ) + Think_163 ) + Think_71 ) + Think_199 ) + Think_191 ) + Think_93 ) + Think_94 ) + Think_198 ) + Think_115 ) + Think_36 ) + Think_51 ) + Think_112 ) + Think_106 ) + Think_33 ) + Think_7 ) + Think_32 ) + Think_124 ) + Think_187 ) + Think_96 ) + Think_18 ) + Think_134 ) + Think_65 ) + Think_111 ) + Think_40 ) + Think_13 ) + Think_67 ) + Think_3 ) + Think_128 ) + Think_107 ) + Think_81 ) + Think_34 ) + Think_172 ) + Think_10 ) + Think_179 ) + Think_136 ) + Think_82 ) + Think_144 ) + Think_11 ) + Think_76 ) + Think_66 ) + Think_79 ) + Think_53 ) + Think_135 ) + Think_141 ) + Think_110 ) + Think_98 ) + Think_105 ) + Think_89 ) + Think_173 ) + Think_162 ) + Think_59 ) + Think_91 ) + Think_174 ) + Think_26 ) + Think_132 ) + Think_123 ) + Think_183 ) + Think_64 ) + Think_126 ) + Think_170 ) + Think_9 ) + Think_185 ) + Think_164 ) + Think_47 ) + Think_147 ) + Think_42 ) + Think_58 ) + Think_85 ) + Think_31 ) + Think_130 ) + Think_152 ) + Think_27 ) + Think_15 ) + Think_87 ) + Think_38 ) + Think_1 ) + Think_20 ) + Think_181 ) + Think_23 ) + Think_84 ) + Think_77 ) + Think_21 ) + Think_143 ) + Think_122 ) + Think_160 ) + Think_166 ) + Think_17 ) + Think_131 ) + Think_39 ) + Think_178 ) + Think_68 ) + Think_5 ) + Think_102 ) + Think_149 ) + Think_69 ) + Think_55 ) + Think_193 ) + Think_70 ) + Think_49 ) + Think_125 ) + Think_61 ) + Think_133 ) + Think_161 ) + Think_24 ) + Think_62 ) + Think_119 ) + Think_109 ) + Think_92 ) + Think_54 ) + Think_194 ) + Think_60 ) + Think_200 ) + Think_14 ) + Think_127 ) + Think_168 ) + Think_97 ) + Think_142 ) + Think_44 ) + Think_57 ) + Think_158 ) + Think_146 ) + Think_83 ) + Think_16 ) + Think_50 ) + Think_167 ) + Think_188 ) + Think_195 ) + Think_197 ) + Think_157 ) + Think_169 ) + Think_88 ) + Think_137 ) + Think_113 ) + Think_72 ) + Think_140 ) + Think_37 ) + Think_41 ) + Think_176 ) + Think_153 ) + Think_12 ) + Think_171 ) + Think_114 ) + Think_151 ) + Think_156 ) + Think_2 ) + Think_8 ) + Think_45 ) + Think_189 ) + Think_30 ) + Think_75 ) + Think_100 ) + Think_139 ) + Think_63 ) + Think_175 ) + Think_138 ) + Think_180 ) + Think_192 ) + Think_43 ) + Think_48 ) + Think_46 ) + Think_101 ) + Think_165 ) + Think_52 ) + Think_19 ) + Think_80 ) + Think_28 ) + Think_184 ) + Think_6 ) + Think_86 ) + Think_35 ) + Think_73 ) + Think_186 ) + Think_108 ) + Think_116 ) + Think_182 ) + Think_56 ) + Think_103 ) + Think_22 ) + Think_74 ) + Think_121 ) + Think_150 ) + Think_95 ) + Think_29 ) + Think_177 ) + Think_120 ) + Think_159 ) + Think_196 ) + Think_154 ) + Think_118 ) + Think_78 ) + Think_4 ) + Think_117 ) + Think_155 ) + Think_145 ) + Think_25 ) + Think_190 ) + Think_129 ) + Think_99 ) | ["Think_139" \in [1, oo) && "Fork_138" \in [1, oo) | ["Think_7" \in [1, oo) && "Fork_6" \in [1, oo) | [[[["Think_100" \in [1, oo) && "Fork_99" \in [1, oo) | [[["Think_150" \in [1, oo) && "Fork_149" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_118" \in [1, oo) && "Fork_117" \in [1, oo) | [[[["Think_97" \in [1, oo) && "Fork_96" \in [1, oo) | [["Think_61" \in [1, oo) && "Fork_60" \in [1, oo) | ["Think_36" \in [1, oo) && "Fork_35" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_36" \in [1, oo) | ["Think_156" \in [1, oo) && "Fork_155" \in [1, oo) | [["Think_85" \in [1, oo) && "Fork_84" \in [1, oo) | ["Think_179" \in [1, oo) && "Fork_178" \in [1, oo) | ["Think_96" \in [1, oo) && "Fork_95" \in [1, oo) | ["Think_197" \in [1, oo) && "Fork_196" \in [1, oo) | ["Think_159" \in [1, oo) && "Fork_158" \in [1, oo) | ["Think_171" \in [1, oo) && "Fork_170" \in [1, oo) | [["Think_126" \in [1, oo) && "Fork_125" \in [1, oo) | ["Think_130" \in [1, oo) && "Fork_129" \in [1, oo) | [["Think_24" \in [1, oo) && "Fork_23" \in [1, oo) | ["Think_122" \in [1, oo) && "Fork_121" \in [1, oo) | ["Think_48" \in [1, oo) && "Fork_47" \in [1, oo) | [["Think_71" \in [1, oo) && "Fork_70" \in [1, oo) | ["Think_135" \in [1, oo) && "Fork_134" \in [1, oo) | [[["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | [[["Think_78" \in [1, oo) && "Fork_77" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_40" \in [1, oo) | ["Think_134" \in [1, oo) && "Fork_133" \in [1, oo) | ["Think_90" \in [1, oo) && "Fork_89" \in [1, oo) | ["Think_64" \in [1, oo) && "Fork_63" \in [1, oo) | [[["Think_112" \in [1, oo) && "Fork_111" \in [1, oo) | ["Think_180" \in [1, oo) && "Fork_179" \in [1, oo) | ["Think_198" \in [1, oo) && "Fork_197" \in [1, oo) | ["Think_56" \in [1, oo) && "Fork_55" \in [1, oo) | [[["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Think_58" \in [1, oo) && "Fork_57" \in [1, oo) | ["Think_30" \in [1, oo) && "Fork_29" \in [1, oo) | ["Think_144" \in [1, oo) && "Fork_143" \in [1, oo) | [[["Think_110" \in [1, oo) && "Fork_109" \in [1, oo) | [[[["Think_26" \in [1, oo) && "Fork_25" \in [1, oo) | [[[["Think_182" \in [1, oo) && "Fork_181" \in [1, oo) | ["Think_59" \in [1, oo) && "Fork_58" \in [1, oo) | [[[["Think_57" \in [1, oo) && "Fork_56" \in [1, oo) | [[[["Think_14" \in [1, oo) && "Fork_13" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_34" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_42" \in [1, oo) | ["Think_181" \in [1, oo) && "Fork_180" \in [1, oo) | ["Think_167" \in [1, oo) && "Fork_166" \in [1, oo) | [[["Think_162" \in [1, oo) && "Fork_161" \in [1, oo) | ["Think_10" \in [1, oo) && "Fork_9" \in [1, oo) | [["Think_55" \in [1, oo) && "Fork_54" \in [1, oo) | ["Think_32" \in [1, oo) && "Fork_31" \in [1, oo) | ["Think_195" \in [1, oo) && "Fork_194" \in [1, oo) | [[[[[["Think_190" \in [1, oo) && "Fork_189" \in [1, oo) | [[[["Think_108" \in [1, oo) && "Fork_107" \in [1, oo) | ["Think_84" \in [1, oo) && "Fork_83" \in [1, oo) | ["Think_76" \in [1, oo) && "Fork_75" \in [1, oo) | [[["Think_40" \in [1, oo) && "Fork_39" \in [1, oo) | ["Think_105" \in [1, oo) && "Fork_104" \in [1, oo) | ["Think_184" \in [1, oo) && "Fork_183" \in [1, oo) | [[["Think_54" \in [1, oo) && "Fork_53" \in [1, oo) | ["Think_22" \in [1, oo) && "Fork_21" \in [1, oo) | [[[["Think_77" \in [1, oo) && "Fork_76" \in [1, oo) | [[[[[["Think_147" \in [1, oo) && "Fork_146" \in [1, oo) | [[["Think_200" \in [1, oo) && "Fork_199" \in [1, oo) | [[[["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_174" \in [1, oo) && "Fork_173" \in [1, oo) | ["Think_116" \in [1, oo) && "Fork_115" \in [1, oo) | [["Think_91" \in [1, oo) && "Fork_90" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | [[[["Think_129" \in [1, oo) && "Fork_128" \in [1, oo) | [[["Think_160" \in [1, oo) && "Fork_159" \in [1, oo) | [[["Think_109" \in [1, oo) && "Fork_108" \in [1, oo) | ["Think_95" \in [1, oo) && "Fork_94" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | [[[[[[[[[[["Think_121" \in [1, oo) && "Fork_120" \in [1, oo) | [[["Think_149" \in [1, oo) && "Fork_148" \in [1, oo) | ["Think_127" \in [1, oo) && "Fork_126" \in [1, oo) | ["Think_170" \in [1, oo) && "Fork_169" \in [1, oo) | ["Think_157" \in [1, oo) && "Fork_156" \in [1, oo) | ["Think_104" \in [1, oo) && "Fork_103" \in [1, oo) | ["Think_166" \in [1, oo) && "Fork_165" \in [1, oo) | ["Think_161" \in [1, oo) && "Fork_160" \in [1, oo) | ["Think_39" \in [1, oo) && "Fork_38" \in [1, oo) | ["Think_132" \in [1, oo) && "Fork_131" \in [1, oo) | ["Think_187" \in [1, oo) && "Fork_186" \in [1, oo) | [["Think_136" \in [1, oo) && "Fork_135" \in [1, oo) | ["Think_148" \in [1, oo) && "Fork_147" \in [1, oo) | ["Think_163" \in [1, oo) && "Fork_162" \in [1, oo) | ["Think_67" \in [1, oo) && "Fork_66" \in [1, oo) | ["Think_80" \in [1, oo) && "Fork_79" \in [1, oo) | ["Think_20" \in [1, oo) && "Fork_19" \in [1, oo) | ["Think_193" \in [1, oo) && "Fork_192" \in [1, oo) | ["Think_6" \in [1, oo) && "Fork_5" \in [1, oo) | ["Think_62" \in [1, oo) && "Fork_61" \in [1, oo) | ["Think_177" \in [1, oo) && "Fork_176" \in [1, oo) | ["Think_82" \in [1, oo) && "Fork_81" \in [1, oo) | ["Think_119" \in [1, oo) && "Fork_118" \in [1, oo) | [[["Think_69" \in [1, oo) && "Fork_68" \in [1, oo) | ["Think_124" \in [1, oo) && "Fork_123" \in [1, oo) | ["Think_12" \in [1, oo) && "Fork_11" \in [1, oo) | ["Think_165" \in [1, oo) && "Fork_164" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_20" \in [1, oo) | ["Think_66" \in [1, oo) && "Fork_65" \in [1, oo) | ["Think_194" \in [1, oo) && "Fork_193" \in [1, oo) | ["Think_123" \in [1, oo) && "Fork_122" \in [1, oo) | ["Think_103" \in [1, oo) && "Fork_102" \in [1, oo) | ["Think_92" \in [1, oo) && "Fork_91" \in [1, oo) | ["Think_115" \in [1, oo) && "Fork_114" \in [1, oo) | ["Think_86" \in [1, oo) && "Fork_85" \in [1, oo) | ["Think_155" \in [1, oo) && "Fork_154" \in [1, oo) | ["Think_46" \in [1, oo) && "Fork_45" \in [1, oo) | ["Think_151" \in [1, oo) && "Fork_150" \in [1, oo) | "Think_185" \in [1, oo) && "Fork_184" \in [1, oo)]]]]]]]]]]]]]]] | "Think_68" \in [1, oo) && "Fork_67" \in [1, oo)] | "Think_9" \in [1, oo) && "Fork_8" \in [1, oo)]]]]]]]]]]]]] | "Think_107" \in [1, oo) && "Fork_106" \in [1, oo)]]]]]]]]]]] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Think_125" \in [1, oo) && "Fork_124" \in [1, oo)]] | "Fork_142" \in [1, oo) && "Think_143" \in [1, oo)] | "Think_191" \in [1, oo) && "Fork_190" \in [1, oo)] | "Think_31" \in [1, oo) && "Fork_30" \in [1, oo)] | "Think_50" \in [1, oo) && "Fork_49" \in [1, oo)] | "Think_145" \in [1, oo) && "Fork_144" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_200" \in [1, oo)] | "Think_73" \in [1, oo) && "Fork_72" \in [1, oo)] | "Think_186" \in [1, oo) && "Fork_185" \in [1, oo)] | "Think_102" \in [1, oo) && "Fork_101" \in [1, oo)] | "Think_33" \in [1, oo) && "Fork_32" \in [1, oo)]]]] | "Think_137" \in [1, oo) && "Fork_136" \in [1, oo)] | "Think_146" \in [1, oo) && "Fork_145" \in [1, oo)]] | "Think_81" \in [1, oo) && "Fork_80" \in [1, oo)] | "Think_27" \in [1, oo) && "Fork_26" \in [1, oo)]] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Think_188" \in [1, oo) && "Fork_187" \in [1, oo)] | "Think_98" \in [1, oo) && "Fork_97" \in [1, oo)]]] | "Think_70" \in [1, oo) && "Fork_69" \in [1, oo)]]]] | "Think_51" \in [1, oo) && "Fork_50" \in [1, oo)] | "Think_111" \in [1, oo) && "Fork_110" \in [1, oo)] | "Think_5" \in [1, oo) && "Fork_4" \in [1, oo)]] | "Think_79" \in [1, oo) && "Fork_78" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)]] | "Think_164" \in [1, oo) && "Fork_163" \in [1, oo)] | "Think_99" \in [1, oo) && "Fork_98" \in [1, oo)] | "Think_18" \in [1, oo) && "Fork_17" \in [1, oo)] | "Think_11" \in [1, oo) && "Fork_10" \in [1, oo)] | "Think_114" \in [1, oo) && "Fork_113" \in [1, oo)]] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Think_75" \in [1, oo) && "Fork_74" \in [1, oo)] | "Think_141" \in [1, oo) && "Fork_140" \in [1, oo)]]] | "Think_88" \in [1, oo) && "Fork_87" \in [1, oo)] | "Think_142" \in [1, oo) && "Fork_141" \in [1, oo)]]]] | "Think_176" \in [1, oo) && "Fork_175" \in [1, oo)] | "Think_154" \in [1, oo) && "Fork_153" \in [1, oo)]]]] | "Think_63" \in [1, oo) && "Fork_62" \in [1, oo)] | "Think_34" \in [1, oo) && "Fork_33" \in [1, oo)] | "Think_13" \in [1, oo) && "Fork_12" \in [1, oo)]] | "Think_120" \in [1, oo) && "Fork_119" \in [1, oo)] | "Think_192" \in [1, oo) && "Fork_191" \in [1, oo)] | "Think_47" \in [1, oo) && "Fork_46" \in [1, oo)] | "Fork_177" \in [1, oo) && "Think_178" \in [1, oo)] | "Think_45" \in [1, oo) && "Fork_44" \in [1, oo)]]]] | "Think_158" \in [1, oo) && "Fork_157" \in [1, oo)]]] | "Think_60" \in [1, oo) && "Fork_59" \in [1, oo)] | "Think_169" \in [1, oo) && "Fork_168" \in [1, oo)]]]]]] | "Think_53" \in [1, oo) && "Fork_52" \in [1, oo)] | "Think_25" \in [1, oo) && "Fork_24" \in [1, oo)] | "Think_168" \in [1, oo) && "Fork_167" \in [1, oo)]] | "Think_138" \in [1, oo) && "Fork_137" \in [1, oo)] | "Think_52" \in [1, oo) && "Fork_51" \in [1, oo)] | "Think_196" \in [1, oo) && "Fork_195" \in [1, oo)]]] | "Think_183" \in [1, oo) && "Fork_182" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)] | "Think_38" \in [1, oo) && "Fork_37" \in [1, oo)]] | "Think_42" \in [1, oo) && "Fork_41" \in [1, oo)] | "Think_131" \in [1, oo) && "Fork_130" \in [1, oo)] | "Think_101" \in [1, oo) && "Fork_100" \in [1, oo)]] | "Think_15" \in [1, oo) && "Fork_14" \in [1, oo)] | "Think_113" \in [1, oo) && "Fork_112" \in [1, oo)]]]]] | "Think_83" \in [1, oo) && "Fork_82" \in [1, oo)] | "Think_128" \in [1, oo) && "Fork_127" \in [1, oo)]]]]] | "Fork_105" \in [1, oo) && "Think_106" \in [1, oo)] | "Think_175" \in [1, oo) && "Fork_174" \in [1, oo)]]]]]] | "Think_172" \in [1, oo) && "Fork_171" \in [1, oo)] | "Think_94" \in [1, oo) && "Fork_93" \in [1, oo)]] | "Think_152" \in [1, oo) && "Fork_151" \in [1, oo)] | "Think_140" \in [1, oo) && "Fork_139" \in [1, oo)]]] | "Think_93" \in [1, oo) && "Fork_92" \in [1, oo)]]]] | "Think_117" \in [1, oo) && "Fork_116" \in [1, oo)]]] | "Think_65" \in [1, oo) && "Fork_64" \in [1, oo)]]]]]]] | "Think_199" \in [1, oo) && "Fork_198" \in [1, oo)]]]]] | "Think_89" \in [1, oo) && "Fork_88" \in [1, oo)]] | "Think_74" \in [1, oo) && "Fork_73" \in [1, oo)] | "Think_87" \in [1, oo) && "Fork_86" \in [1, oo)] | "Think_153" \in [1, oo) && "Fork_152" \in [1, oo)]]]] | "Think_189" \in [1, oo) && "Fork_188" \in [1, oo)] | "Think_49" \in [1, oo) && "Fork_48" \in [1, oo)]] | "Fork_172" \in [1, oo) && "Think_173" \in [1, oo)] | "Think_72" \in [1, oo) && "Fork_71" \in [1, oo)] | "Think_133" \in [1, oo) && "Fork_132" \in [1, oo)]]]]]]]


before gc: list nodes free: 1932561

after gc: idd nodes used:20784, unused:15979216; list nodes free:71203217

before gc: list nodes free: 2166304

after gc: idd nodes used:20094, unused:15979906; list nodes free:71206169

before gc: list nodes free: 2140357

after gc: idd nodes used:19056, unused:15980944; list nodes free:71210666

before gc: list nodes free: 2108362

after gc: idd nodes used:19302, unused:15980698; list nodes free:71209524

before gc: list nodes free: 2062800

after gc: idd nodes used:17578, unused:15982422; list nodes free:71217046

before gc: list nodes free: 1967013

after gc: idd nodes used:17405, unused:15982595; list nodes free:71217714