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

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

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

execution on node 4: quadhexa-2.u-paris10.fr (runId=136983895500200_n_4)
=====================================================================
runnning marcie on SharedMemory-PT-000200 (CTLCardinalityComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is SharedMemory-PT-000200, examination is CTLCardinalityComparison
=====================================================================

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

START 1369868033

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 40601 NrTr: 80200)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369868080

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

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

mcc/mcc_parse.cc:759: Exception: parse error ctl p_1860_cardinalitycomparison_eq_x: E F (X ((|marking(Active_199)|+|marking(Active_62)|+|marking(Active_19)|+|marking(Active_146)|+|marking(Active_84)|+|marking(Active_110)|+|marking(Active_158)|+|marking(Active_112)|+|marking(Active_96)|+|marking(Active_176)|+|marking(Active_123)|+|marking(Active_184)|+|marking(Active_7)|+|marking(Active_142)|+|marking(Active_93)|+|marking(Active_59)|+|marking(Active_76)|+|marking(Active_198)|+|marking(Active_116)|+|marking(Active_47)|+|marking(Active_11)|+|marking(Active_154)|+|marking(Active_10)|+|marking(Active_80)|+|marking(Active_185)|+|marking(Active_41)|+|marking(Active_78)|+|marking(Active_121)|+|marking(Active_183)|+|marking(Active_61)|+|marking(Active_94)|+|marking(Active_103)|+|marking(Active_191)|+|marking(Active_107)|+|marking(Active_148)|+|marking(Active_140)|+|marking(Active_53)|+|marking(Active_29)|+|marking(Active_1)|+|marking(Active_79)|+|marking(Active_16)|+|marking(Active_74)|+|marking(Active_115)|+|marking(Active_22)|+|marking(Active_132)|+|marking(Active_126)|+|marking(Active_36)|+|marking(Active_38)|+|marking(Active_90)|+|marking(Active_113)|+|marking(Active_14)|+|marking(Active_46)|+|marking(Active_153)|+|marking(Active_169)|+|marking(Active_188)|+|marking(Active_147)|+|marking(Active_145)|+|marking(Active_179)|+|marking(Active_25)|+|marking(Active_72)|+|marking(Active_125)|+|marking(Active_75)|+|marking(Active_87)|+|marking(Active_175)|+|marking(Active_133)|+|marking(Active_102)|+|marking(Active_71)|+|marking(Active_104)|+|marking(Active_180)|+|marking(Active_97)|+|marking(Active_18)|+|marking(Active_157)|+|marking(Active_88)|+|marking(Active_85)|+|marking(Active_70)|+|marking(Active_149)|+|marking(Active_15)|+|marking(Active_49)|+|marking(Active_89)|+|marking(Active_50)|+|marking(Active_129)|+|marking(Active_17)|+|marking(Active_40)|+|marking(Active_114)|+|marking(Active_57)|+|marking(Active_69)|+|marking(Active_77)|+|marking(Active_178)|+|marking(Active_58)|+|marking(Active_144)|+|marking(Active_182)|+|marking(Active_119)|+|marking(Active_9)|+|marking(Active_105)|+|marking(Active_44)|+|marking(Active_23)|+|marking(Active_111)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_189)|+|marking(Active_197)|+|marking(Active_174)|+|marking(Active_82)|+|marking(Active_124)|+|marking(Active_195)|+|marking(Active_137)|+|marking(Active_55)|+|marking(Active_99)|+|marking(Active_4)|+|marking(Active_48)|+|marking(Active_12)|+|marking(Active_171)|+|marking(Active_151)|+|marking(Active_181)|+|marking(Active_81)|+|marking(Active_51)|+|marking(Active_3)|+|marking(Active_150)|+|marking(Active_162)|+|marking(Active_128)|+|marking(Active_30)|+|marking(Active_108)|+|marking(Active_136)|+|marking(Active_106)|+|marking(Active_91)|+|marking(Active_167)|+|marking(Active_120)|+|marking(Active_177)|+|marking(Active_152)|+|marking(Active_43)|+|marking(Active_117)|+|marking(Active_54)|+|marking(Active_139)|+|marking(Active_42)|+|marking(Active_21)|+|marking(Active_63)|+|marking(Active_138)|+|marking(Active_52)|+|marking(Active_27)|+|marking(Active_73)|+|marking(Active_156)|+|marking(Active_194)|+|marking(Active_98)|+|marking(Active_56)|+|marking(Active_109)|+|marking(Active_39)|+|marking(Active_67)|+|marking(Active_32)|+|marking(Active_173)|+|marking(Active_130)|+|marking(Active_159)|+|marking(Active_13)|+|marking(Active_35)|+|marking(Active_192)|+|marking(Active_100)|+|marking(Active_161)|+|marking(Active_37)|+|marking(Active_31)|+|marking(Active_65)|+|marking(Active_155)|+|marking(Active_168)|+|marking(Active_95)|+|marking(Active_131)|+|marking(Active_165)|+|marking(Active_24)|+|marking(Active_60)|+|marking(Active_8)|+|marking(Active_20)|+|marking(Active_160)|+|marking(Active_143)|+|marking(Active_26)|+|marking(Active_163)|+|marking(Active_200)|+|marking(Active_186)|+|marking(Active_172)|+|marking(Active_135)|+|marking(Active_68)|+|marking(Active_83)|+|marking(Active_86)|+|marking(Active_166)|+|marking(Active_193)|+|marking(Active_164)|+|marking(Active_196)|+|marking(Active_66)|+|marking(Active_64)|+|marking(Active_28)|+|marking(Active_122)|+|marking(Active_101)|+|marking(Active_5)|+|marking(Active_33)|+|marking(Active_141)|+|marking(Active_6)|+|marking(Active_190)|+|marking(Active_134)|+|marking(Active_170)|+|marking(Active_45)|+|marking(Active_118)|+|marking(Active_187)|+|marking(Active_92)|+|marking(Active_127)|)!=(|marking(Queue_51)|+|marking(Queue_7)|+|marking(Queue_184)|+|marking(Queue_89)|+|marking(Queue_138)|+|marking(Queue_8)|+|marking(Queue_31)|+|marking(Queue_136)|+|marking(Queue_33)|+|marking(Queue_73)|+|marking(Queue_104)|+|marking(Queue_66)|+|marking(Queue_100)|+|marking(Queue_129)|+|marking(Queue_59)|+|marking(Queue_4)|+|marking(Queue_75)|+|marking(Queue_188)|+|marking(Queue_42)|+|marking(Queue_58)|+|marking(Queue_119)|+|marking(Queue_18)|+|marking(Queue_14)|+|marking(Queue_172)|+|marking(Queue_62)|+|marking(Queue_103)|+|marking(Queue_24)|+|marking(Queue_5)|+|marking(Queue_50)|+|marking(Queue_12)|+|marking(Queue_157)|+|marking(Queue_141)|+|marking(Queue_106)|+|marking(Queue_171)|+|marking(Queue_166)|+|marking(Queue_167)|+|marking(Queue_126)|+|marking(Queue_37)|+|marking(Queue_110)|+|marking(Queue_165)|+|marking(Queue_81)|+|marking(Queue_133)|+|marking(Queue_158)|+|marking(Queue_20)|+|marking(Queue_130)|+|marking(Queue_197)|+|marking(Queue_153)|+|marking(Queue_139)|+|marking(Queue_160)|+|marking(Queue_69)|+|marking(Queue_49)|+|marking(Queue_200)|+|marking(Queue_163)|+|marking(Queue_22)|+|marking(Queue_88)|+|marking(Queue_190)|+|marking(Queue_192)|+|marking(Queue_74)|+|marking(Queue_17)|+|marking(Queue_169)|+|marking(Queue_91)|+|marking(Queue_148)|+|marking(Queue_36)|+|marking(Queue_54)|+|marking(Queue_57)|+|marking(Queue_71)|+|marking(Queue_3)|+|marking(Queue_183)|+|marking(Queue_179)|+|marking(Queue_187)|+|marking(Queue_94)|+|marking(Queue_80)|+|marking(Queue_112)|+|marking(Queue_156)|+|marking(Queue_131)|+|marking(Queue_147)|+|marking(Queue_149)|+|marking(Queue_40)|+|marking(Queue_23)|+|marking(Queue_181)|+|marking(Queue_45)|+|marking(Queue_108)|+|marking(Queue_48)|+|marking(Queue_173)|+|marking(Queue_162)|+|marking(Queue_182)|+|marking(Queue_64)|+|marking(Queue_29)|+|marking(Queue_168)|+|marking(Queue_95)|+|marking(Queue_101)|+|marking(Queue_53)|+|marking(Queue_13)|+|marking(Queue_193)|+|marking(Queue_142)|+|marking(Queue_120)|+|marking(Queue_194)|+|marking(Queue_185)|+|marking(Queue_61)|+|marking(Queue_63)|+|marking(Queue_161)|+|marking(Queue_111)|+|marking(Queue_68)|+|marking(Queue_92)|+|marking(Queue_198)|+|marking(Queue_121)|+|marking(Queue_195)|+|marking(Queue_132)|+|marking(Queue_65)|+|marking(Queue_16)|+|marking(Queue_44)|+|marking(Queue_79)|+|marking(Queue_19)|+|marking(Queue_154)|+|marking(Queue_143)|+|marking(Queue_178)|+|marking(Queue_6)|+|marking(Queue_146)|+|marking(Queue_199)|+|marking(Queue_109)|+|marking(Queue_140)|+|marking(Queue_98)|+|marking(Queue_134)|+|marking(Queue_56)|+|marking(Queue_170)|+|marking(Queue_114)|+|marking(Queue_52)|+|marking(Queue_97)|+|marking(Queue_135)|+|marking(Queue_38)|+|marking(Queue_86)|+|marking(Queue_30)|+|marking(Queue_107)|+|marking(Queue_189)|+|marking(Queue_93)|+|marking(Queue_10)|+|marking(Queue_145)|+|marking(Queue_115)|+|marking(Queue_164)|+|marking(Queue_78)|+|marking(Queue_150)|+|marking(Queue_152)|+|marking(Queue_26)|+|marking(Queue_43)|+|marking(Queue_25)|+|marking(Queue_1)|+|marking(Queue_144)|+|marking(Queue_39)|+|marking(Queue_72)|+|marking(Queue_105)|+|marking(Queue_113)|+|marking(Queue_137)|+|marking(Queue_128)|+|marking(Queue_175)|+|marking(Queue_99)|+|marking(Queue_191)|+|marking(Queue_151)|+|marking(Queue_70)|+|marking(Queue_180)|+|marking(Queue_47)|+|marking(Queue_127)|+|marking(Queue_21)|+|marking(Queue_83)|+|marking(Queue_9)|+|marking(Queue_118)|+|marking(Queue_125)|+|marking(Queue_32)|+|marking(Queue_123)|+|marking(Queue_28)|+|marking(Queue_67)|+|marking(Queue_35)|+|marking(Queue_90)|+|marking(Queue_117)|+|marking(Queue_177)|+|marking(Queue_84)|+|marking(Queue_34)|+|marking(Queue_196)|+|marking(Queue_155)|+|marking(Queue_96)|+|marking(Queue_27)|+|marking(Queue_2)|+|marking(Queue_116)|+|marking(Queue_159)|+|marking(Queue_76)|+|marking(Queue_11)|+|marking(Queue_55)|+|marking(Queue_46)|+|marking(Queue_15)|+|marking(Queue_41)|+|marking(Queue_87)|+|marking(Queue_82)|+|marking(Queue_176)|+|marking(Queue_186)|+|marking(Queue_77)|+|marking(Queue_122)|+|marking(Queue_102)|+|marking(Queue_174)|+|marking(Queue_60)|+|marking(Queue_85)|+|marking(Queue_124)|)) => A G ((|marking(Memory_7)|+|marking(Memory_196)|+|marking(Memory_171)|+|marking(Memory_56)|+|marking(Memory_87)|+|marking(Memory_107)|+|marking(Memory_178)|+|marking(Memory_174)|+|marking(Memory_103)|+|marking(Memory_156)|+|marking(Memory_12)|+|marking(Memory_124)|+|marking(Memory_119)|+|marking(Memory_157)|+|marking(Memory_166)|+|marking(Memory_52)|+|marking(Memory_112)|+|marking(Memory_165)|+|marking(Memory_136)|+|marking(Memory_191)|+|marking(Memory_59)|+|marking(Memory_53)|+|marking(Memory_85)|+|marking(Memory_18)|+|marking(Memory_13)|+|marking(Memory_10)|+|marking(Memory_97)|+|marking(Memory_42)|+|marking(Memory_9)|+|marking(Memory_6)|+|marking(Memory_199)|+|marking(Memory_193)|+|marking(Memory_150)|+|marking(Memory_163)|+|marking(Memory_40)|+|marking(Memory_90)|+|marking(Memory_66)|+|marking(Memory_99)|+|marking(Memory_4)|+|marking(Memory_54)|+|marking(Memory_111)|+|marking(Memory_162)|+|marking(Memory_141)|+|marking(Memory_39)|+|marking(Memory_95)|+|marking(Memory_45)|+|marking(Memory_20)|+|marking(Memory_43)|+|marking(Memory_44)|+|marking(Memory_36)|+|marking(Memory_75)|+|marking(Memory_76)|+|marking(Memory_145)|+|marking(Memory_144)|+|marking(Memory_137)|+|marking(Memory_24)|+|marking(Memory_114)|+|marking(Memory_94)|+|marking(Memory_38)|+|marking(Memory_17)|+|marking(Memory_147)|+|marking(Memory_96)|+|marking(Memory_33)|+|marking(Memory_62)|+|marking(Memory_84)|+|marking(Memory_3)|+|marking(Memory_106)|+|marking(Memory_46)|+|marking(Memory_109)|+|marking(Memory_126)|+|marking(Memory_155)|+|marking(Memory_14)|+|marking(Memory_22)|+|marking(Memory_58)|+|marking(Memory_34)|+|marking(Memory_86)|+|marking(Memory_132)|+|marking(Memory_102)|+|marking(Memory_133)|+|marking(Memory_183)|+|marking(Memory_69)|+|marking(Memory_71)|+|marking(Memory_181)|+|marking(Memory_120)|+|marking(Memory_122)|+|marking(Memory_192)|+|marking(Memory_47)|+|marking(Memory_149)|+|marking(Memory_168)|+|marking(Memory_161)|+|marking(Memory_116)|+|marking(Memory_138)|+|marking(Memory_167)|+|marking(Memory_148)|+|marking(Memory_51)|+|marking(Memory_164)|+|marking(Memory_73)|+|marking(Memory_26)|+|marking(Memory_118)|+|marking(Memory_170)|+|marking(Memory_21)|+|marking(Memory_110)|+|marking(Memory_100)|+|marking(Memory_121)|+|marking(Memory_5)|+|marking(Memory_200)|+|marking(Memory_25)|+|marking(Memory_189)|+|marking(Memory_28)|+|marking(Memory_15)|+|marking(Memory_172)|+|marking(Memory_180)|+|marking(Memory_80)|+|marking(Memory_113)|+|marking(Memory_31)|+|marking(Memory_91)|+|marking(Memory_184)|+|marking(Memory_198)|+|marking(Memory_104)|+|marking(Memory_197)|+|marking(Memory_70)|+|marking(Memory_182)|+|marking(Memory_158)|+|marking(Memory_74)|+|marking(Memory_27)|+|marking(Memory_139)|+|marking(Memory_68)|+|marking(Memory_169)|+|marking(Memory_98)|+|marking(Memory_194)|+|marking(Memory_175)|+|marking(Memory_153)|+|marking(Memory_135)|+|marking(Memory_79)|+|marking(Memory_77)|+|marking(Memory_16)|+|marking(Memory_154)|+|marking(Memory_179)|+|marking(Memory_37)|+|marking(Memory_82)|+|marking(Memory_143)|+|marking(Memory_92)|+|marking(Memory_65)|+|marking(Memory_173)|+|marking(Memory_130)|+|marking(Memory_63)|+|marking(Memory_29)|+|marking(Memory_142)|+|marking(Memory_152)|+|marking(Memory_185)|+|marking(Memory_55)|+|marking(Memory_81)|+|marking(Memory_140)|+|marking(Memory_115)|+|marking(Memory_93)|+|marking(Memory_2)|+|marking(Memory_48)|+|marking(Memory_30)|+|marking(Memory_159)|+|marking(Memory_187)|+|marking(Memory_108)|+|marking(Memory_50)|+|marking(Memory_89)|+|marking(Memory_64)|+|marking(Memory_146)|+|marking(Memory_117)|+|marking(Memory_11)|+|marking(Memory_57)|+|marking(Memory_72)|+|marking(Memory_131)|+|marking(Memory_176)|+|marking(Memory_105)|+|marking(Memory_125)|+|marking(Memory_32)|+|marking(Memory_83)|+|marking(Memory_41)|+|marking(Memory_19)|+|marking(Memory_188)|+|marking(Memory_127)|+|marking(Memory_35)|+|marking(Memory_61)|+|marking(Memory_134)|+|marking(Memory_101)|+|marking(Memory_60)|+|marking(Memory_190)|+|marking(Memory_8)|+|marking(Memory_129)|+|marking(Memory_186)|+|marking(Memory_88)|+|marking(Memory_78)|+|marking(Memory_67)|+|marking(Memory_1)|+|marking(Memory_123)|+|marking(Memory_23)|+|marking(Memory_151)|+|marking(Memory_160)|+|marking(Memory_177)|+|marking(Memory_128)|+|marking(Memory_195)|+|marking(Memory_49)|)=(|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)))
ctl p_1861_cardinalitycomparison_full_and: A G (((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)<(|marking(Active_199)|+|marking(Active_62)|+|marking(Active_19)|+|marking(Active_146)|+|marking(Active_84)|+|marking(Active_110)|+|marking(Active_158)|+|marking(Active_112)|+|marking(Active_96)|+|marking(Active_176)|+|marking(Active_123)|+|marking(Active_184)|+|marking(Active_7)|+|marking(Active_142)|+|marking(Active_93)|+|marking(Active_59)|+|marking(Active_76)|+|marking(Active_198)|+|marking(Active_116)|+|marking(Active_47)|+|marking(Active_11)|+|marking(Active_154)|+|marking(Active_10)|+|marking(Active_80)|+|marking(Active_185)|+|marking(Active_41)|+|marking(Active_78)|+|marking(Active_121)|+|marking(Active_183)|+|marking(Active_61)|+|marking(Active_94)|+|marking(Active_103)|+|marking(Active_191)|+|marking(Active_107)|+|marking(Active_148)|+|marking(Active_140)|+|marking(Active_53)|+|marking(Active_29)|+|marking(Active_1)|+|marking(Active_79)|+|marking(Active_16)|+|marking(Active_74)|+|marking(Active_115)|+|marking(Active_22)|+|marking(Active_132)|+|marking(Active_126)|+|marking(Active_36)|+|marking(Active_38)|+|marking(Active_90)|+|marking(Active_113)|+|marking(Active_14)|+|marking(Active_46)|+|marking(Active_153)|+|marking(Active_169)|+|marking(Active_188)|+|marking(Active_147)|+|marking(Active_145)|+|marking(Active_179)|+|marking(Active_25)|+|marking(Active_72)|+|marking(Active_125)|+|marking(Active_75)|+|marking(Active_87)|+|marking(Active_175)|+|marking(Active_133)|+|marking(Active_102)|+|marking(Active_71)|+|marking(Active_104)|+|marking(Active_180)|+|marking(Active_97)|+|marking(Active_18)|+|marking(Active_157)|+|marking(Active_88)|+|marking(Active_85)|+|marking(Active_70)|+|marking(Active_149)|+|marking(Active_15)|+|marking(Active_49)|+|marking(Active_89)|+|marking(Active_50)|+|marking(Active_129)|+|marking(Active_17)|+|marking(Active_40)|+|marking(Active_114)|+|marking(Active_57)|+|marking(Active_69)|+|marking(Active_77)|+|marking(Active_178)|+|marking(Active_58)|+|marking(Active_144)|+|marking(Active_182)|+|marking(Active_119)|+|marking(Active_9)|+|marking(Active_105)|+|marking(Active_44)|+|marking(Active_23)|+|marking(Active_111)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_189)|+|marking(Active_197)|+|marking(Active_174)|+|marking(Active_82)|+|marking(Active_124)|+|marking(Active_195)|+|marking(Active_137)|+|marking(Active_55)|+|marking(Active_99)|+|marking(Active_4)|+|marking(Active_48)|+|marking(Active_12)|+|marking(Active_171)|+|marking(Active_151)|+|marking(Active_181)|+|marking(Active_81)|+|marking(Active_51)|+|marking(Active_3)|+|marking(Active_150)|+|marking(Active_162)|+|marking(Active_128)|+|marking(Active_30)|+|marking(Active_108)|+|marking(Active_136)|+|marking(Active_106)|+|marking(Active_91)|+|marking(Active_167)|+|marking(Active_120)|+|marking(Active_177)|+|marking(Active_152)|+|marking(Active_43)|+|marking(Active_117)|+|marking(Active_54)|+|marking(Active_139)|+|marking(Active_42)|+|marking(Active_21)|+|marking(Active_63)|+|marking(Active_138)|+|marking(Active_52)|+|marking(Active_27)|+|marking(Active_73)|+|marking(Active_156)|+|marking(Active_194)|+|marking(Active_98)|+|marking(Active_56)|+|marking(Active_109)|+|marking(Active_39)|+|marking(Active_67)|+|marking(Active_32)|+|marking(Active_173)|+|marking(Active_130)|+|marking(Active_159)|+|marking(Active_13)|+|marking(Active_35)|+|marking(Active_192)|+|marking(Active_100)|+|marking(Active_161)|+|marking(Active_37)|+|marking(Active_31)|+|marking(Active_65)|+|marking(Active_155)|+|marking(Active_168)|+|marking(Active_95)|+|marking(Active_131)|+|marking(Active_165)|+|marking(Active_24)|+|marking(Active_60)|+|marking(Active_8)|+|marking(Active_20)|+|marking(Active_160)|+|marking(Active_143)|+|marking(Active_26)|+|marking(Active_163)|+|marking(Active_200)|+|marking(Active_186)|+|marking(Active_172)|+|marking(Active_135)|+|marking(Active_68)|+|marking(Active_83)|+|marking(Active_86)|+|marking(Active_166)|+|marking(Active_193)|+|marking(Active_164)|+|marking(Active_196)|+|marking(Active_66)|+|marking(Active_64)|+|marking(Active_28)|+|marking(Active_122)|+|marking(Active_101)|+|marking(Active_5)|+|marking(Active_33)|+|marking(Active_141)|+|marking(Active_6)|+|marking(Active_190)|+|marking(Active_134)|+|marking(Active_170)|+|marking(Active_45)|+|marking(Active_118)|+|marking(Active_187)|+|marking(Active_92)|+|marking(Active_127)|)) & ((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)>(|marking(Memory_7)|+|marking(Memory_196)|+|marking(Memory_171)|+|marking(Memory_56)|+|marking(Memory_87)|+|marking(Memory_107)|+|marking(Memory_178)|+|marking(Memory_174)|+|marking(Memory_103)|+|marking(Memory_156)|+|marking(Memory_12)|+|marking(Memory_124)|+|marking(Memory_119)|+|marking(Memory_157)|+|marking(Memory_166)|+|marking(Memory_52)|+|marking(Memory_112)|+|marking(Memory_165)|+|marking(Memory_136)|+|marking(Memory_191)|+|marking(Memory_59)|+|marking(Memory_53)|+|marking(Memory_85)|+|marking(Memory_18)|+|marking(Memory_13)|+|marking(Memory_10)|+|marking(Memory_97)|+|marking(Memory_42)|+|marking(Memory_9)|+|marking(Memory_6)|+|marking(Memory_199)|+|marking(Memory_193)|+|marking(Memory_150)|+|marking(Memory_163)|+|marking(Memory_40)|+|marking(Memory_90)|+|marking(Memory_66)|+|marking(Memory_99)|+|marking(Memory_4)|+|marking(Memory_54)|+|marking(Memory_111)|+|marking(Memory_162)|+|marking(Memory_141)|+|marking(Memory_39)|+|marking(Memory_95)|+|marking(Memory_45)|+|marking(Memory_20)|+|marking(Memory_43)|+|marking(Memory_44)|+|marking(Memory_36)|+|marking(Memory_75)|+|marking(Memory_76)|+|marking(Memory_145)|+|marking(Memory_144)|+|marking(Memory_137)|+|marking(Memory_24)|+|marking(Memory_114)|+|marking(Memory_94)|+|marking(Memory_38)|+|marking(Memory_17)|+|marking(Memory_147)|+|marking(Memory_96)|+|marking(Memory_33)|+|marking(Memory_62)|+|marking(Memory_84)|+|marking(Memory_3)|+|marking(Memory_106)|+|marking(Memory_46)|+|marking(Memory_109)|+|marking(Memory_126)|+|marking(Memory_155)|+|marking(Memory_14)|+|marking(Memory_22)|+|marking(Memory_58)|+|marking(Memory_34)|+|marking(Memory_86)|+|marking(Memory_132)|+|marking(Memory_102)|+|marking(Memory_133)|+|marking(Memory_183)|+|marking(Memory_69)|+|marking(Memory_71)|+|marking(Memory_181)|+|marking(Memory_120)|+|marking(Memory_122)|+|marking(Memory_192)|+|marking(Memory_47)|+|marking(Memory_149)|+|marking(Memory_168)|+|marking(Memory_161)|+|marking(Memory_116)|+|marking(Memory_138)|+|marking(Memory_167)|+|marking(Memory_148)|+|marking(Memory_51)|+|marking(Memory_164)|+|marking(Memory_73)|+|marking(Memory_26)|+|marking(Memory_118)|+|marking(Memory_170)|+|marking(Memory_21)|+|marking(Memory_110)|+|marking(Memory_100)|+|marking(Memory_121)|+|marking(Memory_5)|+|marking(Memory_200)|+|marking(Memory_25)|+|marking(Memory_189)|+|marking(Memory_28)|+|marking(Memory_15)|+|marking(Memory_172)|+|marking(Memory_180)|+|marking(Memory_80)|+|marking(Memory_113)|+|marking(Memory_31)|+|marking(Memory_91)|+|marking(Memory_184)|+|marking(Memory_198)|+|marking(Memory_104)|+|marking(Memory_197)|+|marking(Memory_70)|+|marking(Memory_182)|+|marking(Memory_158)|+|marking(Memory_74)|+|marking(Memory_27)|+|marking(Memory_139)|+|marking(Memory_68)|+|marking(Memory_169)|+|marking(Memory_98)|+|marking(Memory_194)|+|marking(Memory_175)|+|marking(Memory_153)|+|marking(Memory_135)|+|marking(Memory_79)|+|marking(Memory_77)|+|marking(Memory_16)|+|marking(Memory_154)|+|marking(Memory_179)|+|marking(Memory_37)|+|marking(Memory_82)|+|marking(Memory_143)|+|marking(Memory_92)|+|marking(Memory_65)|+|marking(Memory_173)|+|marking(Memory_130)|+|marking(Memory_63)|+|marking(Memory_29)|+|marking(Memory_142)|+|marking(Memory_152)|+|marking(Memory_185)|+|marking(Memory_55)|+|marking(Memory_81)|+|marking(Memory_140)|+|marking(Memory_115)|+|marking(Memory_93)|+|marking(Memory_2)|+|marking(Memory_48)|+|marking(Memory_30)|+|marking(Memory_159)|+|marking(Memory_187)|+|marking(Memory_108)|+|marking(Memory_50)|+|marking(Memory_89)|+|marking(Memory_64)|+|marking(Memory_146)|+|marking(Memory_117)|+|marking(Memory_11)|+|marking(Memory_57)|+|marking(Memory_72)|+|marking(Memory_131)|+|marking(Memory_176)|+|marking(Memory_105)|+|marking(Memory_125)|+|marking(Memory_32)|+|marking(Memory_83)|+|marking(Memory_41)|+|marking(Memory_19)|+|marking(Memory_188)|+|marking(Memory_127)|+|marking(Memory_35)|+|marking(Memory_61)|+|marking(Memory_134)|+|marking(Memory_101)|+|marking(Memory_60)|+|marking(Memory_190)|+|marking(Memory_8)|+|marking(Memory_129)|+|marking(Memory_186)|+|marking(Memory_88)|+|marking(Memory_78)|+|marking(Memory_67)|+|marking(Memory_1)|+|marking(Memory_123)|+|marking(Memory_23)|+|marking(Memory_151)|+|marking(Memory_160)|+|marking(Memory_177)|+|marking(Memory_128)|+|marking(Memory_195)|+|marking(Memory_49)|)))
ctl p_1862_cardinalitycomparison_full_or: E F (((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)<(|marking(Active_199)|+|marking(Active_62)|+|marking(Active_19)|+|marking(Active_146)|+|marking(Active_84)|+|marking(Active_110)|+|marking(Active_158)|+|marking(Active_112)|+|marking(Active_96)|+|marking(Active_176)|+|marking(Active_123)|+|marking(Active_184)|+|marking(Active_7)|+|marking(Active_142)|+|marking(Active_93)|+|marking(Active_59)|+|marking(Active_76)|+|marking(Active_198)|+|marking(Active_116)|+|marking(Active_47)|+|marking(Active_11)|+|marking(Active_154)|+|marking(Active_10)|+|marking(Active_80)|+|marking(Active_185)|+|marking(Active_41)|+|marking(Active_78)|+|marking(Active_121)|+|marking(Active_183)|+|marking(Active_61)|+|marking(Active_94)|+|marking(Active_103)|+|marking(Active_191)|+|marking(Active_107)|+|marking(Active_148)|+|marking(Active_140)|+|marking(Active_53)|+|marking(Active_29)|+|marking(Active_1)|+|marking(Active_79)|+|marking(Active_16)|+|marking(Active_74)|+|marking(Active_115)|+|marking(Active_22)|+|marking(Active_132)|+|marking(Active_126)|+|marking(Active_36)|+|marking(Active_38)|+|marking(Active_90)|+|marking(Active_113)|+|marking(Active_14)|+|marking(Active_46)|+|marking(Active_153)|+|marking(Active_169)|+|marking(Active_188)|+|marking(Active_147)|+|marking(Active_145)|+|marking(Active_179)|+|marking(Active_25)|+|marking(Active_72)|+|marking(Active_125)|+|marking(Active_75)|+|marking(Active_87)|+|marking(Active_175)|+|marking(Active_133)|+|marking(Active_102)|+|marking(Active_71)|+|marking(Active_104)|+|marking(Active_180)|+|marking(Active_97)|+|marking(Active_18)|+|marking(Active_157)|+|marking(Active_88)|+|marking(Active_85)|+|marking(Active_70)|+|marking(Active_149)|+|marking(Active_15)|+|marking(Active_49)|+|marking(Active_89)|+|marking(Active_50)|+|marking(Active_129)|+|marking(Active_17)|+|marking(Active_40)|+|marking(Active_114)|+|marking(Active_57)|+|marking(Active_69)|+|marking(Active_77)|+|marking(Active_178)|+|marking(Active_58)|+|marking(Active_144)|+|marking(Active_182)|+|marking(Active_119)|+|marking(Active_9)|+|marking(Active_105)|+|marking(Active_44)|+|marking(Active_23)|+|marking(Active_111)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_189)|+|marking(Active_197)|+|marking(Active_174)|+|marking(Active_82)|+|marking(Active_124)|+|marking(Active_195)|+|marking(Active_137)|+|marking(Active_55)|+|marking(Active_99)|+|marking(Active_4)|+|marking(Active_48)|+|marking(Active_12)|+|marking(Active_171)|+|marking(Active_151)|+|marking(Active_181)|+|marking(Active_81)|+|marking(Active_51)|+|marking(Active_3)|+|marking(Active_150)|+|marking(Active_162)|+|marking(Active_128)|+|marking(Active_30)|+|marking(Active_108)|+|marking(Active_136)|+|marking(Active_106)|+|marking(Active_91)|+|marking(Active_167)|+|marking(Active_120)|+|marking(Active_177)|+|marking(Active_152)|+|marking(Active_43)|+|marking(Active_117)|+|marking(Active_54)|+|marking(Active_139)|+|marking(Active_42)|+|marking(Active_21)|+|marking(Active_63)|+|marking(Active_138)|+|marking(Active_52)|+|marking(Active_27)|+|marking(Active_73)|+|marking(Active_156)|+|marking(Active_194)|+|marking(Active_98)|+|marking(Active_56)|+|marking(Active_109)|+|marking(Active_39)|+|marking(Active_67)|+|marking(Active_32)|+|marking(Active_173)|+|marking(Active_130)|+|marking(Active_159)|+|marking(Active_13)|+|marking(Active_35)|+|marking(Active_192)|+|marking(Active_100)|+|marking(Active_161)|+|marking(Active_37)|+|marking(Active_31)|+|marking(Active_65)|+|marking(Active_155)|+|marking(Active_168)|+|marking(Active_95)|+|marking(Active_131)|+|marking(Active_165)|+|marking(Active_24)|+|marking(Active_60)|+|marking(Active_8)|+|marking(Active_20)|+|marking(Active_160)|+|marking(Active_143)|+|marking(Active_26)|+|marking(Active_163)|+|marking(Active_200)|+|marking(Active_186)|+|marking(Active_172)|+|marking(Active_135)|+|marking(Active_68)|+|marking(Active_83)|+|marking(Active_86)|+|marking(Active_166)|+|marking(Active_193)|+|marking(Active_164)|+|marking(Active_196)|+|marking(Active_66)|+|marking(Active_64)|+|marking(Active_28)|+|marking(Active_122)|+|marking(Active_101)|+|marking(Active_5)|+|marking(Active_33)|+|marking(Active_141)|+|marking(Active_6)|+|marking(Active_190)|+|marking(Active_134)|+|marking(Active_170)|+|marking(Active_45)|+|marking(Active_118)|+|marking(Active_187)|+|marking(Active_92)|+|marking(Active_127)|)) | ((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)>(|marking(Memory_7)|+|marking(Memory_196)|+|marking(Memory_171)|+|marking(Memory_56)|+|marking(Memory_87)|+|marking(Memory_107)|+|marking(Memory_178)|+|marking(Memory_174)|+|marking(Memory_103)|+|marking(Memory_156)|+|marking(Memory_12)|+|marking(Memory_124)|+|marking(Memory_119)|+|marking(Memory_157)|+|marking(Memory_166)|+|marking(Memory_52)|+|marking(Memory_112)|+|marking(Memory_165)|+|marking(Memory_136)|+|marking(Memory_191)|+|marking(Memory_59)|+|marking(Memory_53)|+|marking(Memory_85)|+|marking(Memory_18)|+|marking(Memory_13)|+|marking(Memory_10)|+|marking(Memory_97)|+|marking(Memory_42)|+|marking(Memory_9)|+|marking(Memory_6)|+|marking(Memory_199)|+|marking(Memory_193)|+|marking(Memory_150)|+|marking(Memory_163)|+|marking(Memory_40)|+|marking(Memory_90)|+|marking(Memory_66)|+|marking(Memory_99)|+|marking(Memory_4)|+|marking(Memory_54)|+|marking(Memory_111)|+|marking(Memory_162)|+|marking(Memory_141)|+|marking(Memory_39)|+|marking(Memory_95)|+|marking(Memory_45)|+|marking(Memory_20)|+|marking(Memory_43)|+|marking(Memory_44)|+|marking(Memory_36)|+|marking(Memory_75)|+|marking(Memory_76)|+|marking(Memory_145)|+|marking(Memory_144)|+|marking(Memory_137)|+|marking(Memory_24)|+|marking(Memory_114)|+|marking(Memory_94)|+|marking(Memory_38)|+|marking(Memory_17)|+|marking(Memory_147)|+|marking(Memory_96)|+|marking(Memory_33)|+|marking(Memory_62)|+|marking(Memory_84)|+|marking(Memory_3)|+|marking(Memory_106)|+|marking(Memory_46)|+|marking(Memory_109)|+|marking(Memory_126)|+|marking(Memory_155)|+|marking(Memory_14)|+|marking(Memory_22)|+|marking(Memory_58)|+|marking(Memory_34)|+|marking(Memory_86)|+|marking(Memory_132)|+|marking(Memory_102)|+|marking(Memory_133)|+|marking(Memory_183)|+|marking(Memory_69)|+|marking(Memory_71)|+|marking(Memory_181)|+|marking(Memory_120)|+|marking(Memory_122)|+|marking(Memory_192)|+|marking(Memory_47)|+|marking(Memory_149)|+|marking(Memory_168)|+|marking(Memory_161)|+|marking(Memory_116)|+|marking(Memory_138)|+|marking(Memory_167)|+|marking(Memory_148)|+|marking(Memory_51)|+|marking(Memory_164)|+|marking(Memory_73)|+|marking(Memory_26)|+|marking(Memory_118)|+|marking(Memory_170)|+|marking(Memory_21)|+|marking(Memory_110)|+|marking(Memory_100)|+|marking(Memory_121)|+|marking(Memory_5)|+|marking(Memory_200)|+|marking(Memory_25)|+|marking(Memory_189)|+|marking(Memory_28)|+|marking(Memory_15)|+|marking(Memory_172)|+|marking(Memory_180)|+|marking(Memory_80)|+|marking(Memory_113)|+|marking(Memory_31)|+|marking(Memory_91)|+|marking(Memory_184)|+|marking(Memory_198)|+|marking(Memory_104)|+|marking(Memory_197)|+|marking(Memory_70)|+|marking(Memory_182)|+|marking(Memory_158)|+|marking(Memory_74)|+|marking(Memory_27)|+|marking(Memory_139)|+|marking(Memory_68)|+|marking(Memory_169)|+|marking(Memory_98)|+|marking(Memory_194)|+|marking(Memory_175)|+|marking(Memory_153)|+|marking(Memory_135)|+|marking(Memory_79)|+|marking(Memory_77)|+|marking(Memory_16)|+|marking(Memory_154)|+|marking(Memory_179)|+|marking(Memory_37)|+|marking(Memory_82)|+|marking(Memory_143)|+|marking(Memory_92)|+|marking(Memory_65)|+|marking(Memory_173)|+|marking(Memory_130)|+|marking(Memory_63)|+|marking(Memory_29)|+|marking(Memory_142)|+|marking(Memory_152)|+|marking(Memory_185)|+|marking(Memory_55)|+|marking(Memory_81)|+|marking(Memory_140)|+|marking(Memory_115)|+|marking(Memory_93)|+|marking(Memory_2)|+|marking(Memory_48)|+|marking(Memory_30)|+|marking(Memory_159)|+|marking(Memory_187)|+|marking(Memory_108)|+|marking(Memory_50)|+|marking(Memory_89)|+|marking(Memory_64)|+|marking(Memory_146)|+|marking(Memory_117)|+|marking(Memory_11)|+|marking(Memory_57)|+|marking(Memory_72)|+|marking(Memory_131)|+|marking(Memory_176)|+|marking(Memory_105)|+|marking(Memory_125)|+|marking(Memory_32)|+|marking(Memory_83)|+|marking(Memory_41)|+|marking(Memory_19)|+|marking(Memory_188)|+|marking(Memory_127)|+|marking(Memory_35)|+|marking(Memory_61)|+|marking(Memory_134)|+|marking(Memory_101)|+|marking(Memory_60)|+|marking(Memory_190)|+|marking(Memory_8)|+|marking(Memory_129)|+|marking(Memory_186)|+|marking(Memory_88)|+|marking(Memory_78)|+|marking(Memory_67)|+|marking(Memory_1)|+|marking(Memory_123)|+|marking(Memory_23)|+|marking(Memory_151)|+|marking(Memory_160)|+|marking(Memory_177)|+|marking(Memory_128)|+|marking(Memory_195)|+|marking(Memory_49)|)))
ctl p_1863_cardinalitycomparison_full_and_notx: A G (((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)<(|marking(Active_199)|+|marking(Active_62)|+|marking(Active_19)|+|marking(Active_146)|+|marking(Active_84)|+|marking(Active_110)|+|marking(Active_158)|+|marking(Active_112)|+|marking(Active_96)|+|marking(Active_176)|+|marking(Active_123)|+|marking(Active_184)|+|marking(Active_7)|+|marking(Active_142)|+|marking(Active_93)|+|marking(Active_59)|+|marking(Active_76)|+|marking(Active_198)|+|marking(Active_116)|+|marking(Active_47)|+|marking(Active_11)|+|marking(Active_154)|+|marking(Active_10)|+|marking(Active_80)|+|marking(Active_185)|+|marking(Active_41)|+|marking(Active_78)|+|marking(Active_121)|+|marking(Active_183)|+|marking(Active_61)|+|marking(Active_94)|+|marking(Active_103)|+|marking(Active_191)|+|marking(Active_107)|+|marking(Active_148)|+|marking(Active_140)|+|marking(Active_53)|+|marking(Active_29)|+|marking(Active_1)|+|marking(Active_79)|+|marking(Active_16)|+|marking(Active_74)|+|marking(Active_115)|+|marking(Active_22)|+|marking(Active_132)|+|marking(Active_126)|+|marking(Active_36)|+|marking(Active_38)|+|marking(Active_90)|+|marking(Active_113)|+|marking(Active_14)|+|marking(Active_46)|+|marking(Active_153)|+|marking(Active_169)|+|marking(Active_188)|+|marking(Active_147)|+|marking(Active_145)|+|marking(Active_179)|+|marking(Active_25)|+|marking(Active_72)|+|marking(Active_125)|+|marking(Active_75)|+|marking(Active_87)|+|marking(Active_175)|+|marking(Active_133)|+|marking(Active_102)|+|marking(Active_71)|+|marking(Active_104)|+|marking(Active_180)|+|marking(Active_97)|+|marking(Active_18)|+|marking(Active_157)|+|marking(Active_88)|+|marking(Active_85)|+|marking(Active_70)|+|marking(Active_149)|+|marking(Active_15)|+|marking(Active_49)|+|marking(Active_89)|+|marking(Active_50)|+|marking(Active_129)|+|marking(Active_17)|+|marking(Active_40)|+|marking(Active_114)|+|marking(Active_57)|+|marking(Active_69)|+|marking(Active_77)|+|marking(Active_178)|+|marking(Active_58)|+|marking(Active_144)|+|marking(Active_182)|+|marking(Active_119)|+|marking(Active_9)|+|marking(Active_105)|+|marking(Active_44)|+|marking(Active_23)|+|marking(Active_111)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_189)|+|marking(Active_197)|+|marking(Active_174)|+|marking(Active_82)|+|marking(Active_124)|+|marking(Active_195)|+|marking(Active_137)|+|marking(Active_55)|+|marking(Active_99)|+|marking(Active_4)|+|marking(Active_48)|+|marking(Active_12)|+|marking(Active_171)|+|marking(Active_151)|+|marking(Active_181)|+|marking(Active_81)|+|marking(Active_51)|+|marking(Active_3)|+|marking(Active_150)|+|marking(Active_162)|+|marking(Active_128)|+|marking(Active_30)|+|marking(Active_108)|+|marking(Active_136)|+|marking(Active_106)|+|marking(Active_91)|+|marking(Active_167)|+|marking(Active_120)|+|marking(Active_177)|+|marking(Active_152)|+|marking(Active_43)|+|marking(Active_117)|+|marking(Active_54)|+|marking(Active_139)|+|marking(Active_42)|+|marking(Active_21)|+|marking(Active_63)|+|marking(Active_138)|+|marking(Active_52)|+|marking(Active_27)|+|marking(Active_73)|+|marking(Active_156)|+|marking(Active_194)|+|marking(Active_98)|+|marking(Active_56)|+|marking(Active_109)|+|marking(Active_39)|+|marking(Active_67)|+|marking(Active_32)|+|marking(Active_173)|+|marking(Active_130)|+|marking(Active_159)|+|marking(Active_13)|+|marking(Active_35)|+|marking(Active_192)|+|marking(Active_100)|+|marking(Active_161)|+|marking(Active_37)|+|marking(Active_31)|+|marking(Active_65)|+|marking(Active_155)|+|marking(Active_168)|+|marking(Active_95)|+|marking(Active_131)|+|marking(Active_165)|+|marking(Active_24)|+|marking(Active_60)|+|marking(Active_8)|+|marking(Active_20)|+|marking(Active_160)|+|marking(Active_143)|+|marking(Active_26)|+|marking(Active_163)|+|marking(Active_200)|+|marking(Active_186)|+|marking(Active_172)|+|marking(Active_135)|+|marking(Active_68)|+|marking(Active_83)|+|marking(Active_86)|+|marking(Active_166)|+|marking(Active_193)|+|marking(Active_164)|+|marking(Active_196)|+|marking(Active_66)|+|marking(Active_64)|+|marking(Active_28)|+|marking(Active_122)|+|marking(Active_101)|+|marking(Active_5)|+|marking(Active_33)|+|marking(Active_141)|+|marking(Active_6)|+|marking(Active_190)|+|marking(Active_134)|+|marking(Active_170)|+|marking(Active_45)|+|marking(Active_118)|+|marking(Active_187)|+|marking(Active_92)|+|marking(Active_127)|)) & !((|marking(OwnMemAcc_172)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_133)|+|marking(OwnMemAcc_167)|+|marking(OwnMemAcc_170)|+|marking(OwnMemAcc_165)|+|marking(OwnMemAcc_118)|+|marking(OwnMemAcc_186)|+|marking(OwnMemAcc_192)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_114)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_175)|+|marking(OwnMemAcc_164)|+|marking(OwnMemAcc_196)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_188)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_197)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_185)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_158)|+|marking(OwnMemAcc_181)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_200)|+|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_140)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_145)|+|marking(OwnMemAcc_120)|+|marking(OwnMemAcc_160)|+|marking(OwnMemAcc_173)|+|marking(OwnMemAcc_163)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_142)|+|marking(OwnMemAcc_169)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_123)|+|marking(OwnMemAcc_141)|+|marking(OwnMemAcc_113)|+|marking(OwnMemAcc_102)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_179)|+|marking(OwnMemAcc_117)|+|marking(OwnMemAcc_153)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_125)|+|marking(OwnMemAcc_138)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_171)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_126)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_195)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_161)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_122)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_147)|+|marking(OwnMemAcc_151)|+|marking(OwnMemAcc_194)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_177)|+|marking(OwnMemAcc_191)|+|marking(OwnMemAcc_180)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_132)|+|marking(OwnMemAcc_121)|+|marking(OwnMemAcc_159)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_131)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_157)|+|marking(OwnMemAcc_107)|+|marking(OwnMemAcc_127)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_184)|+|marking(OwnMemAcc_156)|+|marking(OwnMemAcc_116)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_182)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_108)|+|marking(OwnMemAcc_101)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_176)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_112)|+|marking(OwnMemAcc_128)|+|marking(OwnMemAcc_144)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_199)|+|marking(OwnMemAcc_150)|+|marking(OwnMemAcc_136)|+|marking(OwnMemAcc_143)|+|marking(OwnMemAcc_187)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_189)|+|marking(OwnMemAcc_111)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_168)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_148)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_149)|+|marking(OwnMemAcc_190)|+|marking(OwnMemAcc_178)|+|marking(OwnMemAcc_135)|+|marking(OwnMemAcc_110)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_124)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_103)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_129)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_154)|+|marking(OwnMemAcc_162)|+|marking(OwnMemAcc_198)|+|marking(OwnMemAcc_174)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_152)|+|marking(OwnMemAcc_193)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_115)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_130)|+|marking(OwnMemAcc_5)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_105)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_155)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_119)|+|marking(OwnMemAcc_106)|+|marking(OwnMemAcc_104)|+|marking(OwnMemAcc_137)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_183)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_134)|+|marking(OwnMemAcc_146)|+|marking(OwnMemAcc_139)|+|marking(OwnMemAcc_166)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_109)|+|marking(OwnMemAcc_98)|)>(|marking(Memory_7)|+|marking(Memory_196)|+|marking(Memory_171)|+|marking(Memory_56)|+|marking(Memory_87)|+|marking(Memory_107)|+|marking(Memory_178)|+|marking(Memory_174)|+|marking(Memory_103)|+|marking(Memory_156)|+|marking(Memory_12)|+|marking(Memory_124)|+|marking(Memory_119)|+|marking(Memory_157)|+|marking(Memory_166)|+|marking(Memory_52)|+|marking(Memory_112)|+|marking(Memory_165)|+|marking(Memory_136)|+|marking(Memory_191)|+|marking(Memory_59)|+|marking(Memory_53)|+|marking(Memory_85)|+|marking(Memory_18)|+|marking(Memory_13)|+|marking(Memory_10)|+|marking(Memory_97)|+|marking(Memory_42)|+|marking(Memory_9)|+|marking(Memory_6)|+|marking(Memory_199)|+|marking(Memory_193)|+|marking(Memory_150)|+|marking(Memory_163)|+|marking(Memory_40)|+|marking(Memory_90)|+|marking(Memory_66)|+|marking(Memory_99)|+|marking(Memory_4)|+|marking(Memory_54)|+|marking(Memory_111)|+|marking(Memory_162)|+|marking(Memory_141)|+|marking(Memory_39)|+|marking(Memory_95)|+|marking(Memory_45)|+|marking(Memory_20)|+|marking(Memory_43)|+|marking(Memory_44)|+|marking(Memory_36)|+|marking(Memory_75)|+|marking(Memory_76)|+|marking(Memory_145)|+|marking(Memory_144)|+|marking(Memory_137)|+|marking(Memory_24)|+|marking(Memory_114)|+|marking(Memory_94)|+|marking(Memory_38)|+|marking(Memory_17)|+|marking(Memory_147)|+|marking(Memory_96)|+|marking(Memory_33)|+|marking(Memory_62)|+|marking(Memory_84)|+|marking(Memory_3)|+|marking(Memory_106)|+|marking(Memory_46)|+|marking(Memory_109)|+|marking(Memory_126)|+|marking(Memory_155)|+|marking(Memory_14)|+|marking(Memory_22)|+|marking(Memory_58)|+|marking(Memory_34)|+|marking(Memory_86)|+|marking(Memory_132)|+|marking(Memory_102)|+|marking(Memory_133)|+|marking(Memory_183)|+|marking(Memory_69)|+|marking(Memory_71)|+|marking(Memory_181)|+|marking(Memory_120)|+|marking(Memory_122)|+|marking(Memory_192)|+|marking(Memory_47)|+|marking(Memory_149)|+|marking(Memory_168)|+|marking(Memory_161)|+|marking(Memory_116)|+|marking(Memory_138)|+|marking(Memory_167)|+|marking(Memory_148)|+|marking(Memory_51)|+|marking(Memory_164)|+|marking(Memory_73)|+|marking(Memory_26)|+|marking(Memory_118)|+|marking(Memory_170)|+|marking(Memory_21)|+|marking(Memory_110)|+|marking(Memory_100)|+|marking(Memory_121)|+|marking(Memory_5)|+|marking(Memory_200)|+|marking(Memory_25)|+|marking(Memory_189)|+|marking(Memory_28)|+|marking(Memory_15)|+|marking(Memory_172)|+|marking(Memory_180)|+|marking(Memory_80)|+|marking(Memory_113)|+|marking(Memory_31)|+|marking(Memory_91)|+|marking(Memory_184)|+|marking(Memory_198)|+|marking(Memory_104)|+|marking(Memory_197)|+|marking(Memory_70)|+|marking(Memory_182)|+|marking(Memory_158)|+|marking(Memory_74)|+|marking(Memory_27)|+|marking(Memory_139)|+|marking(Memory_68)|+|marking(Memory_169)|+|marking(Memory_98)|+|marking(Memory_194)|+|marking(Memory_175)|+|marking(Memory_153)|+|marking(Memory_135)|+|marking(Memory_79)|+|marking(Memory_77)|+|marking(Memory_16)|+|marking(Memory_154)|+|marking(Memory_179)|+|marking(Memory_37)|+|marking(Memory_82)|+|marking(Memory_143)|+|marking(Memory_92)|+|marking(Memory_65)|+|marking(Memory_173)|+|marking(Memory_130)|+|marking(Memory_63)|+|marking(Memory_29)|+|marking(Memory_142)|+|marking(Memory_152)|+|marking(Memory_185)|+|marking(Memory_55)|+|marking(Memory_81)|+|marking(Memory_140)|+|marking(Memory_115)|+|marking(Memory_93)|+|marking(Memory_2)|+|marking(Memory_48)|+|marking(Memory_30)|+|marking(Memory_159)|+|marking(Memory_187)|+|marking(Memory_108)|+|marking(Memory_50)|+|marking(Memory_89)|+|marking(Memory_64)|+|marking(Memory_146)|+|marking(Memory_117)|+|marking(Memory_11)|+|marking(Memory_57)|+|marking(Memory_72)|+|marking(Memory_131)|+|marking(Memory_176)|+|marking(Memory_105)|+|marking(Memory_125)|+|marking(Memory_32)|+|marking(Memory_83)|+|marking(Memory_41)|+|marking(Memory_19)|+|marking(Memory_188)|+|marking(Memory_127)|+|marking(Memory_35)|+|marking(Memory_61)|+|marking(Memory_134)|+|marking(Memory_101)|+|marking(Memory_60)|+|marking(Memory_190)|+|marking(Memory_8)|+|marking(Memory_129)|+|marking(Memory_186)|+|marking(Memory_88)|+|marking(Memory_78)|+|marking(Memory_67)|+|marking(Memory_1)|+|marking(Memory_123)|+|marking(Memory_23)|+|marking(Memory_151)|+|marking(Memory_160)|+|marking(Memory_177)|+|marking(Memory_128)|+|marking(Memory_195)|+|marking(Memory_49)|)))


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