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-000050
export BK_EXAMINATION=CTLMarkingComparison
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-000050
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is SharedMemory-PT-000050, examination is CTLMarkingComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

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

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

execution on node 2: quadhexa-2.u-paris10.fr (runId=136983895500218_n_2)
=====================================================================
runnning marcie on SharedMemory-PT-000050 (CTLMarkingComparison)
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-000050, examination is CTLMarkingComparison
=====================================================================

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

START 1369868399

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 2651 NrTr: 5050)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369868401

--------------------
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_1870_markingcomparison_eq_x: E F (X (true & (1=|marking(Memory_22)|) & (|marking(Memory_23)|=0) & (|marking(Memory_50)|=0) & (|marking(Memory_6)|=0) & (|marking(Memory_12)|=0) & (|marking(Memory_11)|=0) & (|marking(Memory_49)|=0) & (|marking(Memory_36)|=0) & (|marking(Memory_15)|=0) & (|marking(Memory_7)|=0) & (|marking(Memory_21)|=0) & (|marking(Memory_42)|=0) & (|marking(Memory_37)|=0) & (|marking(Memory_27)|=0) & (|marking(Memory_13)|=0) & (|marking(Memory_46)|=0) & (|marking(Memory_5)|=0) & (|marking(Memory_33)|=0) & (|marking(Memory_41)|=0) & (|marking(Memory_35)|=0) & (|marking(Memory_44)|=0) & (|marking(Memory_47)|=0) & (|marking(Memory_3)|=0) & (|marking(Memory_17)|=0) & (|marking(Memory_2)|=0) & (|marking(Memory_9)|=0) & (|marking(Memory_31)|=0) & (|marking(Memory_32)|=0) & (|marking(Memory_43)|=0) & (|marking(Memory_4)|=0) & (|marking(Memory_24)|=0) & (|marking(Memory_8)|=0) & (|marking(Memory_29)|=0) & (|marking(Memory_40)|=0) & (|marking(Memory_28)|=0) & (|marking(Memory_26)|=0) & (|marking(Memory_39)|=0) & (|marking(Memory_1)|=0) & (|marking(Memory_20)|=0) & (|marking(Memory_18)|=0) & (|marking(Memory_16)|=0) & (|marking(Memory_25)|=0) & (|marking(Memory_48)|=0) & (|marking(Memory_14)|=0) & (|marking(Memory_30)|=0) & (|marking(Memory_45)|=0) & (|marking(Memory_34)|=0) & (|marking(Memory_38)|=0) & (|marking(Memory_10)|=0) & (|marking(Memory_19)|=0)) => E G (true & (1=|marking(Ext_Mem_Acc_9_14)|) & (|marking(Ext_Mem_Acc_4_44)|=0) & (|marking(Ext_Mem_Acc_29_7)|=0) & (|marking(Ext_Mem_Acc_44_1)|=0) & (|marking(Ext_Mem_Acc_13_5)|=0) & (|marking(Ext_Mem_Acc_21_5)|=0) & (|marking(Ext_Mem_Acc_12_9)|=0) & (|marking(Ext_Mem_Acc_27_26)|=0) & (|marking(Ext_Mem_Acc_3_42)|=0) & (|marking(Ext_Mem_Acc_10_21)|=0) & (|marking(Ext_Mem_Acc_10_27)|=0) & (|marking(Ext_Mem_Acc_27_43)|=0) & (|marking(Ext_Mem_Acc_47_19)|=0) & (|marking(Ext_Mem_Acc_22_6)|=0) & (|marking(Ext_Mem_Acc_24_41)|=0) & (|marking(Ext_Mem_Acc_19_41)|=0) & (|marking(Ext_Mem_Acc_45_37)|=0) & (|marking(Ext_Mem_Acc_1_6)|=0) & (|marking(Ext_Mem_Acc_17_5)|=0) & (|marking(Ext_Mem_Acc_37_1)|=0) & (|marking(Ext_Mem_Acc_14_11)|=0) & (|marking(Ext_Mem_Acc_17_41)|=0) & (|marking(Ext_Mem_Acc_9_1)|=0) & (|marking(Ext_Mem_Acc_18_33)|=0) & (|marking(Ext_Mem_Acc_24_37)|=0) & (|marking(Ext_Mem_Acc_23_47)|=0) & (|marking(Ext_Mem_Acc_34_7)|=0) & (|marking(Ext_Mem_Acc_31_27)|=0) & (|marking(Ext_Mem_Acc_26_46)|=0) & (|marking(Ext_Mem_Acc_6_7)|=0) & (|marking(Ext_Mem_Acc_42_35)|=0) & (|marking(Ext_Mem_Acc_21_46)|=0) & (|marking(Ext_Mem_Acc_7_31)|=0) & (|marking(Ext_Mem_Acc_2_28)|=0) & (|marking(Ext_Mem_Acc_32_17)|=0) & (|marking(Ext_Mem_Acc_27_29)|=0) & (|marking(Ext_Mem_Acc_18_12)|=0) & (|marking(Ext_Mem_Acc_10_15)|=0) & (|marking(Ext_Mem_Acc_30_27)|=0) & (|marking(Ext_Mem_Acc_36_43)|=0) & (|marking(Ext_Mem_Acc_6_31)|=0) & (|marking(Ext_Mem_Acc_48_6)|=0) & (|marking(Ext_Mem_Acc_33_38)|=0) & (|marking(Ext_Mem_Acc_15_12)|=0) & (|marking(Ext_Mem_Acc_40_28)|=0) & (|marking(Ext_Mem_Acc_27_47)|=0) & (|marking(Ext_Mem_Acc_21_39)|=0) & (|marking(Ext_Mem_Acc_33_44)|=0) & (|marking(Ext_Mem_Acc_37_22)|=0) & (|marking(Ext_Mem_Acc_8_3)|=0) & (|marking(Ext_Mem_Acc_13_33)|=0) & (|marking(Ext_Mem_Acc_18_27)|=0) & (|marking(Ext_Mem_Acc_45_36)|=0) & (|marking(Ext_Mem_Acc_47_1)|=0) & (|marking(Ext_Mem_Acc_32_33)|=0) & (|marking(Ext_Mem_Acc_25_1)|=0) & (|marking(Ext_Mem_Acc_6_2)|=0) & (|marking(Ext_Mem_Acc_17_47)|=0) & (|marking(Ext_Mem_Acc_12_13)|=0) & (|marking(Ext_Mem_Acc_16_19)|=0) & (|marking(Ext_Mem_Acc_20_42)|=0) & (|marking(Ext_Mem_Acc_30_41)|=0) & (|marking(Ext_Mem_Acc_50_17)|=0) & (|marking(Ext_Mem_Acc_28_45)|=0) & (|marking(Ext_Mem_Acc_7_50)|=0) & (|marking(Ext_Mem_Acc_38_50)|=0) & (|marking(Ext_Mem_Acc_36_18)|=0) & (|marking(Ext_Mem_Acc_29_24)|=0) & (|marking(Ext_Mem_Acc_6_39)|=0) & (|marking(Ext_Mem_Acc_50_37)|=0) & (|marking(Ext_Mem_Acc_9_17)|=0) & (|marking(Ext_Mem_Acc_22_35)|=0) & (|marking(Ext_Mem_Acc_44_25)|=0) & (|marking(Ext_Mem_Acc_2_18)|=0) & (|marking(Ext_Mem_Acc_26_1)|=0) & (|marking(Ext_Mem_Acc_33_45)|=0) & (|marking(Ext_Mem_Acc_16_28)|=0) & (|marking(Ext_Mem_Acc_1_21)|=0) & (|marking(Ext_Mem_Acc_30_33)|=0) & (|marking(Ext_Mem_Acc_32_50)|=0) & (|marking(Ext_Mem_Acc_40_4)|=0) & (|marking(Ext_Mem_Acc_7_12)|=0) & (|marking(Ext_Mem_Acc_22_4)|=0) & (|marking(Ext_Mem_Acc_15_37)|=0) & (|marking(Ext_Mem_Acc_7_26)|=0) & (|marking(Ext_Mem_Acc_12_29)|=0) & (|marking(Ext_Mem_Acc_39_3)|=0) & (|marking(Ext_Mem_Acc_22_46)|=0) & (|marking(Ext_Mem_Acc_25_39)|=0) & (|marking(Ext_Mem_Acc_27_8)|=0) & (|marking(Ext_Mem_Acc_8_1)|=0) & (|marking(Ext_Mem_Acc_39_5)|=0) & (|marking(Ext_Mem_Acc_38_14)|=0) & (|marking(Ext_Mem_Acc_24_43)|=0) & (|marking(Ext_Mem_Acc_16_25)|=0) & (|marking(Ext_Mem_Acc_27_25)|=0) & (|marking(Ext_Mem_Acc_21_24)|=0) & (|marking(Ext_Mem_Acc_45_30)|=0) & (|marking(Ext_Mem_Acc_4_45)|=0) & (|marking(Ext_Mem_Acc_44_50)|=0) & (|marking(Ext_Mem_Acc_30_44)|=0) & (|marking(Ext_Mem_Acc_46_23)|=0) & (|marking(Ext_Mem_Acc_44_22)|=0) & (|marking(Ext_Mem_Acc_1_24)|=0) & (|marking(Ext_Mem_Acc_41_40)|=0) & (|marking(Ext_Mem_Acc_36_31)|=0) & (|marking(Ext_Mem_Acc_18_34)|=0) & (|marking(Ext_Mem_Acc_15_28)|=0) & (|marking(Ext_Mem_Acc_38_12)|=0) & (|marking(Ext_Mem_Acc_9_35)|=0) & (|marking(Ext_Mem_Acc_48_18)|=0) & (|marking(Ext_Mem_Acc_4_22)|=0) & (|marking(Ext_Mem_Acc_24_7)|=0) & (|marking(Ext_Mem_Acc_46_14)|=0) & (|marking(Ext_Mem_Acc_40_27)|=0) & (|marking(Ext_Mem_Acc_42_17)|=0) & (|marking(Ext_Mem_Acc_41_47)|=0) & (|marking(Ext_Mem_Acc_45_28)|=0) & (|marking(Ext_Mem_Acc_16_31)|=0) & (|marking(Ext_Mem_Acc_4_40)|=0) & (|marking(Ext_Mem_Acc_17_33)|=0) & (|marking(Ext_Mem_Acc_24_2)|=0) & (|marking(Ext_Mem_Acc_5_49)|=0) & (|marking(Ext_Mem_Acc_12_42)|=0) & (|marking(Ext_Mem_Acc_22_1)|=0) & (|marking(Ext_Mem_Acc_17_43)|=0) & (|marking(Ext_Mem_Acc_17_39)|=0) & (|marking(Ext_Mem_Acc_2_11)|=0) & (|marking(Ext_Mem_Acc_11_46)|=0) & (|marking(Ext_Mem_Acc_17_48)|=0) & (|marking(Ext_Mem_Acc_26_47)|=0) & (|marking(Ext_Mem_Acc_45_31)|=0) & (|marking(Ext_Mem_Acc_8_44)|=0) & (|marking(Ext_Mem_Acc_30_26)|=0) & (|marking(Ext_Mem_Acc_13_12)|=0) & (|marking(Ext_Mem_Acc_9_21)|=0) & (|marking(Ext_Mem_Acc_13_43)|=0) & (|marking(Ext_Mem_Acc_11_23)|=0) & (|marking(Ext_Mem_Acc_8_23)|=0) & (|marking(Ext_Mem_Acc_3_4)|=0) & (|marking(Ext_Mem_Acc_42_32)|=0) & (|marking(Ext_Mem_Acc_29_10)|=0) & (|marking(Ext_Mem_Acc_40_23)|=0) & (|marking(Ext_Mem_Acc_10_42)|=0) & (|marking(Ext_Mem_Acc_23_34)|=0) & (|marking(Ext_Mem_Acc_29_47)|=0) & (|marking(Ext_Mem_Acc_21_12)|=0) & (|marking(Ext_Mem_Acc_1_18)|=0) & (|marking(Ext_Mem_Acc_33_49)|=0) & (|marking(Ext_Mem_Acc_6_42)|=0) & (|marking(Ext_Mem_Acc_22_12)|=0) & (|marking(Ext_Mem_Acc_10_34)|=0) & (|marking(Ext_Mem_Acc_39_34)|=0) & (|marking(Ext_Mem_Acc_8_40)|=0) & (|marking(Ext_Mem_Acc_48_31)|=0) & (|marking(Ext_Mem_Acc_38_28)|=0) & (|marking(Ext_Mem_Acc_39_48)|=0) & (|marking(Ext_Mem_Acc_17_1)|=0) & (|marking(Ext_Mem_Acc_16_2)|=0) & (|marking(Ext_Mem_Acc_1_27)|=0) & (|marking(Ext_Mem_Acc_11_8)|=0) & (|marking(Ext_Mem_Acc_23_14)|=0) & (|marking(Ext_Mem_Acc_20_2)|=0) & (|marking(Ext_Mem_Acc_38_15)|=0) & (|marking(Ext_Mem_Acc_20_45)|=0) & (|marking(Ext_Mem_Acc_27_45)|=0) & (|marking(Ext_Mem_Acc_43_33)|=0) & (|marking(Ext_Mem_Acc_45_10)|=0) & (|marking(Ext_Mem_Acc_25_49)|=0) & (|marking(Ext_Mem_Acc_28_47)|=0) & (|marking(Ext_Mem_Acc_27_13)|=0) & (|marking(Ext_Mem_Acc_25_16)|=0) & (|marking(Ext_Mem_Acc_11_41)|=0) & (|marking(Ext_Mem_Acc_25_4)|=0) & (|marking(Ext_Mem_Acc_4_6)|=0) & (|marking(Ext_Mem_Acc_7_3)|=0) & (|marking(Ext_Mem_Acc_8_38)|=0) & (|marking(Ext_Mem_Acc_15_17)|=0) & (|marking(Ext_Mem_Acc_32_7)|=0) & (|marking(Ext_Mem_Acc_40_2)|=0) & (|marking(Ext_Mem_Acc_6_43)|=0) & (|marking(Ext_Mem_Acc_27_35)|=0) & (|marking(Ext_Mem_Acc_25_50)|=0) & (|marking(Ext_Mem_Acc_20_14)|=0) & (|marking(Ext_Mem_Acc_50_16)|=0) & (|marking(Ext_Mem_Acc_8_46)|=0) & (|marking(Ext_Mem_Acc_37_41)|=0) & (|marking(Ext_Mem_Acc_23_6)|=0) & (|marking(Ext_Mem_Acc_48_2)|=0) & (|marking(Ext_Mem_Acc_2_15)|=0) & (|marking(Ext_Mem_Acc_3_6)|=0) & (|marking(Ext_Mem_Acc_28_35)|=0) & (|marking(Ext_Mem_Acc_26_29)|=0) & (|marking(Ext_Mem_Acc_13_24)|=0) & (|marking(Ext_Mem_Acc_16_24)|=0) & (|marking(Ext_Mem_Acc_26_25)|=0) & (|marking(Ext_Mem_Acc_25_45)|=0) & (|marking(Ext_Mem_Acc_16_44)|=0) & (|marking(Ext_Mem_Acc_8_49)|=0) & (|marking(Ext_Mem_Acc_23_41)|=0) & (|marking(Ext_Mem_Acc_31_43)|=0) & (|marking(Ext_Mem_Acc_10_40)|=0) & (|marking(Ext_Mem_Acc_7_16)|=0) & (|marking(Ext_Mem_Acc_30_49)|=0) & (|marking(Ext_Mem_Acc_14_6)|=0) & (|marking(Ext_Mem_Acc_12_39)|=0) & (|marking(Ext_Mem_Acc_35_26)|=0) & (|marking(Ext_Mem_Acc_45_48)|=0) & (|marking(Ext_Mem_Acc_4_3)|=0) & (|marking(Ext_Mem_Acc_38_32)|=0) & (|marking(Ext_Mem_Acc_38_17)|=0) & (|marking(Ext_Mem_Acc_38_45)|=0) & (|marking(Ext_Mem_Acc_28_15)|=0) & (|marking(Ext_Mem_Acc_43_14)|=0) & (|marking(Ext_Mem_Acc_16_13)|=0) & (|marking(Ext_Mem_Acc_41_30)|=0) & (|marking(Ext_Mem_Acc_40_46)|=0) & (|marking(Ext_Mem_Acc_31_16)|=0) & (|marking(Ext_Mem_Acc_8_21)|=0) & (|marking(Ext_Mem_Acc_23_48)|=0) & (|marking(Ext_Mem_Acc_33_48)|=0) & (|marking(Ext_Mem_Acc_42_2)|=0) & (|marking(Ext_Mem_Acc_5_29)|=0) & (|marking(Ext_Mem_Acc_29_9)|=0) & (|marking(Ext_Mem_Acc_5_26)|=0) & (|marking(Ext_Mem_Acc_27_41)|=0) & (|marking(Ext_Mem_Acc_17_24)|=0) & (|marking(Ext_Mem_Acc_1_38)|=0) & (|marking(Ext_Mem_Acc_28_36)|=0) & (|marking(Ext_Mem_Acc_20_44)|=0) & (|marking(Ext_Mem_Acc_31_10)|=0) & (|marking(Ext_Mem_Acc_37_25)|=0) & (|marking(Ext_Mem_Acc_24_29)|=0) & (|marking(Ext_Mem_Acc_33_37)|=0) & (|marking(Ext_Mem_Acc_47_42)|=0) & (|marking(Ext_Mem_Acc_43_44)|=0) & (|marking(Ext_Mem_Acc_5_39)|=0) & (|marking(Ext_Mem_Acc_49_3)|=0) & (|marking(Ext_Mem_Acc_48_41)|=0) & (|marking(Ext_Mem_Acc_22_2)|=0) & (|marking(Ext_Mem_Acc_46_48)|=0) & (|marking(Ext_Mem_Acc_44_12)|=0) & (|marking(Ext_Mem_Acc_44_28)|=0) & (|marking(Ext_Mem_Acc_2_8)|=0) & (|marking(Ext_Mem_Acc_12_25)|=0) & (|marking(Ext_Mem_Acc_48_46)|=0) & (|marking(Ext_Mem_Acc_10_48)|=0) & (|marking(Ext_Mem_Acc_46_40)|=0) & (|marking(Ext_Mem_Acc_36_30)|=0) & (|marking(Ext_Mem_Acc_14_23)|=0) & (|marking(Ext_Mem_Acc_32_29)|=0) & (|marking(Ext_Mem_Acc_11_15)|=0) & (|marking(Ext_Mem_Acc_34_14)|=0) & (|marking(Ext_Mem_Acc_12_31)|=0) & (|marking(Ext_Mem_Acc_15_49)|=0) & (|marking(Ext_Mem_Acc_34_1)|=0) & (|marking(Ext_Mem_Acc_46_32)|=0) & (|marking(Ext_Mem_Acc_28_8)|=0) & (|marking(Ext_Mem_Acc_38_9)|=0) & (|marking(Ext_Mem_Acc_16_45)|=0) & (|marking(Ext_Mem_Acc_10_22)|=0) & (|marking(Ext_Mem_Acc_36_44)|=0) & (|marking(Ext_Mem_Acc_17_13)|=0) & (|marking(Ext_Mem_Acc_47_30)|=0) & (|marking(Ext_Mem_Acc_25_34)|=0) & (|marking(Ext_Mem_Acc_15_36)|=0) & (|marking(Ext_Mem_Acc_17_22)|=0) & (|marking(Ext_Mem_Acc_7_44)|=0) & (|marking(Ext_Mem_Acc_37_15)|=0) & (|marking(Ext_Mem_Acc_21_11)|=0) & (|marking(Ext_Mem_Acc_6_15)|=0) & (|marking(Ext_Mem_Acc_1_44)|=0) & (|marking(Ext_Mem_Acc_37_48)|=0) & (|marking(Ext_Mem_Acc_34_11)|=0) & (|marking(Ext_Mem_Acc_42_34)|=0) & (|marking(Ext_Mem_Acc_13_41)|=0) & (|marking(Ext_Mem_Acc_36_34)|=0) & (|marking(Ext_Mem_Acc_29_40)|=0) & (|marking(Ext_Mem_Acc_48_32)|=0) & (|marking(Ext_Mem_Acc_7_20)|=0) & (|marking(Ext_Mem_Acc_45_39)|=0) & (|marking(Ext_Mem_Acc_4_50)|=0) & (|marking(Ext_Mem_Acc_11_6)|=0) & (|marking(Ext_Mem_Acc_7_39)|=0) & (|marking(Ext_Mem_Acc_12_23)|=0) & (|marking(Ext_Mem_Acc_32_45)|=0) & (|marking(Ext_Mem_Acc_7_30)|=0) & (|marking(Ext_Mem_Acc_25_21)|=0) & (|marking(Ext_Mem_Acc_49_7)|=0) & (|marking(Ext_Mem_Acc_43_18)|=0) & (|marking(Ext_Mem_Acc_14_44)|=0) & (|marking(Ext_Mem_Acc_13_39)|=0) & (|marking(Ext_Mem_Acc_41_3)|=0) & (|marking(Ext_Mem_Acc_13_10)|=0) & (|marking(Ext_Mem_Acc_18_48)|=0) & (|marking(Ext_Mem_Acc_1_3)|=0) & (|marking(Ext_Mem_Acc_17_19)|=0) & (|marking(Ext_Mem_Acc_44_31)|=0) & (|marking(Ext_Mem_Acc_28_21)|=0) & (|marking(Ext_Mem_Acc_23_45)|=0) & (|marking(Ext_Mem_Acc_18_19)|=0) & (|marking(Ext_Mem_Acc_13_50)|=0) & (|marking(Ext_Mem_Acc_42_31)|=0) & (|marking(Ext_Mem_Acc_44_29)|=0) & (|marking(Ext_Mem_Acc_29_45)|=0) & (|marking(Ext_Mem_Acc_35_9)|=0) & (|marking(Ext_Mem_Acc_8_2)|=0) & (|marking(Ext_Mem_Acc_4_15)|=0) & (|marking(Ext_Mem_Acc_14_50)|=0) & (|marking(Ext_Mem_Acc_19_43)|=0) & (|marking(Ext_Mem_Acc_1_46)|=0) & (|marking(Ext_Mem_Acc_9_15)|=0) & (|marking(Ext_Mem_Acc_28_3)|=0) & (|marking(Ext_Mem_Acc_2_46)|=0) & (|marking(Ext_Mem_Acc_2_35)|=0) & (|marking(Ext_Mem_Acc_26_48)|=0) & (|marking(Ext_Mem_Acc_15_23)|=0) & (|marking(Ext_Mem_Acc_29_21)|=0) & (|marking(Ext_Mem_Acc_11_24)|=0) & (|marking(Ext_Mem_Acc_33_13)|=0) & (|marking(Ext_Mem_Acc_4_10)|=0) & (|marking(Ext_Mem_Acc_22_28)|=0) & (|marking(Ext_Mem_Acc_23_32)|=0) & (|marking(Ext_Mem_Acc_24_15)|=0) & (|marking(Ext_Mem_Acc_18_23)|=0) & (|marking(Ext_Mem_Acc_40_45)|=0) & (|marking(Ext_Mem_Acc_43_37)|=0) & (|marking(Ext_Mem_Acc_50_40)|=0) & (|marking(Ext_Mem_Acc_49_43)|=0) & (|marking(Ext_Mem_Acc_48_47)|=0) & (|marking(Ext_Mem_Acc_4_30)|=0) & (|marking(Ext_Mem_Acc_39_28)|=0) & (|marking(Ext_Mem_Acc_11_33)|=0) & (|marking(Ext_Mem_Acc_15_31)|=0) & (|marking(Ext_Mem_Acc_44_40)|=0) & (|marking(Ext_Mem_Acc_3_44)|=0) & (|marking(Ext_Mem_Acc_21_23)|=0) & (|marking(Ext_Mem_Acc_42_47)|=0) & (|marking(Ext_Mem_Acc_50_4)|=0) & (|marking(Ext_Mem_Acc_17_40)|=0) & (|marking(Ext_Mem_Acc_22_38)|=0) & (|marking(Ext_Mem_Acc_5_25)|=0) & (|marking(Ext_Mem_Acc_31_11)|=0) & (|marking(Ext_Mem_Acc_21_32)|=0) & (|marking(Ext_Mem_Acc_31_49)|=0) & (|marking(Ext_Mem_Acc_2_33)|=0) & (|marking(Ext_Mem_Acc_26_42)|=0) & (|marking(Ext_Mem_Acc_23_19)|=0) & (|marking(Ext_Mem_Acc_42_44)|=0) & (|marking(Ext_Mem_Acc_35_29)|=0) & (|marking(Ext_Mem_Acc_38_8)|=0) & (|marking(Ext_Mem_Acc_18_13)|=0) & (|marking(Ext_Mem_Acc_22_7)|=0) & (|marking(Ext_Mem_Acc_23_35)|=0) & (|marking(Ext_Mem_Acc_34_25)|=0) & (|marking(Ext_Mem_Acc_45_44)|=0) & (|marking(Ext_Mem_Acc_31_29)|=0) & (|marking(Ext_Mem_Acc_45_14)|=0) & (|marking(Ext_Mem_Acc_30_42)|=0) & (|marking(Ext_Mem_Acc_4_33)|=0) & (|marking(Ext_Mem_Acc_28_38)|=0) & (|marking(Ext_Mem_Acc_20_49)|=0) & (|marking(Ext_Mem_Acc_46_35)|=0) & (|marking(Ext_Mem_Acc_43_21)|=0) & (|marking(Ext_Mem_Acc_16_33)|=0) & (|marking(Ext_Mem_Acc_26_27)|=0) & (|marking(Ext_Mem_Acc_48_38)|=0) & (|marking(Ext_Mem_Acc_22_24)|=0) & (|marking(Ext_Mem_Acc_45_23)|=0) & (|marking(Ext_Mem_Acc_34_29)|=0) & (|marking(Ext_Mem_Acc_24_12)|=0) & (|marking(Ext_Mem_Acc_13_25)|=0) & (|marking(Ext_Mem_Acc_20_22)|=0) & (|marking(Ext_Mem_Acc_10_18)|=0) & (|marking(Ext_Mem_Acc_47_7)|=0) & (|marking(Ext_Mem_Acc_37_16)|=0) & (|marking(Ext_Mem_Acc_47_14)|=0) & (|marking(Ext_Mem_Acc_11_10)|=0) & (|marking(Ext_Mem_Acc_2_45)|=0) & (|marking(Ext_Mem_Acc_9_46)|=0) & (|marking(Ext_Mem_Acc_4_19)|=0) & (|marking(Ext_Mem_Acc_27_34)|=0) & (|marking(Ext_Mem_Acc_48_12)|=0) & (|marking(Ext_Mem_Acc_25_11)|=0) & (|marking(Ext_Mem_Acc_7_17)|=0) & (|marking(Ext_Mem_Acc_33_16)|=0) & (|marking(Ext_Mem_Acc_49_50)|=0) & (|marking(Ext_Mem_Acc_33_46)|=0) & (|marking(Ext_Mem_Acc_25_15)|=0) & (|marking(Ext_Mem_Acc_49_42)|=0) & (|marking(Ext_Mem_Acc_3_21)|=0) & (|marking(Ext_Mem_Acc_23_30)|=0) & (|marking(Ext_Mem_Acc_3_16)|=0) & (|marking(Ext_Mem_Acc_18_5)|=0) & (|marking(Ext_Mem_Acc_14_32)|=0) & (|marking(Ext_Mem_Acc_44_48)|=0) & (|marking(Ext_Mem_Acc_41_44)|=0) & (|marking(Ext_Mem_Acc_18_50)|=0) & (|marking(Ext_Mem_Acc_19_18)|=0) & (|marking(Ext_Mem_Acc_16_5)|=0) & (|marking(Ext_Mem_Acc_28_22)|=0) & (|marking(Ext_Mem_Acc_30_47)|=0) & (|marking(Ext_Mem_Acc_9_32)|=0) & (|marking(Ext_Mem_Acc_17_21)|=0) & (|marking(Ext_Mem_Acc_10_37)|=0) & (|marking(Ext_Mem_Acc_23_38)|=0) & (|marking(Ext_Mem_Acc_8_29)|=0) & (|marking(Ext_Mem_Acc_2_16)|=0) & (|marking(Ext_Mem_Acc_5_44)|=0) & (|marking(Ext_Mem_Acc_36_50)|=0) & (|marking(Ext_Mem_Acc_39_42)|=0) & (|marking(Ext_Mem_Acc_4_34)|=0) & (|marking(Ext_Mem_Acc_41_34)|=0) & (|marking(Ext_Mem_Acc_31_39)|=0) & (|marking(Ext_Mem_Acc_41_14)|=0) & (|marking(Ext_Mem_Acc_16_20)|=0) & (|marking(Ext_Mem_Acc_45_46)|=0) & (|marking(Ext_Mem_Acc_49_47)|=0) & (|marking(Ext_Mem_Acc_22_18)|=0) & (|marking(Ext_Mem_Acc_16_49)|=0) & (|marking(Ext_Mem_Acc_11_4)|=0) & (|marking(Ext_Mem_Acc_46_26)|=0) & (|marking(Ext_Mem_Acc_14_18)|=0) & (|marking(Ext_Mem_Acc_20_36)|=0) & (|marking(Ext_Mem_Acc_45_9)|=0) & (|marking(Ext_Mem_Acc_30_1)|=0) & (|marking(Ext_Mem_Acc_4_18)|=0) & (|marking(Ext_Mem_Acc_20_17)|=0) & (|marking(Ext_Mem_Acc_34_12)|=0) & (|marking(Ext_Mem_Acc_47_45)|=0) & (|marking(Ext_Mem_Acc_24_49)|=0) & (|marking(Ext_Mem_Acc_31_17)|=0) & (|marking(Ext_Mem_Acc_29_33)|=0) & (|marking(Ext_Mem_Acc_30_39)|=0) & (|marking(Ext_Mem_Acc_33_26)|=0) & (|marking(Ext_Mem_Acc_4_9)|=0) & (|marking(Ext_Mem_Acc_26_32)|=0) & (|marking(Ext_Mem_Acc_25_12)|=0) & (|marking(Ext_Mem_Acc_26_34)|=0) & (|marking(Ext_Mem_Acc_32_49)|=0) & (|marking(Ext_Mem_Acc_40_44)|=0) & (|marking(Ext_Mem_Acc_47_2)|=0) & (|marking(Ext_Mem_Acc_2_27)|=0) & (|marking(Ext_Mem_Acc_11_43)|=0) & (|marking(Ext_Mem_Acc_16_4)|=0) & (|marking(Ext_Mem_Acc_29_49)|=0) & (|marking(Ext_Mem_Acc_34_39)|=0) & (|marking(Ext_Mem_Acc_45_1)|=0) & (|marking(Ext_Mem_Acc_38_46)|=0) & (|marking(Ext_Mem_Acc_27_4)|=0) & (|marking(Ext_Mem_Acc_10_26)|=0) & (|marking(Ext_Mem_Acc_19_48)|=0) & (|marking(Ext_Mem_Acc_26_7)|=0) & (|marking(Ext_Mem_Acc_28_7)|=0) & (|marking(Ext_Mem_Acc_25_32)|=0) & (|marking(Ext_Mem_Acc_8_6)|=0) & (|marking(Ext_Mem_Acc_32_24)|=0) & (|marking(Ext_Mem_Acc_12_43)|=0) & (|marking(Ext_Mem_Acc_25_40)|=0) & (|marking(Ext_Mem_Acc_24_47)|=0) & (|marking(Ext_Mem_Acc_6_40)|=0) & (|marking(Ext_Mem_Acc_24_18)|=0) & (|marking(Ext_Mem_Acc_33_22)|=0) & (|marking(Ext_Mem_Acc_41_39)|=0) & (|marking(Ext_Mem_Acc_15_45)|=0) & (|marking(Ext_Mem_Acc_23_50)|=0) & (|marking(Ext_Mem_Acc_9_40)|=0) & (|marking(Ext_Mem_Acc_17_38)|=0) & (|marking(Ext_Mem_Acc_38_31)|=0) & (|marking(Ext_Mem_Acc_9_3)|=0) & (|marking(Ext_Mem_Acc_41_6)|=0) & (|marking(Ext_Mem_Acc_23_8)|=0) & (|marking(Ext_Mem_Acc_50_15)|=0) & (|marking(Ext_Mem_Acc_29_28)|=0) & (|marking(Ext_Mem_Acc_24_38)|=0) & (|marking(Ext_Mem_Acc_3_29)|=0) & (|marking(Ext_Mem_Acc_14_34)|=0) & (|marking(Ext_Mem_Acc_49_22)|=0) & (|marking(Ext_Mem_Acc_49_13)|=0) & (|marking(Ext_Mem_Acc_22_27)|=0) & (|marking(Ext_Mem_Acc_7_24)|=0) & (|marking(Ext_Mem_Acc_14_48)|=0) & (|marking(Ext_Mem_Acc_2_25)|=0) & (|marking(Ext_Mem_Acc_5_48)|=0) & (|marking(Ext_Mem_Acc_18_43)|=0) & (|marking(Ext_Mem_Acc_30_3)|=0) & (|marking(Ext_Mem_Acc_40_5)|=0) & (|marking(Ext_Mem_Acc_39_26)|=0) & (|marking(Ext_Mem_Acc_19_35)|=0) & (|marking(Ext_Mem_Acc_4_11)|=0) & (|marking(Ext_Mem_Acc_44_42)|=0) & (|marking(Ext_Mem_Acc_3_9)|=0) & (|marking(Ext_Mem_Acc_50_46)|=0) & (|marking(Ext_Mem_Acc_9_4)|=0) & (|marking(Ext_Mem_Acc_22_41)|=0) & (|marking(Ext_Mem_Acc_19_27)|=0) & (|marking(Ext_Mem_Acc_17_35)|=0) & (|marking(Ext_Mem_Acc_34_42)|=0) & (|marking(Ext_Mem_Acc_2_30)|=0) & (|marking(Ext_Mem_Acc_3_48)|=0) & (|marking(Ext_Mem_Acc_19_9)|=0) & (|marking(Ext_Mem_Acc_37_42)|=0) & (|marking(Ext_Mem_Acc_26_17)|=0) & (|marking(Ext_Mem_Acc_8_10)|=0) & (|marking(Ext_Mem_Acc_20_11)|=0) & (|marking(Ext_Mem_Acc_47_36)|=0) & (|marking(Ext_Mem_Acc_25_43)|=0) & (|marking(Ext_Mem_Acc_48_49)|=0) & (|marking(Ext_Mem_Acc_48_26)|=0) & (|marking(Ext_Mem_Acc_37_6)|=0) & (|marking(Ext_Mem_Acc_13_4)|=0) & (|marking(Ext_Mem_Acc_46_12)|=0) & (|marking(Ext_Mem_Acc_8_22)|=0) & (|marking(Ext_Mem_Acc_30_2)|=0) & (|marking(Ext_Mem_Acc_11_17)|=0) & (|marking(Ext_Mem_Acc_8_32)|=0) & (|marking(Ext_Mem_Acc_43_23)|=0) & (|marking(Ext_Mem_Acc_27_5)|=0) & (|marking(Ext_Mem_Acc_37_7)|=0) & (|marking(Ext_Mem_Acc_29_37)|=0) & (|marking(Ext_Mem_Acc_46_24)|=0) & (|marking(Ext_Mem_Acc_37_17)|=0) & (|marking(Ext_Mem_Acc_20_33)|=0) & (|marking(Ext_Mem_Acc_13_27)|=0) & (|marking(Ext_Mem_Acc_46_4)|=0) & (|marking(Ext_Mem_Acc_35_33)|=0) & (|marking(Ext_Mem_Acc_43_3)|=0) & (|marking(Ext_Mem_Acc_41_21)|=0) & (|marking(Ext_Mem_Acc_1_40)|=0) & (|marking(Ext_Mem_Acc_32_27)|=0) & (|marking(Ext_Mem_Acc_39_4)|=0) & (|marking(Ext_Mem_Acc_5_23)|=0) & (|marking(Ext_Mem_Acc_49_25)|=0) & (|marking(Ext_Mem_Acc_4_5)|=0) & (|marking(Ext_Mem_Acc_32_14)|=0) & (|marking(Ext_Mem_Acc_46_31)|=0) & (|marking(Ext_Mem_Acc_24_50)|=0) & (|marking(Ext_Mem_Acc_24_31)|=0) & (|marking(Ext_Mem_Acc_12_46)|=0) & (|marking(Ext_Mem_Acc_21_36)|=0) & (|marking(Ext_Mem_Acc_25_30)|=0) & (|marking(Ext_Mem_Acc_17_6)|=0) & (|marking(Ext_Mem_Acc_11_49)|=0) & (|marking(Ext_Mem_Acc_31_45)|=0) & (|marking(Ext_Mem_Acc_6_27)|=0) & (|marking(Ext_Mem_Acc_48_23)|=0) & (|marking(Ext_Mem_Acc_19_36)|=0) & (|marking(Ext_Mem_Acc_26_40)|=0) & (|marking(Ext_Mem_Acc_2_12)|=0) & (|marking(Ext_Mem_Acc_41_26)|=0) & (|marking(Ext_Mem_Acc_21_2)|=0) & (|marking(Ext_Mem_Acc_24_44)|=0) & (|marking(Ext_Mem_Acc_34_46)|=0) & (|marking(Ext_Mem_Acc_25_13)|=0) & (|marking(Ext_Mem_Acc_32_19)|=0) & (|marking(Ext_Mem_Acc_24_5)|=0) & (|marking(Ext_Mem_Acc_49_26)|=0) & (|marking(Ext_Mem_Acc_6_33)|=0) & (|marking(Ext_Mem_Acc_6_11)|=0) & (|marking(Ext_Mem_Acc_31_36)|=0) & (|marking(Ext_Mem_Acc_27_46)|=0) & (|marking(Ext_Mem_Acc_37_47)|=0) & (|marking(Ext_Mem_Acc_10_36)|=0) & (|marking(Ext_Mem_Acc_33_3)|=0) & (|marking(Ext_Mem_Acc_8_7)|=0) & (|marking(Ext_Mem_Acc_17_16)|=0) & (|marking(Ext_Mem_Acc_14_25)|=0) & (|marking(Ext_Mem_Acc_25_38)|=0) & (|marking(Ext_Mem_Acc_5_10)|=0) & (|marking(Ext_Mem_Acc_3_2)|=0) & (|marking(Ext_Mem_Acc_22_26)|=0) & (|marking(Ext_Mem_Acc_25_37)|=0) & (|marking(Ext_Mem_Acc_39_19)|=0) & (|marking(Ext_Mem_Acc_25_24)|=0) & (|marking(Ext_Mem_Acc_41_16)|=0) & (|marking(Ext_Mem_Acc_36_1)|=0) & (|marking(Ext_Mem_Acc_35_6)|=0) & (|marking(Ext_Mem_Acc_42_36)|=0) & (|marking(Ext_Mem_Acc_26_24)|=0) & (|marking(Ext_Mem_Acc_33_15)|=0) & (|marking(Ext_Mem_Acc_29_39)|=0) & (|marking(Ext_Mem_Acc_16_29)|=0) & (|marking(Ext_Mem_Acc_50_32)|=0) & (|marking(Ext_Mem_Acc_9_42)|=0) & (|marking(Ext_Mem_Acc_10_9)|=0) & (|marking(Ext_Mem_Acc_39_32)|=0) & (|marking(Ext_Mem_Acc_9_45)|=0) & (|marking(Ext_Mem_Acc_3_45)|=0) & (|marking(Ext_Mem_Acc_9_50)|=0) & (|marking(Ext_Mem_Acc_12_4)|=0) & (|marking(Ext_Mem_Acc_2_6)|=0) & (|marking(Ext_Mem_Acc_23_33)|=0) & (|marking(Ext_Mem_Acc_5_1)|=0) & (|marking(Ext_Mem_Acc_34_45)|=0) & (|marking(Ext_Mem_Acc_4_42)|=0) & (|marking(Ext_Mem_Acc_50_12)|=0) & (|marking(Ext_Mem_Acc_27_17)|=0) & (|marking(Ext_Mem_Acc_28_34)|=0) & (|marking(Ext_Mem_Acc_45_47)|=0) & (|marking(Ext_Mem_Acc_15_16)|=0) & (|marking(Ext_Mem_Acc_19_29)|=0) & (|marking(Ext_Mem_Acc_50_5)|=0) & (|marking(Ext_Mem_Acc_42_33)|=0) & (|marking(Ext_Mem_Acc_49_11)|=0) & (|marking(Ext_Mem_Acc_26_30)|=0) & (|marking(Ext_Mem_Acc_21_9)|=0) & (|marking(Ext_Mem_Acc_11_45)|=0) & (|marking(Ext_Mem_Acc_15_9)|=0) & (|marking(Ext_Mem_Acc_35_50)|=0) & (|marking(Ext_Mem_Acc_28_1)|=0) & (|marking(Ext_Mem_Acc_32_46)|=0) & (|marking(Ext_Mem_Acc_1_34)|=0) & (|marking(Ext_Mem_Acc_43_34)|=0) & (|marking(Ext_Mem_Acc_35_18)|=0) & (|marking(Ext_Mem_Acc_25_2)|=0) & (|marking(Ext_Mem_Acc_19_46)|=0) & (|marking(Ext_Mem_Acc_35_4)|=0) & (|marking(Ext_Mem_Acc_21_4)|=0) & (|marking(Ext_Mem_Acc_47_22)|=0) & (|marking(Ext_Mem_Acc_20_37)|=0) & (|marking(Ext_Mem_Acc_17_42)|=0) & (|marking(Ext_Mem_Acc_10_11)|=0) & (|marking(Ext_Mem_Acc_4_17)|=0) & (|marking(Ext_Mem_Acc_38_49)|=0) & (|marking(Ext_Mem_Acc_49_23)|=0) & (|marking(Ext_Mem_Acc_5_21)|=0) & (|marking(Ext_Mem_Acc_45_27)|=0) & (|marking(Ext_Mem_Acc_24_40)|=0) & (|marking(Ext_Mem_Acc_23_18)|=0) & (|marking(Ext_Mem_Acc_13_8)|=0) & (|marking(Ext_Mem_Acc_39_23)|=0) & (|marking(Ext_Mem_Acc_29_3)|=0) & (|marking(Ext_Mem_Acc_43_50)|=0) & (|marking(Ext_Mem_Acc_39_50)|=0) & (|marking(Ext_Mem_Acc_13_35)|=0) & (|marking(Ext_Mem_Acc_45_50)|=0) & (|marking(Ext_Mem_Acc_5_28)|=0) & (|marking(Ext_Mem_Acc_46_3)|=0) & (|marking(Ext_Mem_Acc_45_35)|=0) & (|marking(Ext_Mem_Acc_21_28)|=0) & (|marking(Ext_Mem_Acc_18_35)|=0) & (|marking(Ext_Mem_Acc_11_27)|=0) & (|marking(Ext_Mem_Acc_34_33)|=0) & (|marking(Ext_Mem_Acc_44_38)|=0) & (|marking(Ext_Mem_Acc_50_44)|=0) & (|marking(Ext_Mem_Acc_26_39)|=0) & (|marking(Ext_Mem_Acc_28_48)|=0) & (|marking(Ext_Mem_Acc_10_43)|=0) & (|marking(Ext_Mem_Acc_18_4)|=0) & (|marking(Ext_Mem_Acc_31_34)|=0) & (|marking(Ext_Mem_Acc_25_10)|=0) & (|marking(Ext_Mem_Acc_39_41)|=0) & (|marking(Ext_Mem_Acc_34_30)|=0) & (|marking(Ext_Mem_Acc_38_1)|=0) & (|marking(Ext_Mem_Acc_11_44)|=0) & (|marking(Ext_Mem_Acc_8_43)|=0) & (|marking(Ext_Mem_Acc_2_39)|=0) & (|marking(Ext_Mem_Acc_46_45)|=0) & (|marking(Ext_Mem_Acc_27_12)|=0) & (|marking(Ext_Mem_Acc_45_6)|=0) & (|marking(Ext_Mem_Acc_39_14)|=0) & (|marking(Ext_Mem_Acc_38_5)|=0) & (|marking(Ext_Mem_Acc_46_49)|=0) & (|marking(Ext_Mem_Acc_3_13)|=0) & (|marking(Ext_Mem_Acc_41_50)|=0) & (|marking(Ext_Mem_Acc_48_29)|=0) & (|marking(Ext_Mem_Acc_26_14)|=0) & (|marking(Ext_Mem_Acc_21_25)|=0) & (|marking(Ext_Mem_Acc_50_11)|=0) & (|marking(Ext_Mem_Acc_4_35)|=0) & (|marking(Ext_Mem_Acc_5_24)|=0) & (|marking(Ext_Mem_Acc_41_27)|=0) & (|marking(Ext_Mem_Acc_16_34)|=0) & (|marking(Ext_Mem_Acc_46_37)|=0) & (|marking(Ext_Mem_Acc_1_13)|=0) & (|marking(Ext_Mem_Acc_3_8)|=0) & (|marking(Ext_Mem_Acc_16_42)|=0) & (|marking(Ext_Mem_Acc_18_28)|=0) & (|marking(Ext_Mem_Acc_32_31)|=0) & (|marking(Ext_Mem_Acc_13_38)|=0) & (|marking(Ext_Mem_Acc_20_7)|=0) & (|marking(Ext_Mem_Acc_17_3)|=0) & (|marking(Ext_Mem_Acc_24_45)|=0) & (|marking(Ext_Mem_Acc_36_26)|=0) & (|marking(Ext_Mem_Acc_47_13)|=0) & (|marking(Ext_Mem_Acc_3_47)|=0) & (|marking(Ext_Mem_Acc_25_44)|=0) & (|marking(Ext_Mem_Acc_27_42)|=0) & (|marking(Ext_Mem_Acc_47_37)|=0) & (|marking(Ext_Mem_Acc_8_13)|=0) & (|marking(Ext_Mem_Acc_41_17)|=0) & (|marking(Ext_Mem_Acc_47_24)|=0) & (|marking(Ext_Mem_Acc_13_17)|=0) & (|marking(Ext_Mem_Acc_13_16)|=0) & (|marking(Ext_Mem_Acc_46_6)|=0) & (|marking(Ext_Mem_Acc_18_7)|=0) & (|marking(Ext_Mem_Acc_22_30)|=0) & (|marking(Ext_Mem_Acc_43_19)|=0) & (|marking(Ext_Mem_Acc_6_49)|=0) & (|marking(Ext_Mem_Acc_33_39)|=0) & (|marking(Ext_Mem_Acc_2_50)|=0) & (|marking(Ext_Mem_Acc_1_9)|=0) & (|marking(Ext_Mem_Acc_20_1)|=0) & (|marking(Ext_Mem_Acc_6_24)|=0) & (|marking(Ext_Mem_Acc_14_1)|=0) & (|marking(Ext_Mem_Acc_36_28)|=0) & (|marking(Ext_Mem_Acc_48_8)|=0) & (|marking(Ext_Mem_Acc_7_34)|=0) & (|marking(Ext_Mem_Acc_46_1)|=0) & (|marking(Ext_Mem_Acc_42_37)|=0) & (|marking(Ext_Mem_Acc_15_50)|=0) & (|marking(Ext_Mem_Acc_30_32)|=0) & (|marking(Ext_Mem_Acc_40_22)|=0) & (|marking(Ext_Mem_Acc_21_1)|=0) & (|marking(Ext_Mem_Acc_6_37)|=0) & (|marking(Ext_Mem_Acc_23_4)|=0) & (|marking(Ext_Mem_Acc_31_47)|=0) & (|marking(Ext_Mem_Acc_1_31)|=0) & (|marking(Ext_Mem_Acc_50_47)|=0) & (|marking(Ext_Mem_Acc_9_22)|=0) & (|marking(Ext_Mem_Acc_42_11)|=0) & (|marking(Ext_Mem_Acc_19_37)|=0) & (|marking(Ext_Mem_Acc_24_9)|=0) & (|marking(Ext_Mem_Acc_44_18)|=0) & (|marking(Ext_Mem_Acc_25_5)|=0) & (|marking(Ext_Mem_Acc_33_14)|=0) & (|marking(Ext_Mem_Acc_23_36)|=0) & (|marking(Ext_Mem_Acc_19_40)|=0) & (|marking(Ext_Mem_Acc_46_41)|=0) & (|marking(Ext_Mem_Acc_25_47)|=0) & (|marking(Ext_Mem_Acc_4_36)|=0) & (|marking(Ext_Mem_Acc_26_16)|=0) & (|marking(Ext_Mem_Acc_26_23)|=0) & (|marking(Ext_Mem_Acc_9_34)|=0) & (|marking(Ext_Mem_Acc_43_8)|=0) & (|marking(Ext_Mem_Acc_1_33)|=0) & (|marking(Ext_Mem_Acc_35_44)|=0) & (|marking(Ext_Mem_Acc_24_16)|=0) & (|marking(Ext_Mem_Acc_13_36)|=0) & (|marking(Ext_Mem_Acc_21_48)|=0) & (|marking(Ext_Mem_Acc_35_13)|=0) & (|marking(Ext_Mem_Acc_45_19)|=0) & (|marking(Ext_Mem_Acc_20_31)|=0) & (|marking(Ext_Mem_Acc_32_48)|=0) & (|marking(Ext_Mem_Acc_18_42)|=0) & (|marking(Ext_Mem_Acc_18_11)|=0) & (|marking(Ext_Mem_Acc_7_15)|=0) & (|marking(Ext_Mem_Acc_33_35)|=0) & (|marking(Ext_Mem_Acc_36_25)|=0) & (|marking(Ext_Mem_Acc_6_16)|=0) & (|marking(Ext_Mem_Acc_17_31)|=0) & (|marking(Ext_Mem_Acc_37_23)|=0) & (|marking(Ext_Mem_Acc_16_21)|=0) & (|marking(Ext_Mem_Acc_6_19)|=0) & (|marking(Ext_Mem_Acc_39_30)|=0) & (|marking(Ext_Mem_Acc_40_41)|=0) & (|marking(Ext_Mem_Acc_5_9)|=0) & (|marking(Ext_Mem_Acc_17_36)|=0) & (|marking(Ext_Mem_Acc_36_4)|=0) & (|marking(Ext_Mem_Acc_38_30)|=0) & (|marking(Ext_Mem_Acc_31_44)|=0) & (|marking(Ext_Mem_Acc_8_19)|=0) & (|marking(Ext_Mem_Acc_48_45)|=0) & (|marking(Ext_Mem_Acc_42_19)|=0) & (|marking(Ext_Mem_Acc_6_26)|=0) & (|marking(Ext_Mem_Acc_28_42)|=0) & (|marking(Ext_Mem_Acc_24_21)|=0) & (|marking(Ext_Mem_Acc_30_29)|=0) & (|marking(Ext_Mem_Acc_26_5)|=0) & (|marking(Ext_Mem_Acc_33_43)|=0) & (|marking(Ext_Mem_Acc_14_29)|=0) & (|marking(Ext_Mem_Acc_6_46)|=0) & (|marking(Ext_Mem_Acc_41_4)|=0) & (|marking(Ext_Mem_Acc_13_28)|=0) & (|marking(Ext_Mem_Acc_3_11)|=0) & (|marking(Ext_Mem_Acc_3_24)|=0) & (|marking(Ext_Mem_Acc_22_31)|=0) & (|marking(Ext_Mem_Acc_26_11)|=0) & (|marking(Ext_Mem_Acc_3_23)|=0) & (|marking(Ext_Mem_Acc_2_38)|=0) & (|marking(Ext_Mem_Acc_30_19)|=0) & (|marking(Ext_Mem_Acc_8_15)|=0) & (|marking(Ext_Mem_Acc_31_18)|=0) & (|marking(Ext_Mem_Acc_37_20)|=0) & (|marking(Ext_Mem_Acc_1_10)|=0) & (|marking(Ext_Mem_Acc_38_16)|=0) & (|marking(Ext_Mem_Acc_9_36)|=0) & (|marking(Ext_Mem_Acc_20_15)|=0) & (|marking(Ext_Mem_Acc_23_44)|=0) & (|marking(Ext_Mem_Acc_19_26)|=0) & (|marking(Ext_Mem_Acc_43_45)|=0) & (|marking(Ext_Mem_Acc_35_23)|=0) & (|marking(Ext_Mem_Acc_7_22)|=0) & (|marking(Ext_Mem_Acc_24_6)|=0) & (|marking(Ext_Mem_Acc_18_32)|=0) & (|marking(Ext_Mem_Acc_16_27)|=0) & (|marking(Ext_Mem_Acc_9_47)|=0) & (|marking(Ext_Mem_Acc_42_30)|=0) & (|marking(Ext_Mem_Acc_18_15)|=0) & (|marking(Ext_Mem_Acc_20_25)|=0) & (|marking(Ext_Mem_Acc_35_12)|=0) & (|marking(Ext_Mem_Acc_22_33)|=0) & (|marking(Ext_Mem_Acc_7_28)|=0) & (|marking(Ext_Mem_Acc_39_43)|=0) & (|marking(Ext_Mem_Acc_7_42)|=0) & (|marking(Ext_Mem_Acc_23_7)|=0) & (|marking(Ext_Mem_Acc_7_36)|=0) & (|marking(Ext_Mem_Acc_43_25)|=0) & (|marking(Ext_Mem_Acc_27_2)|=0) & (|marking(Ext_Mem_Acc_42_21)|=0) & (|marking(Ext_Mem_Acc_11_20)|=0) & (|marking(Ext_Mem_Acc_44_33)|=0) & (|marking(Ext_Mem_Acc_16_8)|=0) & (|marking(Ext_Mem_Acc_25_6)|=0) & (|marking(Ext_Mem_Acc_9_7)|=0) & (|marking(Ext_Mem_Acc_43_36)|=0) & (|marking(Ext_Mem_Acc_7_45)|=0) & (|marking(Ext_Mem_Acc_47_21)|=0) & (|marking(Ext_Mem_Acc_1_48)|=0) & (|marking(Ext_Mem_Acc_45_24)|=0) & (|marking(Ext_Mem_Acc_26_4)|=0) & (|marking(Ext_Mem_Acc_50_29)|=0) & (|marking(Ext_Mem_Acc_14_27)|=0) & (|marking(Ext_Mem_Acc_40_15)|=0) & (|marking(Ext_Mem_Acc_28_4)|=0) & (|marking(Ext_Mem_Acc_48_16)|=0) & (|marking(Ext_Mem_Acc_48_10)|=0) & (|marking(Ext_Mem_Acc_33_41)|=0) & (|marking(Ext_Mem_Acc_32_30)|=0) & (|marking(Ext_Mem_Acc_36_32)|=0) & (|marking(Ext_Mem_Acc_14_35)|=0) & (|marking(Ext_Mem_Acc_8_24)|=0) & (|marking(Ext_Mem_Acc_34_8)|=0) & (|marking(Ext_Mem_Acc_49_32)|=0) & (|marking(Ext_Mem_Acc_19_28)|=0) & (|marking(Ext_Mem_Acc_24_25)|=0) & (|marking(Ext_Mem_Acc_28_46)|=0) & (|marking(Ext_Mem_Acc_33_9)|=0) & (|marking(Ext_Mem_Acc_45_34)|=0) & (|marking(Ext_Mem_Acc_21_34)|=0) & (|marking(Ext_Mem_Acc_40_12)|=0) & (|marking(Ext_Mem_Acc_3_26)|=0) & (|marking(Ext_Mem_Acc_32_26)|=0) & (|marking(Ext_Mem_Acc_27_6)|=0) & (|marking(Ext_Mem_Acc_14_4)|=0) & (|marking(Ext_Mem_Acc_24_10)|=0) & (|marking(Ext_Mem_Acc_18_40)|=0) & (|marking(Ext_Mem_Acc_26_21)|=0) & (|marking(Ext_Mem_Acc_41_19)|=0) & (|marking(Ext_Mem_Acc_37_13)|=0) & (|marking(Ext_Mem_Acc_12_10)|=0) & (|marking(Ext_Mem_Acc_42_4)|=0) & (|marking(Ext_Mem_Acc_17_11)|=0) & (|marking(Ext_Mem_Acc_23_2)|=0) & (|marking(Ext_Mem_Acc_7_5)|=0) & (|marking(Ext_Mem_Acc_14_15)|=0) & (|marking(Ext_Mem_Acc_31_8)|=0) & (|marking(Ext_Mem_Acc_50_2)|=0) & (|marking(Ext_Mem_Acc_35_2)|=0) & (|marking(Ext_Mem_Acc_31_23)|=0) & (|marking(Ext_Mem_Acc_15_20)|=0) & (|marking(Ext_Mem_Acc_12_17)|=0) & (|marking(Ext_Mem_Acc_32_37)|=0) & (|marking(Ext_Mem_Acc_33_10)|=0) & (|marking(Ext_Mem_Acc_49_27)|=0) & (|marking(Ext_Mem_Acc_37_29)|=0) & (|marking(Ext_Mem_Acc_7_2)|=0) & (|marking(Ext_Mem_Acc_42_39)|=0) & (|marking(Ext_Mem_Acc_22_45)|=0) & (|marking(Ext_Mem_Acc_7_40)|=0) & (|marking(Ext_Mem_Acc_1_45)|=0) & (|marking(Ext_Mem_Acc_24_4)|=0) & (|marking(Ext_Mem_Acc_2_49)|=0) & (|marking(Ext_Mem_Acc_42_45)|=0) & (|marking(Ext_Mem_Acc_14_45)|=0) & (|marking(Ext_Mem_Acc_20_43)|=0) & (|marking(Ext_Mem_Acc_13_18)|=0) & (|marking(Ext_Mem_Acc_38_47)|=0) & (|marking(Ext_Mem_Acc_35_14)|=0) & (|marking(Ext_Mem_Acc_45_16)|=0) & (|marking(Ext_Mem_Acc_8_11)|=0) & (|marking(Ext_Mem_Acc_15_11)|=0) & (|marking(Ext_Mem_Acc_14_46)|=0) & (|marking(Ext_Mem_Acc_31_22)|=0) & (|marking(Ext_Mem_Acc_16_48)|=0) & (|marking(Ext_Mem_Acc_31_25)|=0) & (|marking(Ext_Mem_Acc_36_13)|=0) & (|marking(Ext_Mem_Acc_21_49)|=0) & (|marking(Ext_Mem_Acc_32_4)|=0) & (|marking(Ext_Mem_Acc_14_47)|=0) & (|marking(Ext_Mem_Acc_27_36)|=0) & (|marking(Ext_Mem_Acc_38_24)|=0) & (|marking(Ext_Mem_Acc_9_24)|=0) & (|marking(Ext_Mem_Acc_26_33)|=0) & (|marking(Ext_Mem_Acc_44_3)|=0) & (|marking(Ext_Mem_Acc_49_1)|=0) & (|marking(Ext_Mem_Acc_21_50)|=0) & (|marking(Ext_Mem_Acc_44_43)|=0) & (|marking(Ext_Mem_Acc_8_30)|=0) & (|marking(Ext_Mem_Acc_33_5)|=0) & (|marking(Ext_Mem_Acc_3_36)|=0) & (|marking(Ext_Mem_Acc_40_3)|=0) & (|marking(Ext_Mem_Acc_43_42)|=0) & (|marking(Ext_Mem_Acc_24_48)|=0) & (|marking(Ext_Mem_Acc_43_6)|=0) & (|marking(Ext_Mem_Acc_15_24)|=0) & (|marking(Ext_Mem_Acc_9_8)|=0) & (|marking(Ext_Mem_Acc_33_23)|=0) & (|marking(Ext_Mem_Acc_42_41)|=0) & (|marking(Ext_Mem_Acc_15_3)|=0) & (|marking(Ext_Mem_Acc_15_5)|=0) & (|marking(Ext_Mem_Acc_7_32)|=0) & (|marking(Ext_Mem_Acc_26_13)|=0) & (|marking(Ext_Mem_Acc_31_7)|=0) & (|marking(Ext_Mem_Acc_45_33)|=0) & (|marking(Ext_Mem_Acc_27_21)|=0) & (|marking(Ext_Mem_Acc_46_39)|=0) & (|marking(Ext_Mem_Acc_39_2)|=0) & (|marking(Ext_Mem_Acc_18_25)|=0) & (|marking(Ext_Mem_Acc_6_36)|=0) & (|marking(Ext_Mem_Acc_47_44)|=0) & (|marking(Ext_Mem_Acc_13_29)|=0) & (|marking(Ext_Mem_Acc_26_38)|=0) & (|marking(Ext_Mem_Acc_29_50)|=0) & (|marking(Ext_Mem_Acc_37_30)|=0) & (|marking(Ext_Mem_Acc_45_7)|=0) & (|marking(Ext_Mem_Acc_16_40)|=0) & (|marking(Ext_Mem_Acc_42_26)|=0) & (|marking(Ext_Mem_Acc_39_49)|=0) & (|marking(Ext_Mem_Acc_21_42)|=0) & (|marking(Ext_Mem_Acc_42_14)|=0) & (|marking(Ext_Mem_Acc_13_42)|=0) & (|marking(Ext_Mem_Acc_20_30)|=0) & (|marking(Ext_Mem_Acc_41_28)|=0) & (|marking(Ext_Mem_Acc_43_15)|=0) & (|marking(Ext_Mem_Acc_12_35)|=0) & (|marking(Ext_Mem_Acc_49_40)|=0) & (|marking(Ext_Mem_Acc_13_14)|=0) & (|marking(Ext_Mem_Acc_47_33)|=0) & (|marking(Ext_Mem_Acc_27_31)|=0) & (|marking(Ext_Mem_Acc_5_11)|=0) & (|marking(Ext_Mem_Acc_4_8)|=0) & (|marking(Ext_Mem_Acc_13_1)|=0) & (|marking(Ext_Mem_Acc_8_20)|=0) & (|marking(Ext_Mem_Acc_16_6)|=0) & (|marking(Ext_Mem_Acc_45_29)|=0) & (|marking(Ext_Mem_Acc_10_30)|=0) & (|marking(Ext_Mem_Acc_13_49)|=0) & (|marking(Ext_Mem_Acc_40_14)|=0) & (|marking(Ext_Mem_Acc_44_9)|=0) & (|marking(Ext_Mem_Acc_14_49)|=0) & (|marking(Ext_Mem_Acc_36_5)|=0) & (|marking(Ext_Mem_Acc_28_10)|=0) & (|marking(Ext_Mem_Acc_50_24)|=0) & (|marking(Ext_Mem_Acc_2_22)|=0) & (|marking(Ext_Mem_Acc_24_17)|=0) & (|marking(Ext_Mem_Acc_31_30)|=0) & (|marking(Ext_Mem_Acc_23_24)|=0) & (|marking(Ext_Mem_Acc_18_26)|=0) & (|marking(Ext_Mem_Acc_6_35)|=0) & (|marking(Ext_Mem_Acc_23_40)|=0) & (|marking(Ext_Mem_Acc_41_24)|=0) & (|marking(Ext_Mem_Acc_34_35)|=0) & (|marking(Ext_Mem_Acc_44_16)|=0) & (|marking(Ext_Mem_Acc_2_24)|=0) & (|marking(Ext_Mem_Acc_30_14)|=0) & (|marking(Ext_Mem_Acc_27_32)|=0) & (|marking(Ext_Mem_Acc_46_21)|=0) & (|marking(Ext_Mem_Acc_47_28)|=0) & (|marking(Ext_Mem_Acc_35_28)|=0) & (|marking(Ext_Mem_Acc_2_34)|=0) & (|marking(Ext_Mem_Acc_18_20)|=0) & (|marking(Ext_Mem_Acc_41_25)|=0) & (|marking(Ext_Mem_Acc_38_6)|=0) & (|marking(Ext_Mem_Acc_3_35)|=0) & (|marking(Ext_Mem_Acc_22_43)|=0) & (|marking(Ext_Mem_Acc_19_8)|=0) & (|marking(Ext_Mem_Acc_40_7)|=0) & (|marking(Ext_Mem_Acc_30_9)|=0) & (|marking(Ext_Mem_Acc_4_32)|=0) & (|marking(Ext_Mem_Acc_38_21)|=0) & (|marking(Ext_Mem_Acc_1_29)|=0) & (|marking(Ext_Mem_Acc_40_47)|=0) & (|marking(Ext_Mem_Acc_40_31)|=0) & (|marking(Ext_Mem_Acc_39_16)|=0) & (|marking(Ext_Mem_Acc_17_45)|=0) & (|marking(Ext_Mem_Acc_39_44)|=0) & (|marking(Ext_Mem_Acc_45_21)|=0) & (|marking(Ext_Mem_Acc_39_8)|=0) & (|marking(Ext_Mem_Acc_10_3)|=0) & (|marking(Ext_Mem_Acc_39_17)|=0) & (|marking(Ext_Mem_Acc_9_26)|=0) & (|marking(Ext_Mem_Acc_2_31)|=0) & (|marking(Ext_Mem_Acc_25_35)|=0) & (|marking(Ext_Mem_Acc_32_8)|=0) & (|marking(Ext_Mem_Acc_9_2)|=0) & (|marking(Ext_Mem_Acc_30_25)|=0) & (|marking(Ext_Mem_Acc_19_5)|=0) & (|marking(Ext_Mem_Acc_30_12)|=0) & (|marking(Ext_Mem_Acc_27_14)|=0) & (|marking(Ext_Mem_Acc_48_42)|=0) & (|marking(Ext_Mem_Acc_37_24)|=0) & (|marking(Ext_Mem_Acc_10_14)|=0) & (|marking(Ext_Mem_Acc_33_25)|=0) & (|marking(Ext_Mem_Acc_50_6)|=0) & (|marking(Ext_Mem_Acc_20_38)|=0) & (|marking(Ext_Mem_Acc_43_41)|=0) & (|marking(Ext_Mem_Acc_47_9)|=0) & (|marking(Ext_Mem_Acc_12_27)|=0) & (|marking(Ext_Mem_Acc_41_22)|=0) & (|marking(Ext_Mem_Acc_35_21)|=0) & (|marking(Ext_Mem_Acc_26_8)|=0) & (|marking(Ext_Mem_Acc_18_10)|=0) & (|marking(Ext_Mem_Acc_11_34)|=0) & (|marking(Ext_Mem_Acc_15_29)|=0) & (|marking(Ext_Mem_Acc_2_23)|=0) & (|marking(Ext_Mem_Acc_2_13)|=0) & (|marking(Ext_Mem_Acc_22_14)|=0) & (|marking(Ext_Mem_Acc_12_48)|=0) & (|marking(Ext_Mem_Acc_40_37)|=0) & (|marking(Ext_Mem_Acc_42_15)|=0) & (|marking(Ext_Mem_Acc_3_49)|=0) & (|marking(Ext_Mem_Acc_9_5)|=0) & (|marking(Ext_Mem_Acc_14_40)|=0) & (|marking(Ext_Mem_Acc_31_9)|=0) & (|marking(Ext_Mem_Acc_44_41)|=0) & (|marking(Ext_Mem_Acc_26_20)|=0) & (|marking(Ext_Mem_Acc_6_1)|=0) & (|marking(Ext_Mem_Acc_4_16)|=0) & (|marking(Ext_Mem_Acc_3_14)|=0) & (|marking(Ext_Mem_Acc_21_43)|=0) & (|marking(Ext_Mem_Acc_3_20)|=0) & (|marking(Ext_Mem_Acc_42_28)|=0) & (|marking(Ext_Mem_Acc_14_21)|=0) & (|marking(Ext_Mem_Acc_47_26)|=0) & (|marking(Ext_Mem_Acc_33_31)|=0) & (|marking(Ext_Mem_Acc_36_38)|=0) & (|marking(Ext_Mem_Acc_47_49)|=0) & (|marking(Ext_Mem_Acc_21_19)|=0) & (|marking(Ext_Mem_Acc_45_40)|=0) & (|marking(Ext_Mem_Acc_17_34)|=0) & (|marking(Ext_Mem_Acc_35_42)|=0) & (|marking(Ext_Mem_Acc_7_6)|=0) & (|marking(Ext_Mem_Acc_15_4)|=0) & (|marking(Ext_Mem_Acc_6_28)|=0) & (|marking(Ext_Mem_Acc_15_26)|=0) & (|marking(Ext_Mem_Acc_5_30)|=0) & (|marking(Ext_Mem_Acc_45_32)|=0) & (|marking(Ext_Mem_Acc_8_31)|=0) & (|marking(Ext_Mem_Acc_9_49)|=0) & (|marking(Ext_Mem_Acc_31_33)|=0) & (|marking(Ext_Mem_Acc_1_39)|=0) & (|marking(Ext_Mem_Acc_18_8)|=0) & (|marking(Ext_Mem_Acc_8_16)|=0) & (|marking(Ext_Mem_Acc_1_22)|=0) & (|marking(Ext_Mem_Acc_16_15)|=0) & (|marking(Ext_Mem_Acc_44_34)|=0) & (|marking(Ext_Mem_Acc_12_30)|=0) & (|marking(Ext_Mem_Acc_48_4)|=0) & (|marking(Ext_Mem_Acc_10_39)|=0) & (|marking(Ext_Mem_Acc_23_26)|=0) & (|marking(Ext_Mem_Acc_25_36)|=0) & (|marking(Ext_Mem_Acc_10_23)|=0) & (|marking(Ext_Mem_Acc_45_8)|=0) & (|marking(Ext_Mem_Acc_30_20)|=0) & (|marking(Ext_Mem_Acc_35_17)|=0) & (|marking(Ext_Mem_Acc_49_12)|=0) & (|marking(Ext_Mem_Acc_17_9)|=0) & (|marking(Ext_Mem_Acc_2_5)|=0) & (|marking(Ext_Mem_Acc_48_15)|=0) & (|marking(Ext_Mem_Acc_36_11)|=0) & (|marking(Ext_Mem_Acc_21_8)|=0) & (|marking(Ext_Mem_Acc_33_29)|=0) & (|marking(Ext_Mem_Acc_48_37)|=0) & (|marking(Ext_Mem_Acc_49_36)|=0) & (|marking(Ext_Mem_Acc_41_7)|=0) & (|marking(Ext_Mem_Acc_23_31)|=0) & (|marking(Ext_Mem_Acc_5_27)|=0) & (|marking(Ext_Mem_Acc_29_19)|=0) & (|marking(Ext_Mem_Acc_50_45)|=0) & (|marking(Ext_Mem_Acc_29_42)|=0) & (|marking(Ext_Mem_Acc_50_30)|=0) & (|marking(Ext_Mem_Acc_20_34)|=0) & (|marking(Ext_Mem_Acc_47_50)|=0) & (|marking(Ext_Mem_Acc_38_13)|=0) & (|marking(Ext_Mem_Acc_37_45)|=0) & (|marking(Ext_Mem_Acc_22_49)|=0) & (|marking(Ext_Mem_Acc_47_46)|=0) & (|marking(Ext_Mem_Acc_49_10)|=0) & (|marking(Ext_Mem_Acc_33_42)|=0) & (|marking(Ext_Mem_Acc_29_41)|=0) & (|marking(Ext_Mem_Acc_45_18)|=0) & (|marking(Ext_Mem_Acc_10_16)|=0) & (|marking(Ext_Mem_Acc_7_1)|=0) & (|marking(Ext_Mem_Acc_24_39)|=0) & (|marking(Ext_Mem_Acc_14_37)|=0) & (|marking(Ext_Mem_Acc_34_49)|=0) & (|marking(Ext_Mem_Acc_42_10)|=0) & (|marking(Ext_Mem_Acc_32_43)|=0) & (|marking(Ext_Mem_Acc_50_27)|=0) & (|marking(Ext_Mem_Acc_31_40)|=0) & (|marking(Ext_Mem_Acc_4_43)|=0) & (|marking(Ext_Mem_Acc_14_19)|=0) & (|marking(Ext_Mem_Acc_33_27)|=0) & (|marking(Ext_Mem_Acc_5_16)|=0) & (|marking(Ext_Mem_Acc_13_6)|=0) & (|marking(Ext_Mem_Acc_25_27)|=0) & (|marking(Ext_Mem_Acc_9_31)|=0) & (|marking(Ext_Mem_Acc_33_19)|=0) & (|marking(Ext_Mem_Acc_27_3)|=0) & (|marking(Ext_Mem_Acc_10_4)|=0) & (|marking(Ext_Mem_Acc_10_24)|=0) & (|marking(Ext_Mem_Acc_31_48)|=0) & (|marking(Ext_Mem_Acc_12_36)|=0) & (|marking(Ext_Mem_Acc_3_18)|=0) & (|marking(Ext_Mem_Acc_24_1)|=0) & (|marking(Ext_Mem_Acc_35_20)|=0) & (|marking(Ext_Mem_Acc_49_39)|=0) & (|marking(Ext_Mem_Acc_29_23)|=0) & (|marking(Ext_Mem_Acc_18_14)|=0) & (|marking(Ext_Mem_Acc_45_22)|=0) & (|marking(Ext_Mem_Acc_7_11)|=0) & (|marking(Ext_Mem_Acc_5_33)|=0) & (|marking(Ext_Mem_Acc_44_19)|=0) & (|marking(Ext_Mem_Acc_46_7)|=0) & (|marking(Ext_Mem_Acc_39_7)|=0) & (|marking(Ext_Mem_Acc_10_44)|=0) & (|marking(Ext_Mem_Acc_36_47)|=0) & (|marking(Ext_Mem_Acc_43_49)|=0) & (|marking(Ext_Mem_Acc_17_46)|=0) & (|marking(Ext_Mem_Acc_41_29)|=0) & (|marking(Ext_Mem_Acc_41_49)|=0) & (|marking(Ext_Mem_Acc_4_29)|=0) & (|marking(Ext_Mem_Acc_3_31)|=0) & (|marking(Ext_Mem_Acc_29_15)|=0) & (|marking(Ext_Mem_Acc_26_45)|=0) & (|marking(Ext_Mem_Acc_34_48)|=0) & (|marking(Ext_Mem_Acc_38_18)|=0) & (|marking(Ext_Mem_Acc_32_2)|=0) & (|marking(Ext_Mem_Acc_10_17)|=0) & (|marking(Ext_Mem_Acc_44_14)|=0) & (|marking(Ext_Mem_Acc_18_17)|=0) & (|marking(Ext_Mem_Acc_27_23)|=0) & (|marking(Ext_Mem_Acc_5_14)|=0) & (|marking(Ext_Mem_Acc_33_6)|=0) & (|marking(Ext_Mem_Acc_7_49)|=0) & (|marking(Ext_Mem_Acc_28_5)|=0) & (|marking(Ext_Mem_Acc_6_34)|=0) & (|marking(Ext_Mem_Acc_22_47)|=0) & (|marking(Ext_Mem_Acc_43_10)|=0) & (|marking(Ext_Mem_Acc_13_9)|=0) & (|marking(Ext_Mem_Acc_10_31)|=0) & (|marking(Ext_Mem_Acc_20_32)|=0) & (|marking(Ext_Mem_Acc_20_41)|=0) & (|marking(Ext_Mem_Acc_5_4)|=0) & (|marking(Ext_Mem_Acc_46_50)|=0) & (|marking(Ext_Mem_Acc_21_22)|=0) & (|marking(Ext_Mem_Acc_42_40)|=0) & (|marking(Ext_Mem_Acc_17_8)|=0) & (|marking(Ext_Mem_Acc_35_24)|=0) & (|marking(Ext_Mem_Acc_45_3)|=0) & (|marking(Ext_Mem_Acc_46_25)|=0) & (|marking(Ext_Mem_Acc_12_40)|=0) & (|marking(Ext_Mem_Acc_35_3)|=0) & (|marking(Ext_Mem_Acc_12_24)|=0) & (|marking(Ext_Mem_Acc_35_31)|=0) & (|marking(Ext_Mem_Acc_19_12)|=0) & (|marking(Ext_Mem_Acc_49_4)|=0) & (|marking(Ext_Mem_Acc_41_10)|=0) & (|marking(Ext_Mem_Acc_37_12)|=0) & (|marking(Ext_Mem_Acc_11_28)|=0) & (|marking(Ext_Mem_Acc_10_19)|=0) & (|marking(Ext_Mem_Acc_13_2)|=0) & (|marking(Ext_Mem_Acc_12_16)|=0) & (|marking(Ext_Mem_Acc_31_42)|=0) & (|marking(Ext_Mem_Acc_16_23)|=0) & (|marking(Ext_Mem_Acc_23_42)|=0) & (|marking(Ext_Mem_Acc_50_39)|=0) & (|marking(Ext_Mem_Acc_40_42)|=0) & (|marking(Ext_Mem_Acc_4_26)|=0) & (|marking(Ext_Mem_Acc_34_43)|=0) & (|marking(Ext_Mem_Acc_11_40)|=0) & (|marking(Ext_Mem_Acc_33_32)|=0) & (|marking(Ext_Mem_Acc_15_18)|=0) & (|marking(Ext_Mem_Acc_10_8)|=0) & (|marking(Ext_Mem_Acc_22_39)|=0) & (|marking(Ext_Mem_Acc_27_44)|=0) & (|marking(Ext_Mem_Acc_5_32)|=0) & (|marking(Ext_Mem_Acc_38_36)|=0) & (|marking(Ext_Mem_Acc_40_10)|=0) & (|marking(Ext_Mem_Acc_19_3)|=0) & (|marking(Ext_Mem_Acc_16_39)|=0) & (|marking(Ext_Mem_Acc_20_47)|=0) & (|marking(Ext_Mem_Acc_17_12)|=0) & (|marking(Ext_Mem_Acc_48_3)|=0) & (|marking(Ext_Mem_Acc_23_9)|=0) & (|marking(Ext_Mem_Acc_39_35)|=0) & (|marking(Ext_Mem_Acc_37_3)|=0) & (|marking(Ext_Mem_Acc_16_43)|=0) & (|marking(Ext_Mem_Acc_42_38)|=0) & (|marking(Ext_Mem_Acc_33_50)|=0) & (|marking(Ext_Mem_Acc_10_13)|=0) & (|marking(Ext_Mem_Acc_28_26)|=0) & (|marking(Ext_Mem_Acc_17_37)|=0) & (|marking(Ext_Mem_Acc_11_47)|=0) & (|marking(Ext_Mem_Acc_13_19)|=0) & (|marking(Ext_Mem_Acc_34_3)|=0) & (|marking(Ext_Mem_Acc_15_22)|=0) & (|marking(Ext_Mem_Acc_41_35)|=0) & (|marking(Ext_Mem_Acc_43_7)|=0) & (|marking(Ext_Mem_Acc_27_39)|=0) & (|marking(Ext_Mem_Acc_34_38)|=0) & (|marking(Ext_Mem_Acc_12_20)|=0) & (|marking(Ext_Mem_Acc_24_23)|=0) & (|marking(Ext_Mem_Acc_5_18)|=0) & (|marking(Ext_Mem_Acc_31_37)|=0) & (|marking(Ext_Mem_Acc_4_23)|=0) & (|marking(Ext_Mem_Acc_34_4)|=0) & (|marking(Ext_Mem_Acc_35_8)|=0) & (|marking(Ext_Mem_Acc_21_13)|=0) & (|marking(Ext_Mem_Acc_11_50)|=0) & (|marking(Ext_Mem_Acc_11_12)|=0) & (|marking(Ext_Mem_Acc_42_16)|=0) & (|marking(Ext_Mem_Acc_15_38)|=0) & (|marking(Ext_Mem_Acc_44_27)|=0) & (|marking(Ext_Mem_Acc_43_16)|=0) & (|marking(Ext_Mem_Acc_42_24)|=0) & (|marking(Ext_Mem_Acc_43_46)|=0) & (|marking(Ext_Mem_Acc_15_32)|=0) & (|marking(Ext_Mem_Acc_8_42)|=0) & (|marking(Ext_Mem_Acc_34_36)|=0) & (|marking(Ext_Mem_Acc_9_38)|=0) & (|marking(Ext_Mem_Acc_50_36)|=0) & (|marking(Ext_Mem_Acc_16_14)|=0) & (|marking(Ext_Mem_Acc_43_12)|=0) & (|marking(Ext_Mem_Acc_39_9)|=0) & (|marking(Ext_Mem_Acc_10_45)|=0) & (|marking(Ext_Mem_Acc_38_7)|=0) & (|marking(Ext_Mem_Acc_49_18)|=0) & (|marking(Ext_Mem_Acc_26_36)|=0) & (|marking(Ext_Mem_Acc_45_4)|=0) & (|marking(Ext_Mem_Acc_10_1)|=0) & (|marking(Ext_Mem_Acc_28_14)|=0) & (|marking(Ext_Mem_Acc_11_32)|=0) & (|marking(Ext_Mem_Acc_48_5)|=0) & (|marking(Ext_Mem_Acc_44_10)|=0) & (|marking(Ext_Mem_Acc_12_37)|=0) & (|marking(Ext_Mem_Acc_7_46)|=0) & (|marking(Ext_Mem_Acc_16_3)|=0) & (|marking(Ext_Mem_Acc_45_38)|=0) & (|marking(Ext_Mem_Acc_47_18)|=0) & (|marking(Ext_Mem_Acc_37_19)|=0) & (|marking(Ext_Mem_Acc_31_26)|=0) & (|marking(Ext_Mem_Acc_1_2)|=0) & (|marking(Ext_Mem_Acc_9_30)|=0) & (|marking(Ext_Mem_Acc_40_35)|=0) & (|marking(Ext_Mem_Acc_19_39)|=0) & (|marking(Ext_Mem_Acc_37_11)|=0) & (|marking(Ext_Mem_Acc_17_25)|=0) & (|marking(Ext_Mem_Acc_22_15)|=0) & (|marking(Ext_Mem_Acc_25_19)|=0) & (|marking(Ext_Mem_Acc_39_45)|=0) & (|marking(Ext_Mem_Acc_21_47)|=0) & (|marking(Ext_Mem_Acc_15_40)|=0) & (|marking(Ext_Mem_Acc_33_30)|=0) & (|marking(Ext_Mem_Acc_39_40)|=0) & (|marking(Ext_Mem_Acc_30_36)|=0) & (|marking(Ext_Mem_Acc_26_22)|=0) & (|marking(Ext_Mem_Acc_50_9)|=0) & (|marking(Ext_Mem_Acc_34_21)|=0) & (|marking(Ext_Mem_Acc_28_9)|=0) & (|marking(Ext_Mem_Acc_4_7)|=0) & (|marking(Ext_Mem_Acc_22_8)|=0) & (|marking(Ext_Mem_Acc_29_12)|=0) & (|marking(Ext_Mem_Acc_26_41)|=0) & (|marking(Ext_Mem_Acc_11_18)|=0) & (|marking(Ext_Mem_Acc_17_20)|=0) & (|marking(Ext_Mem_Acc_28_20)|=0) & (|marking(Ext_Mem_Acc_4_20)|=0) & (|marking(Ext_Mem_Acc_44_30)|=0) & (|marking(Ext_Mem_Acc_5_31)|=0) & (|marking(Ext_Mem_Acc_32_40)|=0) & (|marking(Ext_Mem_Acc_9_23)|=0) & (|marking(Ext_Mem_Acc_6_45)|=0) & (|marking(Ext_Mem_Acc_5_8)|=0) & (|marking(Ext_Mem_Acc_20_46)|=0) & (|marking(Ext_Mem_Acc_14_16)|=0) & (|marking(Ext_Mem_Acc_3_25)|=0) & (|marking(Ext_Mem_Acc_30_10)|=0) & (|marking(Ext_Mem_Acc_9_37)|=0) & (|marking(Ext_Mem_Acc_19_1)|=0) & (|marking(Ext_Mem_Acc_21_30)|=0) & (|marking(Ext_Mem_Acc_46_44)|=0) & (|marking(Ext_Mem_Acc_15_48)|=0) & (|marking(Ext_Mem_Acc_49_9)|=0) & (|marking(Ext_Mem_Acc_44_49)|=0) & (|marking(Ext_Mem_Acc_4_21)|=0) & (|marking(Ext_Mem_Acc_38_35)|=0) & (|marking(Ext_Mem_Acc_30_22)|=0) & (|marking(Ext_Mem_Acc_36_37)|=0) & (|marking(Ext_Mem_Acc_30_16)|=0) & (|marking(Ext_Mem_Acc_17_23)|=0) & (|marking(Ext_Mem_Acc_18_36)|=0) & (|marking(Ext_Mem_Acc_21_6)|=0) & (|marking(Ext_Mem_Acc_29_48)|=0) & (|marking(Ext_Mem_Acc_3_46)|=0) & (|marking(Ext_Mem_Acc_8_5)|=0) & (|marking(Ext_Mem_Acc_43_47)|=0) & (|marking(Ext_Mem_Acc_35_32)|=0) & (|marking(Ext_Mem_Acc_18_49)|=0) & (|marking(Ext_Mem_Acc_23_43)|=0) & (|marking(Ext_Mem_Acc_20_9)|=0) & (|marking(Ext_Mem_Acc_8_45)|=0) & (|marking(Ext_Mem_Acc_24_33)|=0) & (|marking(Ext_Mem_Acc_4_47)|=0) & (|marking(Ext_Mem_Acc_40_8)|=0) & (|marking(Ext_Mem_Acc_26_28)|=0) & (|marking(Ext_Mem_Acc_29_22)|=0) & (|marking(Ext_Mem_Acc_49_33)|=0) & (|marking(Ext_Mem_Acc_28_40)|=0) & (|marking(Ext_Mem_Acc_46_29)|=0) & (|marking(Ext_Mem_Acc_28_39)|=0) & (|marking(Ext_Mem_Acc_46_28)|=0) & (|marking(Ext_Mem_Acc_31_38)|=0) & (|marking(Ext_Mem_Acc_43_17)|=0) & (|marking(Ext_Mem_Acc_6_20)|=0) & (|marking(Ext_Mem_Acc_20_3)|=0) & (|marking(Ext_Mem_Acc_14_17)|=0) & (|marking(Ext_Mem_Acc_46_8)|=0) & (|marking(Ext_Mem_Acc_29_36)|=0) & (|marking(Ext_Mem_Acc_47_8)|=0) & (|marking(Ext_Mem_Acc_1_28)|=0) & (|marking(Ext_Mem_Acc_22_23)|=0) & (|marking(Ext_Mem_Acc_33_11)|=0) & (|marking(Ext_Mem_Acc_34_17)|=0) & (|marking(Ext_Mem_Acc_26_37)|=0) & (|marking(Ext_Mem_Acc_37_50)|=0) & (|marking(Ext_Mem_Acc_44_17)|=0) & (|marking(Ext_Mem_Acc_33_17)|=0) & (|marking(Ext_Mem_Acc_26_35)|=0) & (|marking(Ext_Mem_Acc_35_10)|=0) & (|marking(Ext_Mem_Acc_25_18)|=0) & (|marking(Ext_Mem_Acc_15_33)|=0) & (|marking(Ext_Mem_Acc_28_32)|=0) & (|marking(Ext_Mem_Acc_28_33)|=0) & (|marking(Ext_Mem_Acc_30_6)|=0) & (|marking(Ext_Mem_Acc_30_48)|=0) & (|marking(Ext_Mem_Acc_49_16)|=0) & (|marking(Ext_Mem_Acc_22_21)|=0) & (|marking(Ext_Mem_Acc_35_27)|=0) & (|marking(Ext_Mem_Acc_24_19)|=0) & (|marking(Ext_Mem_Acc_42_25)|=0) & (|marking(Ext_Mem_Acc_44_37)|=0) & (|marking(Ext_Mem_Acc_37_28)|=0) & (|marking(Ext_Mem_Acc_47_48)|=0) & (|marking(Ext_Mem_Acc_43_31)|=0) & (|marking(Ext_Mem_Acc_22_42)|=0) & (|marking(Ext_Mem_Acc_4_37)|=0) & (|marking(Ext_Mem_Acc_15_34)|=0) & (|marking(Ext_Mem_Acc_44_46)|=0) & (|marking(Ext_Mem_Acc_50_1)|=0) & (|marking(Ext_Mem_Acc_2_37)|=0) & (|marking(Ext_Mem_Acc_20_26)|=0) & (|marking(Ext_Mem_Acc_21_29)|=0) & (|marking(Ext_Mem_Acc_21_26)|=0) & (|marking(Ext_Mem_Acc_49_30)|=0) & (|marking(Ext_Mem_Acc_8_47)|=0) & (|marking(Ext_Mem_Acc_38_4)|=0) & (|marking(Ext_Mem_Acc_44_4)|=0) & (|marking(Ext_Mem_Acc_8_17)|=0) & (|marking(Ext_Mem_Acc_36_2)|=0) & (|marking(Ext_Mem_Acc_20_13)|=0) & (|marking(Ext_Mem_Acc_10_29)|=0) & (|marking(Ext_Mem_Acc_42_27)|=0) & (|marking(Ext_Mem_Acc_47_38)|=0) & (|marking(Ext_Mem_Acc_44_23)|=0) & (|marking(Ext_Mem_Acc_3_12)|=0) & (|marking(Ext_Mem_Acc_7_25)|=0) & (|marking(Ext_Mem_Acc_12_34)|=0) & (|marking(Ext_Mem_Acc_50_10)|=0) & (|marking(Ext_Mem_Acc_47_39)|=0) & (|marking(Ext_Mem_Acc_4_28)|=0) & (|marking(Ext_Mem_Acc_1_8)|=0) & (|marking(Ext_Mem_Acc_42_20)|=0) & (|marking(Ext_Mem_Acc_43_26)|=0) & (|marking(Ext_Mem_Acc_46_11)|=0) & (|marking(Ext_Mem_Acc_23_27)|=0) & (|marking(Ext_Mem_Acc_27_15)|=0) & (|marking(Ext_Mem_Acc_1_4)|=0) & (|marking(Ext_Mem_Acc_11_30)|=0) & (|marking(Ext_Mem_Acc_26_6)|=0) & (|marking(Ext_Mem_Acc_49_31)|=0) & (|marking(Ext_Mem_Acc_10_6)|=0) & (|marking(Ext_Mem_Acc_10_38)|=0) & (|marking(Ext_Mem_Acc_33_34)|=0) & (|marking(Ext_Mem_Acc_4_14)|=0) & (|marking(Ext_Mem_Acc_2_26)|=0) & (|marking(Ext_Mem_Acc_1_30)|=0) & (|marking(Ext_Mem_Acc_34_23)|=0) & (|marking(Ext_Mem_Acc_18_41)|=0) & (|marking(Ext_Mem_Acc_31_6)|=0) & (|marking(Ext_Mem_Acc_27_9)|=0) & (|marking(Ext_Mem_Acc_42_7)|=0) & (|marking(Ext_Mem_Acc_6_9)|=0) & (|marking(Ext_Mem_Acc_42_8)|=0) & (|marking(Ext_Mem_Acc_46_47)|=0) & (|marking(Ext_Mem_Acc_20_28)|=0) & (|marking(Ext_Mem_Acc_22_10)|=0) & (|marking(Ext_Mem_Acc_16_22)|=0) & (|marking(Ext_Mem_Acc_9_19)|=0) & (|marking(Ext_Mem_Acc_21_18)|=0) & (|marking(Ext_Mem_Acc_20_29)|=0) & (|marking(Ext_Mem_Acc_1_50)|=0) & (|marking(Ext_Mem_Acc_44_6)|=0) & (|marking(Ext_Mem_Acc_38_22)|=0) & (|marking(Ext_Mem_Acc_13_44)|=0) & (|marking(Ext_Mem_Acc_40_36)|=0) & (|marking(Ext_Mem_Acc_8_37)|=0) & (|marking(Ext_Mem_Acc_34_41)|=0) & (|marking(Ext_Mem_Acc_38_40)|=0) & (|marking(Ext_Mem_Acc_9_13)|=0) & (|marking(Ext_Mem_Acc_45_25)|=0) & (|marking(Ext_Mem_Acc_23_22)|=0) & (|marking(Ext_Mem_Acc_37_43)|=0) & (|marking(Ext_Mem_Acc_35_38)|=0) & (|marking(Ext_Mem_Acc_15_46)|=0) & (|marking(Ext_Mem_Acc_26_18)|=0) & (|marking(Ext_Mem_Acc_10_7)|=0) & (|marking(Ext_Mem_Acc_10_33)|=0) & (|marking(Ext_Mem_Acc_49_21)|=0) & (|marking(Ext_Mem_Acc_15_27)|=0) & (|marking(Ext_Mem_Acc_31_24)|=0) & (|marking(Ext_Mem_Acc_18_24)|=0) & (|marking(Ext_Mem_Acc_11_9)|=0) & (|marking(Ext_Mem_Acc_43_29)|=0) & (|marking(Ext_Mem_Acc_30_23)|=0) & (|marking(Ext_Mem_Acc_1_20)|=0) & (|marking(Ext_Mem_Acc_22_13)|=0) & (|marking(Ext_Mem_Acc_16_9)|=0) & (|marking(Ext_Mem_Acc_7_38)|=0) & (|marking(Ext_Mem_Acc_6_3)|=0) & (|marking(Ext_Mem_Acc_41_43)|=0) & (|marking(Ext_Mem_Acc_5_41)|=0) & (|marking(Ext_Mem_Acc_34_26)|=0) & (|marking(Ext_Mem_Acc_25_17)|=0) & (|marking(Ext_Mem_Acc_21_40)|=0) & (|marking(Ext_Mem_Acc_30_38)|=0) & (|marking(Ext_Mem_Acc_11_26)|=0) & (|marking(Ext_Mem_Acc_48_22)|=0) & (|marking(Ext_Mem_Acc_7_23)|=0) & (|marking(Ext_Mem_Acc_46_9)|=0) & (|marking(Ext_Mem_Acc_31_50)|=0) & (|marking(Ext_Mem_Acc_47_15)|=0) & (|marking(Ext_Mem_Acc_7_37)|=0) & (|marking(Ext_Mem_Acc_5_35)|=0) & (|marking(Ext_Mem_Acc_41_31)|=0) & (|marking(Ext_Mem_Acc_10_50)|=0) & (|marking(Ext_Mem_Acc_5_7)|=0) & (|marking(Ext_Mem_Acc_37_44)|=0) & (|marking(Ext_Mem_Acc_36_21)|=0) & (|marking(Ext_Mem_Acc_12_1)|=0) & (|marking(Ext_Mem_Acc_37_39)|=0) & (|marking(Ext_Mem_Acc_47_31)|=0) & (|marking(Ext_Mem_Acc_7_10)|=0) & (|marking(Ext_Mem_Acc_5_43)|=0) & (|marking(Ext_Mem_Acc_39_12)|=0) & (|marking(Ext_Mem_Acc_3_5)|=0) & (|marking(Ext_Mem_Acc_30_13)|=0) & (|marking(Ext_Mem_Acc_23_20)|=0) & (|marking(Ext_Mem_Acc_7_9)|=0) & (|marking(Ext_Mem_Acc_29_17)|=0) & (|marking(Ext_Mem_Acc_26_50)|=0) & (|marking(Ext_Mem_Acc_36_24)|=0) & (|marking(Ext_Mem_Acc_32_22)|=0) & (|marking(Ext_Mem_Acc_50_28)|=0) & (|marking(Ext_Mem_Acc_15_8)|=0) & (|marking(Ext_Mem_Acc_8_12)|=0) & (|marking(Ext_Mem_Acc_27_50)|=0) & (|marking(Ext_Mem_Acc_36_39)|=0) & (|marking(Ext_Mem_Acc_12_7)|=0) & (|marking(Ext_Mem_Acc_12_19)|=0) & (|marking(Ext_Mem_Acc_35_15)|=0) & (|marking(Ext_Mem_Acc_14_43)|=0) & (|marking(Ext_Mem_Acc_50_42)|=0) & (|marking(Ext_Mem_Acc_15_2)|=0) & (|marking(Ext_Mem_Acc_18_3)|=0) & (|marking(Ext_Mem_Acc_36_22)|=0) & (|marking(Ext_Mem_Acc_35_25)|=0) & (|marking(Ext_Mem_Acc_36_49)|=0) & (|marking(Ext_Mem_Acc_34_19)|=0) & (|marking(Ext_Mem_Acc_22_36)|=0) & (|marking(Ext_Mem_Acc_12_38)|=0) & (|marking(Ext_Mem_Acc_39_31)|=0) & (|marking(Ext_Mem_Acc_29_14)|=0) & (|marking(Ext_Mem_Acc_46_30)|=0) & (|marking(Ext_Mem_Acc_17_18)|=0) & (|marking(Ext_Mem_Acc_42_1)|=0) & (|marking(Ext_Mem_Acc_18_29)|=0) & (|marking(Ext_Mem_Acc_10_12)|=0) & (|marking(Ext_Mem_Acc_6_12)|=0) & (|marking(Ext_Mem_Acc_37_33)|=0) & (|marking(Ext_Mem_Acc_24_8)|=0) & (|marking(Ext_Mem_Acc_23_10)|=0) & (|marking(Ext_Mem_Acc_31_41)|=0) & (|marking(Ext_Mem_Acc_36_40)|=0) & (|marking(Ext_Mem_Acc_1_12)|=0) & (|marking(Ext_Mem_Acc_30_17)|=0) & (|marking(Ext_Mem_Acc_46_42)|=0) & (|marking(Ext_Mem_Acc_18_1)|=0) & (|marking(Ext_Mem_Acc_22_5)|=0) & (|marking(Ext_Mem_Acc_8_26)|=0) & (|marking(Ext_Mem_Acc_16_1)|=0) & (|marking(Ext_Mem_Acc_28_31)|=0) & (|marking(Ext_Mem_Acc_4_13)|=0) & (|marking(Ext_Mem_Acc_40_26)|=0) & (|marking(Ext_Mem_Acc_21_41)|=0) & (|marking(Ext_Mem_Acc_25_8)|=0) & (|marking(Ext_Mem_Acc_40_18)|=0) & (|marking(Ext_Mem_Acc_50_26)|=0) & (|marking(Ext_Mem_Acc_7_14)|=0) & (|marking(Ext_Mem_Acc_15_1)|=0) & (|marking(Ext_Mem_Acc_45_20)|=0) & (|marking(Ext_Mem_Acc_3_1)|=0) & (|marking(Ext_Mem_Acc_48_50)|=0) & (|marking(Ext_Mem_Acc_12_44)|=0) & (|marking(Ext_Mem_Acc_1_14)|=0) & (|marking(Ext_Mem_Acc_28_17)|=0) & (|marking(Ext_Mem_Acc_42_29)|=0) & (|marking(Ext_Mem_Acc_24_27)|=0) & (|marking(Ext_Mem_Acc_48_34)|=0) & (|marking(Ext_Mem_Acc_39_20)|=0) & (|marking(Ext_Mem_Acc_41_18)|=0) & (|marking(Ext_Mem_Acc_37_14)|=0) & (|marking(Ext_Mem_Acc_19_11)|=0) & (|marking(Ext_Mem_Acc_39_10)|=0) & (|marking(Ext_Mem_Acc_37_36)|=0) & (|marking(Ext_Mem_Acc_36_14)|=0) & (|marking(Ext_Mem_Acc_50_14)|=0) & (|marking(Ext_Mem_Acc_38_19)|=0) & (|marking(Ext_Mem_Acc_32_1)|=0) & (|marking(Ext_Mem_Acc_28_6)|=0) & (|marking(Ext_Mem_Acc_36_27)|=0) & (|marking(Ext_Mem_Acc_41_32)|=0) & (|marking(Ext_Mem_Acc_31_14)|=0) & (|marking(Ext_Mem_Acc_25_41)|=0) & (|marking(Ext_Mem_Acc_32_39)|=0) & (|marking(Ext_Mem_Acc_26_49)|=0) & (|marking(Ext_Mem_Acc_31_28)|=0) & (|marking(Ext_Mem_Acc_24_35)|=0) & (|marking(Ext_Mem_Acc_8_33)|=0) & (|marking(Ext_Mem_Acc_8_48)|=0) & (|marking(Ext_Mem_Acc_20_8)|=0) & (|marking(Ext_Mem_Acc_10_28)|=0) & (|marking(Ext_Mem_Acc_44_20)|=0) & (|marking(Ext_Mem_Acc_40_13)|=0) & (|marking(Ext_Mem_Acc_40_32)|=0) & (|marking(Ext_Mem_Acc_28_27)|=0) & (|marking(Ext_Mem_Acc_15_43)|=0) & (|marking(Ext_Mem_Acc_48_43)|=0) & (|marking(Ext_Mem_Acc_1_15)|=0) & (|marking(Ext_Mem_Acc_11_22)|=0) & (|marking(Ext_Mem_Acc_31_13)|=0) & (|marking(Ext_Mem_Acc_28_41)|=0) & (|marking(Ext_Mem_Acc_31_20)|=0) & (|marking(Ext_Mem_Acc_27_28)|=0) & (|marking(Ext_Mem_Acc_28_50)|=0) & (|marking(Ext_Mem_Acc_27_24)|=0) & (|marking(Ext_Mem_Acc_36_35)|=0) & (|marking(Ext_Mem_Acc_47_11)|=0) & (|marking(Ext_Mem_Acc_5_38)|=0) & (|marking(Ext_Mem_Acc_4_25)|=0) & (|marking(Ext_Mem_Acc_46_5)|=0) & (|marking(Ext_Mem_Acc_49_41)|=0) & (|marking(Ext_Mem_Acc_25_14)|=0) & (|marking(Ext_Mem_Acc_35_34)|=0) & (|marking(Ext_Mem_Acc_11_1)|=0) & (|marking(Ext_Mem_Acc_19_42)|=0) & (|marking(Ext_Mem_Acc_1_7)|=0) & (|marking(Ext_Mem_Acc_19_50)|=0) & (|marking(Ext_Mem_Acc_7_33)|=0) & (|marking(Ext_Mem_Acc_42_12)|=0) & (|marking(Ext_Mem_Acc_46_20)|=0) & (|marking(Ext_Mem_Acc_43_38)|=0) & (|marking(Ext_Mem_Acc_29_8)|=0) & (|marking(Ext_Mem_Acc_22_44)|=0) & (|marking(Ext_Mem_Acc_19_22)|=0) & (|marking(Ext_Mem_Acc_27_1)|=0) & (|marking(Ext_Mem_Acc_44_5)|=0) & (|marking(Ext_Mem_Acc_20_12)|=0) & (|marking(Ext_Mem_Acc_40_33)|=0) & (|marking(Ext_Mem_Acc_47_3)|=0) & (|marking(Ext_Mem_Acc_50_33)|=0) & (|marking(Ext_Mem_Acc_33_24)|=0) & (|marking(Ext_Mem_Acc_16_30)|=0) & (|marking(Ext_Mem_Acc_21_3)|=0) & (|marking(Ext_Mem_Acc_16_37)|=0) & (|marking(Ext_Mem_Acc_37_10)|=0) & (|marking(Ext_Mem_Acc_19_14)|=0) & (|marking(Ext_Mem_Acc_27_30)|=0) & (|marking(Ext_Mem_Acc_26_31)|=0) & (|marking(Ext_Mem_Acc_4_49)|=0) & (|marking(Ext_Mem_Acc_13_7)|=0) & (|marking(Ext_Mem_Acc_13_31)|=0) & (|marking(Ext_Mem_Acc_32_44)|=0) & (|marking(Ext_Mem_Acc_1_49)|=0) & (|marking(Ext_Mem_Acc_6_32)|=0) & (|marking(Ext_Mem_Acc_23_11)|=0) & (|marking(Ext_Mem_Acc_32_34)|=0) & (|marking(Ext_Mem_Acc_45_12)|=0) & (|marking(Ext_Mem_Acc_25_48)|=0) & (|marking(Ext_Mem_Acc_14_30)|=0) & (|marking(Ext_Mem_Acc_30_40)|=0) & (|marking(Ext_Mem_Acc_31_2)|=0) & (|marking(Ext_Mem_Acc_43_32)|=0) & (|marking(Ext_Mem_Acc_24_14)|=0) & (|marking(Ext_Mem_Acc_3_10)|=0) & (|marking(Ext_Mem_Acc_44_39)|=0) & (|marking(Ext_Mem_Acc_49_37)|=0) & (|marking(Ext_Mem_Acc_15_13)|=0) & (|marking(Ext_Mem_Acc_18_45)|=0) & (|marking(Ext_Mem_Acc_32_23)|=0) & (|marking(Ext_Mem_Acc_28_13)|=0) & (|marking(Ext_Mem_Acc_32_6)|=0) & (|marking(Ext_Mem_Acc_26_9)|=0) & (|marking(Ext_Mem_Acc_43_5)|=0) & (|marking(Ext_Mem_Acc_9_43)|=0) & (|marking(Ext_Mem_Acc_29_25)|=0) & (|marking(Ext_Mem_Acc_14_22)|=0) & (|marking(Ext_Mem_Acc_34_24)|=0) & (|marking(Ext_Mem_Acc_28_19)|=0) & (|marking(Ext_Mem_Acc_19_38)|=0) & (|marking(Ext_Mem_Acc_42_3)|=0) & (|marking(Ext_Mem_Acc_4_41)|=0) & (|marking(Ext_Mem_Acc_3_27)|=0) & (|marking(Ext_Mem_Acc_38_27)|=0) & (|marking(Ext_Mem_Acc_12_6)|=0) & (|marking(Ext_Mem_Acc_27_49)|=0) & (|marking(Ext_Mem_Acc_39_47)|=0) & (|marking(Ext_Mem_Acc_13_45)|=0) & (|marking(Ext_Mem_Acc_30_7)|=0) & (|marking(Ext_Mem_Acc_15_41)|=0) & (|marking(Ext_Mem_Acc_26_10)|=0) & (|marking(Ext_Mem_Acc_35_22)|=0) & (|marking(Ext_Mem_Acc_11_3)|=0) & (|marking(Ext_Mem_Acc_6_14)|=0) & (|marking(Ext_Mem_Acc_14_38)|=0) & (|marking(Ext_Mem_Acc_31_35)|=0) & (|marking(Ext_Mem_Acc_49_38)|=0) & (|marking(Ext_Mem_Acc_33_28)|=0) & (|marking(Ext_Mem_Acc_37_26)|=0) & (|marking(Ext_Mem_Acc_20_48)|=0) & (|marking(Ext_Mem_Acc_14_39)|=0) & (|marking(Ext_Mem_Acc_33_1)|=0) & (|marking(Ext_Mem_Acc_20_18)|=0) & (|marking(Ext_Mem_Acc_2_41)|=0) & (|marking(Ext_Mem_Acc_13_47)|=0) & (|marking(Ext_Mem_Acc_23_28)|=0) & (|marking(Ext_Mem_Acc_47_29)|=0) & (|marking(Ext_Mem_Acc_2_17)|=0) & (|marking(Ext_Mem_Acc_47_27)|=0) & (|marking(Ext_Mem_Acc_43_28)|=0) & (|marking(Ext_Mem_Acc_5_12)|=0) & (|marking(Ext_Mem_Acc_18_31)|=0) & (|marking(Ext_Mem_Acc_24_26)|=0) & (|marking(Ext_Mem_Acc_45_5)|=0) & (|marking(Ext_Mem_Acc_44_11)|=0) & (|marking(Ext_Mem_Acc_46_19)|=0) & (|marking(Ext_Mem_Acc_10_49)|=0) & (|marking(Ext_Mem_Acc_32_11)|=0) & (|marking(Ext_Mem_Acc_29_13)|=0) & (|marking(Ext_Mem_Acc_3_28)|=0) & (|marking(Ext_Mem_Acc_14_36)|=0) & (|marking(Ext_Mem_Acc_21_15)|=0) & (|marking(Ext_Mem_Acc_43_11)|=0) & (|marking(Ext_Mem_Acc_2_19)|=0) & (|marking(Ext_Mem_Acc_10_46)|=0) & (|marking(Ext_Mem_Acc_14_3)|=0) & (|marking(Ext_Mem_Acc_33_2)|=0) & (|marking(Ext_Mem_Acc_18_9)|=0) & (|marking(Ext_Mem_Acc_19_10)|=0) & (|marking(Ext_Mem_Acc_8_9)|=0) & (|marking(Ext_Mem_Acc_36_15)|=0) & (|marking(Ext_Mem_Acc_19_23)|=0) & (|marking(Ext_Mem_Acc_38_37)|=0) & (|marking(Ext_Mem_Acc_6_21)|=0) & (|marking(Ext_Mem_Acc_38_11)|=0) & (|marking(Ext_Mem_Acc_38_41)|=0) & (|marking(Ext_Mem_Acc_24_3)|=0) & (|marking(Ext_Mem_Acc_4_12)|=0) & (|marking(Ext_Mem_Acc_24_13)|=0) & (|marking(Ext_Mem_Acc_5_50)|=0) & (|marking(Ext_Mem_Acc_37_32)|=0) & (|marking(Ext_Mem_Acc_24_30)|=0) & (|marking(Ext_Mem_Acc_48_14)|=0) & (|marking(Ext_Mem_Acc_9_20)|=0) & (|marking(Ext_Mem_Acc_24_20)|=0) & (|marking(Ext_Mem_Acc_22_16)|=0) & (|marking(Ext_Mem_Acc_20_4)|=0) & (|marking(Ext_Mem_Acc_19_15)|=0) & (|marking(Ext_Mem_Acc_11_7)|=0) & (|marking(Ext_Mem_Acc_32_38)|=0) & (|marking(Ext_Mem_Acc_26_19)|=0) & (|marking(Ext_Mem_Acc_36_16)|=0) & (|marking(Ext_Mem_Acc_3_33)|=0) & (|marking(Ext_Mem_Acc_29_34)|=0) & (|marking(Ext_Mem_Acc_18_38)|=0) & (|marking(Ext_Mem_Acc_43_2)|=0) & (|marking(Ext_Mem_Acc_30_18)|=0) & (|marking(Ext_Mem_Acc_7_18)|=0) & (|marking(Ext_Mem_Acc_43_39)|=0) & (|marking(Ext_Mem_Acc_34_40)|=0) & (|marking(Ext_Mem_Acc_18_37)|=0) & (|marking(Ext_Mem_Acc_22_34)|=0) & (|marking(Ext_Mem_Acc_46_13)|=0) & (|marking(Ext_Mem_Acc_38_23)|=0) & (|marking(Ext_Mem_Acc_7_47)|=0) & (|marking(Ext_Mem_Acc_15_47)|=0) & (|marking(Ext_Mem_Acc_1_5)|=0) & (|marking(Ext_Mem_Acc_17_44)|=0) & (|marking(Ext_Mem_Acc_1_37)|=0) & (|marking(Ext_Mem_Acc_20_10)|=0) & (|marking(Ext_Mem_Acc_39_22)|=0) & (|marking(Ext_Mem_Acc_4_1)|=0) & (|marking(Ext_Mem_Acc_26_43)|=0) & (|marking(Ext_Mem_Acc_2_20)|=0) & (|marking(Ext_Mem_Acc_39_25)|=0) & (|marking(Ext_Mem_Acc_39_13)|=0) & (|marking(Ext_Mem_Acc_41_48)|=0) & (|marking(Ext_Mem_Acc_39_37)|=0) & (|marking(Ext_Mem_Acc_23_46)|=0) & (|marking(Ext_Mem_Acc_21_17)|=0) & (|marking(Ext_Mem_Acc_39_21)|=0) & (|marking(Ext_Mem_Acc_8_34)|=0) & (|marking(Ext_Mem_Acc_49_8)|=0) & (|marking(Ext_Mem_Acc_17_27)|=0) & (|marking(Ext_Mem_Acc_50_19)|=0) & (|marking(Ext_Mem_Acc_7_48)|=0) & (|marking(Ext_Mem_Acc_43_1)|=0) & (|marking(Ext_Mem_Acc_38_34)|=0) & (|marking(Ext_Mem_Acc_31_46)|=0) & (|marking(Ext_Mem_Acc_37_4)|=0) & (|marking(Ext_Mem_Acc_29_1)|=0) & (|marking(Ext_Mem_Acc_14_10)|=0) & (|marking(Ext_Mem_Acc_19_31)|=0) & (|marking(Ext_Mem_Acc_22_40)|=0) & (|marking(Ext_Mem_Acc_19_45)|=0) & (|marking(Ext_Mem_Acc_28_11)|=0) & (|marking(Ext_Mem_Acc_15_44)|=0) & (|marking(Ext_Mem_Acc_1_19)|=0) & (|marking(Ext_Mem_Acc_9_6)|=0) & (|marking(Ext_Mem_Acc_23_29)|=0) & (|marking(Ext_Mem_Acc_1_23)|=0) & (|marking(Ext_Mem_Acc_6_38)|=0) & (|marking(Ext_Mem_Acc_47_20)|=0) & (|marking(Ext_Mem_Acc_45_11)|=0) & (|marking(Ext_Mem_Acc_4_46)|=0) & (|marking(Ext_Mem_Acc_49_46)|=0) & (|marking(Ext_Mem_Acc_23_15)|=0) & (|marking(Ext_Mem_Acc_9_25)|=0) & (|marking(Ext_Mem_Acc_29_16)|=0) & (|marking(Ext_Mem_Acc_41_8)|=0) & (|marking(Ext_Mem_Acc_16_36)|=0) & (|marking(Ext_Mem_Acc_1_42)|=0) & (|marking(Ext_Mem_Acc_45_49)|=0) & (|marking(Ext_Mem_Acc_46_43)|=0) & (|marking(Ext_Mem_Acc_16_46)|=0) & (|marking(Ext_Mem_Acc_4_24)|=0) & (|marking(Ext_Mem_Acc_9_39)|=0) & (|marking(Ext_Mem_Acc_6_48)|=0) & (|marking(Ext_Mem_Acc_25_3)|=0) & (|marking(Ext_Mem_Acc_2_10)|=0) & (|marking(Ext_Mem_Acc_49_2)|=0) & (|marking(Ext_Mem_Acc_14_28)|=0) & (|marking(Ext_Mem_Acc_18_46)|=0) & (|marking(Ext_Mem_Acc_24_32)|=0) & (|marking(Ext_Mem_Acc_50_34)|=0) & (|marking(Ext_Mem_Acc_29_20)|=0) & (|marking(Ext_Mem_Acc_34_16)|=0) & (|marking(Ext_Mem_Acc_13_11)|=0) & (|marking(Ext_Mem_Acc_20_39)|=0) & (|marking(Ext_Mem_Acc_9_10)|=0) & (|marking(Ext_Mem_Acc_48_21)|=0) & (|marking(Ext_Mem_Acc_18_39)|=0) & (|marking(Ext_Mem_Acc_48_44)|=0) & (|marking(Ext_Mem_Acc_43_4)|=0) & (|marking(Ext_Mem_Acc_21_44)|=0) & (|marking(Ext_Mem_Acc_40_21)|=0) & (|marking(Ext_Mem_Acc_29_46)|=0) & (|marking(Ext_Mem_Acc_37_5)|=0) & (|marking(Ext_Mem_Acc_49_48)|=0) & (|marking(Ext_Mem_Acc_6_47)|=0) & (|marking(Ext_Mem_Acc_40_24)|=0) & (|marking(Ext_Mem_Acc_14_7)|=0) & (|marking(Ext_Mem_Acc_20_40)|=0) & (|marking(Ext_Mem_Acc_32_21)|=0) & (|marking(Ext_Mem_Acc_2_47)|=0) & (|marking(Ext_Mem_Acc_24_28)|=0) & (|marking(Ext_Mem_Acc_49_17)|=0) & (|marking(Ext_Mem_Acc_2_4)|=0) & (|marking(Ext_Mem_Acc_36_3)|=0) & (|marking(Ext_Mem_Acc_45_41)|=0) & (|marking(Ext_Mem_Acc_35_19)|=0) & (|marking(Ext_Mem_Acc_34_31)|=0) & (|marking(Ext_Mem_Acc_28_49)|=0) & (|marking(Ext_Mem_Acc_41_15)|=0) & (|marking(Ext_Mem_Acc_48_13)|=0) & (|marking(Ext_Mem_Acc_13_46)|=0) & (|marking(Ext_Mem_Acc_48_40)|=0) & (|marking(Ext_Mem_Acc_37_34)|=0) & (|marking(Ext_Mem_Acc_44_21)|=0) & (|marking(Ext_Mem_Acc_12_22)|=0) & (|marking(Ext_Mem_Acc_26_15)|=0) & (|marking(Ext_Mem_Acc_39_38)|=0) & (|marking(Ext_Mem_Acc_35_39)|=0) & (|marking(Ext_Mem_Acc_37_9)|=0) & (|marking(Ext_Mem_Acc_35_7)|=0) & (|marking(Ext_Mem_Acc_28_18)|=0) & (|marking(Ext_Mem_Acc_25_26)|=0) & (|marking(Ext_Mem_Acc_12_45)|=0) & (|marking(Ext_Mem_Acc_28_2)|=0) & (|marking(Ext_Mem_Acc_27_48)|=0) & (|marking(Ext_Mem_Acc_6_29)|=0) & (|marking(Ext_Mem_Acc_42_43)|=0) & (|marking(Ext_Mem_Acc_45_13)|=0) & (|marking(Ext_Mem_Acc_39_18)|=0) & (|marking(Ext_Mem_Acc_2_9)|=0) & (|marking(Ext_Mem_Acc_28_12)|=0) & (|marking(Ext_Mem_Acc_41_1)|=0) & (|marking(Ext_Mem_Acc_41_5)|=0) & (|marking(Ext_Mem_Acc_27_10)|=0) & (|marking(Ext_Mem_Acc_41_11)|=0) & (|marking(Ext_Mem_Acc_1_17)|=0) & (|marking(Ext_Mem_Acc_35_36)|=0) & (|marking(Ext_Mem_Acc_37_40)|=0) & (|marking(Ext_Mem_Acc_32_18)|=0) & (|marking(Ext_Mem_Acc_11_14)|=0) & (|marking(Ext_Mem_Acc_38_48)|=0) & (|marking(Ext_Mem_Acc_11_39)|=0) & (|marking(Ext_Mem_Acc_17_7)|=0) & (|marking(Ext_Mem_Acc_48_19)|=0) & (|marking(Ext_Mem_Acc_38_29)|=0) & (|marking(Ext_Mem_Acc_11_19)|=0) & (|marking(Ext_Mem_Acc_33_18)|=0) & (|marking(Ext_Mem_Acc_10_47)|=0) & (|marking(Ext_Mem_Acc_32_15)|=0) & (|marking(Ext_Mem_Acc_29_11)|=0) & (|marking(Ext_Mem_Acc_16_32)|=0) & (|marking(Ext_Mem_Acc_25_23)|=0) & (|marking(Ext_Mem_Acc_11_21)|=0) & (|marking(Ext_Mem_Acc_18_2)|=0) & (|marking(Ext_Mem_Acc_34_32)|=0) & (|marking(Ext_Mem_Acc_8_28)|=0) & (|marking(Ext_Mem_Acc_7_41)|=0) & (|marking(Ext_Mem_Acc_47_40)|=0) & (|marking(Ext_Mem_Acc_48_1)|=0) & (|marking(Ext_Mem_Acc_12_3)|=0) & (|marking(Ext_Mem_Acc_50_23)|=0) & (|marking(Ext_Mem_Acc_30_45)|=0) & (|marking(Ext_Mem_Acc_40_19)|=0) & (|marking(Ext_Mem_Acc_19_13)|=0) & (|marking(Ext_Mem_Acc_25_28)|=0) & (|marking(Ext_Mem_Acc_8_35)|=0) & (|marking(Ext_Mem_Acc_21_16)|=0) & (|marking(Ext_Mem_Acc_34_13)|=0) & (|marking(Ext_Mem_Acc_32_10)|=0) & (|marking(Ext_Mem_Acc_30_11)|=0) & (|marking(Ext_Mem_Acc_7_19)|=0) & (|marking(Ext_Mem_Acc_2_29)|=0) & (|marking(Ext_Mem_Acc_29_18)|=0) & (|marking(Ext_Mem_Acc_22_48)|=0) & (|marking(Ext_Mem_Acc_6_18)|=0) & (|marking(Ext_Mem_Acc_39_29)|=0) & (|marking(Ext_Mem_Acc_28_29)|=0) & (|marking(Ext_Mem_Acc_26_2)|=0) & (|marking(Ext_Mem_Acc_42_13)|=0) & (|marking(Ext_Mem_Acc_46_33)|=0) & (|marking(Ext_Mem_Acc_36_45)|=0) & (|marking(Ext_Mem_Acc_35_45)|=0) & (|marking(Ext_Mem_Acc_32_3)|=0) & (|marking(Ext_Mem_Acc_2_42)|=0) & (|marking(Ext_Mem_Acc_20_23)|=0) & (|marking(Ext_Mem_Acc_29_32)|=0) & (|marking(Ext_Mem_Acc_31_12)|=0) & (|marking(Ext_Mem_Acc_40_34)|=0) & (|marking(Ext_Mem_Acc_13_26)|=0) & (|marking(Ext_Mem_Acc_14_12)|=0) & (|marking(Ext_Mem_Acc_43_20)|=0) & (|marking(Ext_Mem_Acc_36_6)|=0) & (|marking(Ext_Mem_Acc_37_21)|=0) & (|marking(Ext_Mem_Acc_34_20)|=0) & (|marking(Ext_Mem_Acc_27_40)|=0) & (|marking(Ext_Mem_Acc_28_25)|=0) & (|marking(Ext_Mem_Acc_43_22)|=0) & (|marking(Ext_Mem_Acc_21_27)|=0) & (|marking(Ext_Mem_Acc_33_12)|=0) & (|marking(Ext_Mem_Acc_1_43)|=0) & (|marking(Ext_Mem_Acc_46_16)|=0) & (|marking(Ext_Mem_Acc_45_15)|=0) & (|marking(Ext_Mem_Acc_49_28)|=0) & (|marking(Ext_Mem_Acc_29_6)|=0) & (|marking(Ext_Mem_Acc_41_42)|=0) & (|marking(Ext_Mem_Acc_19_24)|=0) & (|marking(Ext_Mem_Acc_23_39)|=0) & (|marking(Ext_Mem_Acc_34_6)|=0) & (|marking(Ext_Mem_Acc_13_23)|=0) & (|marking(Ext_Mem_Acc_21_45)|=0) & (|marking(Ext_Mem_Acc_27_37)|=0) & (|marking(Ext_Mem_Acc_13_40)|=0) & (|marking(Ext_Mem_Acc_17_14)|=0) & (|marking(Ext_Mem_Acc_48_30)|=0) & (|marking(Ext_Mem_Acc_38_39)|=0) & (|marking(Ext_Mem_Acc_50_8)|=0) & (|marking(Ext_Mem_Acc_47_5)|=0) & (|marking(Ext_Mem_Acc_13_15)|=0) & (|marking(Ext_Mem_Acc_40_38)|=0) & (|marking(Ext_Mem_Acc_47_32)|=0) & (|marking(Ext_Mem_Acc_38_2)|=0) & (|marking(Ext_Mem_Acc_34_22)|=0) & (|marking(Ext_Mem_Acc_29_2)|=0) & (|marking(Ext_Mem_Acc_12_47)|=0) & (|marking(Ext_Mem_Acc_22_3)|=0) & (|marking(Ext_Mem_Acc_20_19)|=0) & (|marking(Ext_Mem_Acc_9_28)|=0) & (|marking(Ext_Mem_Acc_43_27)|=0) & (|marking(Ext_Mem_Acc_25_42)|=0) & (|marking(Ext_Mem_Acc_40_48)|=0) & (|marking(Ext_Mem_Acc_8_14)|=0) & (|marking(Ext_Mem_Acc_12_15)|=0) & (|marking(Ext_Mem_Acc_48_11)|=0) & (|marking(Ext_Mem_Acc_5_3)|=0) & (|marking(Ext_Mem_Acc_45_42)|=0) & (|marking(Ext_Mem_Acc_26_12)|=0) & (|marking(Ext_Mem_Acc_12_21)|=0) & (|marking(Ext_Mem_Acc_38_25)|=0) & (|marking(Ext_Mem_Acc_48_9)|=0) & (|marking(Ext_Mem_Acc_12_49)|=0) & (|marking(Ext_Mem_Acc_23_5)|=0) & (|marking(Ext_Mem_Acc_16_26)|=0) & (|marking(Ext_Mem_Acc_7_43)|=0) & (|marking(Ext_Mem_Acc_17_2)|=0) & (|marking(Ext_Mem_Acc_11_35)|=0) & (|marking(Ext_Mem_Acc_27_22)|=0) & (|marking(Ext_Mem_Acc_39_46)|=0) & (|marking(Ext_Mem_Acc_25_46)|=0) & (|marking(Ext_Mem_Acc_22_37)|=0) & (|marking(Ext_Mem_Acc_36_23)|=0) & (|marking(Ext_Mem_Acc_38_44)|=0) & (|marking(Ext_Mem_Acc_28_37)|=0) & (|marking(Ext_Mem_Acc_1_32)|=0) & (|marking(Ext_Mem_Acc_19_44)|=0) & (|marking(Ext_Mem_Acc_31_4)|=0) & (|marking(Ext_Mem_Acc_50_20)|=0) & (|marking(Ext_Mem_Acc_19_32)|=0) & (|marking(Ext_Mem_Acc_14_13)|=0) & (|marking(Ext_Mem_Acc_14_24)|=0) & (|marking(Ext_Mem_Acc_38_3)|=0) & (|marking(Ext_Mem_Acc_15_21)|=0) & (|marking(Ext_Mem_Acc_40_30)|=0) & (|marking(Ext_Mem_Acc_32_5)|=0) & (|marking(Ext_Mem_Acc_6_10)|=0) & (|marking(Ext_Mem_Acc_40_17)|=0) & (|marking(Ext_Mem_Acc_14_42)|=0) & (|marking(Ext_Mem_Acc_7_21)|=0) & (|marking(Ext_Mem_Acc_33_20)|=0) & (|marking(Ext_Mem_Acc_9_48)|=0) & (|marking(Ext_Mem_Acc_1_16)|=0) & (|marking(Ext_Mem_Acc_27_38)|=0) & (|marking(Ext_Mem_Acc_15_42)|=0) & (|marking(Ext_Mem_Acc_47_34)|=0) & (|marking(Ext_Mem_Acc_3_30)|=0) & (|marking(Ext_Mem_Acc_41_38)|=0) & (|marking(Ext_Mem_Acc_43_24)|=0) & (|marking(Ext_Mem_Acc_49_20)|=0) & (|marking(Ext_Mem_Acc_24_42)|=0) & (|marking(Ext_Mem_Acc_1_11)|=0) & (|marking(Ext_Mem_Acc_41_23)|=0) & (|marking(Ext_Mem_Acc_19_17)|=0) & (|marking(Ext_Mem_Acc_43_9)|=0) & (|marking(Ext_Mem_Acc_44_8)|=0) & (|marking(Ext_Mem_Acc_15_30)|=0) & (|marking(Ext_Mem_Acc_13_20)|=0) & (|marking(Ext_Mem_Acc_3_38)|=0) & (|marking(Ext_Mem_Acc_2_32)|=0) & (|marking(Ext_Mem_Acc_48_25)|=0) & (|marking(Ext_Mem_Acc_47_35)|=0) & (|marking(Ext_Mem_Acc_5_42)|=0) & (|marking(Ext_Mem_Acc_49_29)|=0) & (|marking(Ext_Mem_Acc_35_37)|=0) & (|marking(Ext_Mem_Acc_1_36)|=0) & (|marking(Ext_Mem_Acc_15_19)|=0) & (|marking(Ext_Mem_Acc_29_43)|=0) & (|marking(Ext_Mem_Acc_13_21)|=0) & (|marking(Ext_Mem_Acc_41_36)|=0) & (|marking(Ext_Mem_Acc_34_15)|=0) & (|marking(Ext_Mem_Acc_20_35)|=0) & (|marking(Ext_Mem_Acc_37_27)|=0) & (|marking(Ext_Mem_Acc_23_21)|=0) & (|marking(Ext_Mem_Acc_10_20)|=0) & (|marking(Ext_Mem_Acc_32_16)|=0) & (|marking(Ext_Mem_Acc_7_29)|=0) & (|marking(Ext_Mem_Acc_9_11)|=0) & (|marking(Ext_Mem_Acc_44_36)|=0) & (|marking(Ext_Mem_Acc_14_5)|=0) & (|marking(Ext_Mem_Acc_16_12)|=0) & (|marking(Ext_Mem_Acc_26_3)|=0) & (|marking(Ext_Mem_Acc_43_35)|=0) & (|marking(Ext_Mem_Acc_21_10)|=0) & (|marking(Ext_Mem_Acc_16_47)|=0) & (|marking(Ext_Mem_Acc_36_42)|=0) & (|marking(Ext_Mem_Acc_8_50)|=0) & (|marking(Ext_Mem_Acc_36_29)|=0) & (|marking(Ext_Mem_Acc_5_34)|=0) & (|marking(Ext_Mem_Acc_4_2)|=0) & (|marking(Ext_Mem_Acc_38_20)|=0) & (|marking(Ext_Mem_Acc_3_39)|=0) & (|marking(Ext_Mem_Acc_31_3)|=0) & (|marking(Ext_Mem_Acc_6_4)|=0) & (|marking(Ext_Mem_Acc_18_30)|=0) & (|marking(Ext_Mem_Acc_44_35)|=0) & (|marking(Ext_Mem_Acc_15_14)|=0) & (|marking(Ext_Mem_Acc_50_13)|=0) & (|marking(Ext_Mem_Acc_23_16)|=0) & (|marking(Ext_Mem_Acc_28_24)|=0) & (|marking(Ext_Mem_Acc_30_15)|=0) & (|marking(Ext_Mem_Acc_30_46)|=0) & (|marking(Ext_Mem_Acc_39_27)|=0) & (|marking(Ext_Mem_Acc_14_20)|=0) & (|marking(Ext_Mem_Acc_14_2)|=0) & (|marking(Ext_Mem_Acc_20_50)|=0) & (|marking(Ext_Mem_Acc_32_36)|=0) & (|marking(Ext_Mem_Acc_3_15)|=0) & (|marking(Ext_Mem_Acc_12_28)|=0) & (|marking(Ext_Mem_Acc_28_30)|=0) & (|marking(Ext_Mem_Acc_8_25)|=0) & (|marking(Ext_Mem_Acc_29_5)|=0) & (|marking(Ext_Mem_Acc_50_38)|=0) & (|marking(Ext_Mem_Acc_33_47)|=0) & (|marking(Ext_Mem_Acc_36_7)|=0) & (|marking(Ext_Mem_Acc_6_50)|=0) & (|marking(Ext_Mem_Acc_22_25)|=0) & (|marking(Ext_Mem_Acc_6_8)|=0) & (|marking(Ext_Mem_Acc_6_13)|=0) & (|marking(Ext_Mem_Acc_42_23)|=0) & (|marking(Ext_Mem_Acc_17_50)|=0) & (|marking(Ext_Mem_Acc_38_10)|=0) & (|marking(Ext_Mem_Acc_34_9)|=0) & (|marking(Ext_Mem_Acc_28_44)|=0) & (|marking(Ext_Mem_Acc_10_5)|=0) & (|marking(Ext_Mem_Acc_3_41)|=0) & (|marking(Ext_Mem_Acc_38_42)|=0) & (|marking(Ext_Mem_Acc_43_48)|=0) & (|marking(Ext_Mem_Acc_41_45)|=0) & (|marking(Ext_Mem_Acc_45_43)|=0) & (|marking(Ext_Mem_Acc_33_36)|=0) & (|marking(Ext_Mem_Acc_50_41)|=0) & (|marking(Ext_Mem_Acc_19_47)|=0) & (|marking(Ext_Mem_Acc_19_7)|=0) & (|marking(Ext_Mem_Acc_5_17)|=0) & (|marking(Ext_Mem_Acc_42_46)|=0) & (|marking(Ext_Mem_Acc_31_1)|=0) & (|marking(Ext_Mem_Acc_34_18)|=0) & (|marking(Ext_Mem_Acc_29_26)|=0) & (|marking(Ext_Mem_Acc_33_4)|=0) & (|marking(Ext_Mem_Acc_19_2)|=0) & (|marking(Ext_Mem_Acc_15_25)|=0) & (|marking(Ext_Mem_Acc_36_19)|=0) & (|marking(Ext_Mem_Acc_14_31)|=0) & (|marking(Ext_Mem_Acc_17_32)|=0) & (|marking(Ext_Mem_Acc_5_47)|=0) & (|marking(Ext_Mem_Acc_7_35)|=0) & (|marking(Ext_Mem_Acc_44_26)|=0) & (|marking(Ext_Mem_Acc_47_4)|=0) & (|marking(Ext_Mem_Acc_6_22)|=0) & (|marking(Ext_Mem_Acc_46_18)|=0) & (|marking(Ext_Mem_Acc_49_34)|=0) & (|marking(Ext_Mem_Acc_17_28)|=0) & (|marking(Ext_Mem_Acc_23_13)|=0) & (|marking(Ext_Mem_Acc_9_44)|=0) & (|marking(Ext_Mem_Acc_40_49)|=0) & (|marking(Ext_Mem_Acc_8_27)|=0) & (|marking(Ext_Mem_Acc_11_31)|=0) & (|marking(Ext_Mem_Acc_10_25)|=0) & (|marking(Ext_Mem_Acc_11_16)|=0) & (|marking(Ext_Mem_Acc_29_27)|=0) & (|marking(Ext_Mem_Acc_40_29)|=0) & (|marking(Ext_Mem_Acc_1_47)|=0) & (|marking(Ext_Mem_Acc_27_33)|=0) & (|marking(Ext_Mem_Acc_39_15)|=0) & (|marking(Ext_Mem_Acc_21_7)|=0) & (|marking(Ext_Mem_Acc_27_18)|=0) & (|marking(Ext_Mem_Acc_11_48)|=0) & (|marking(Ext_Mem_Acc_46_38)|=0) & (|marking(Ext_Mem_Acc_40_39)|=0) & (|marking(Ext_Mem_Acc_35_16)|=0) & (|marking(Ext_Mem_Acc_50_48)|=0) & (|marking(Ext_Mem_Acc_49_14)|=0) & (|marking(Ext_Mem_Acc_3_32)|=0) & (|marking(Ext_Mem_Acc_44_15)|=0) & (|marking(Ext_Mem_Acc_40_11)|=0) & (|marking(Ext_Mem_Acc_11_37)|=0) & (|marking(Ext_Mem_Acc_11_38)|=0) & (|marking(Ext_Mem_Acc_25_31)|=0) & (|marking(Ext_Mem_Acc_24_22)|=0) & (|marking(Ext_Mem_Acc_20_5)|=0) & (|marking(Ext_Mem_Acc_37_35)|=0) & (|marking(Ext_Mem_Acc_49_45)|=0) & (|marking(Ext_Mem_Acc_32_9)|=0) & (|marking(Ext_Mem_Acc_37_31)|=0) & (|marking(Ext_Mem_Acc_50_43)|=0) & (|marking(Ext_Mem_Acc_48_27)|=0) & (|marking(Ext_Mem_Acc_19_20)|=0) & (|marking(Ext_Mem_Acc_39_33)|=0) & (|marking(Ext_Mem_Acc_50_49)|=0) & (|marking(Ext_Mem_Acc_29_30)|=0) & (|marking(Ext_Mem_Acc_11_2)|=0) & (|marking(Ext_Mem_Acc_21_35)|=0) & (|marking(Ext_Mem_Acc_32_20)|=0) & (|marking(Ext_Mem_Acc_5_36)|=0) & (|marking(Ext_Mem_Acc_44_45)|=0) & (|marking(Ext_Mem_Acc_37_49)|=0) & (|marking(Ext_Mem_Acc_11_25)|=0) & (|marking(Ext_Mem_Acc_46_2)|=0) & (|marking(Ext_Mem_Acc_30_28)|=0) & (|marking(Ext_Mem_Acc_32_28)|=0) & (|marking(Ext_Mem_Acc_17_10)|=0) & (|marking(Ext_Mem_Acc_32_13)|=0) & (|marking(Ext_Mem_Acc_30_50)|=0) & (|marking(Ext_Mem_Acc_29_38)|=0) & (|marking(Ext_Mem_Acc_4_48)|=0) & (|marking(Ext_Mem_Acc_47_10)|=0) & (|marking(Ext_Mem_Acc_12_33)|=0) & (|marking(Ext_Mem_Acc_25_20)|=0) & (|marking(Ext_Mem_Acc_44_2)|=0) & (|marking(Ext_Mem_Acc_4_38)|=0) & (|marking(Ext_Mem_Acc_23_17)|=0) & (|marking(Ext_Mem_Acc_3_37)|=0) & (|marking(Ext_Mem_Acc_5_2)|=0) & (|marking(Ext_Mem_Acc_49_15)|=0) & (|marking(Ext_Mem_Acc_15_10)|=0) & (|marking(Ext_Mem_Acc_16_10)|=0) & (|marking(Ext_Mem_Acc_32_35)|=0) & (|marking(Ext_Mem_Acc_30_24)|=0) & (|marking(Ext_Mem_Acc_12_32)|=0) & (|marking(Ext_Mem_Acc_9_41)|=0) & (|marking(Ext_Mem_Acc_9_27)|=0) & (|marking(Ext_Mem_Acc_5_37)|=0) & (|marking(Ext_Mem_Acc_16_41)|=0) & (|marking(Ext_Mem_Acc_29_31)|=0) & (|marking(Ext_Mem_Acc_22_9)|=0) & (|marking(Ext_Mem_Acc_31_32)|=0) & (|marking(Ext_Mem_Acc_5_15)|=0) & (|marking(Ext_Mem_Acc_34_10)|=0) & (|marking(Ext_Mem_Acc_25_7)|=0) & (|marking(Ext_Mem_Acc_33_21)|=0) & (|marking(Ext_Mem_Acc_2_48)|=0) & (|marking(Ext_Mem_Acc_44_24)|=0) & (|marking(Ext_Mem_Acc_36_20)|=0) & (|marking(Ext_Mem_Acc_43_13)|=0) & (|marking(Ext_Mem_Acc_22_17)|=0) & (|marking(Ext_Mem_Acc_47_41)|=0) & (|marking(Ext_Mem_Acc_30_4)|=0) & (|marking(Ext_Mem_Acc_48_24)|=0) & (|marking(Ext_Mem_Acc_36_17)|=0) & (|marking(Ext_Mem_Acc_18_21)|=0) & (|marking(Ext_Mem_Acc_39_6)|=0) & (|marking(Ext_Mem_Acc_2_7)|=0) & (|marking(Ext_Mem_Acc_46_17)|=0) & (|marking(Ext_Mem_Acc_48_20)|=0) & (|marking(Ext_Mem_Acc_30_35)|=0) & (|marking(Ext_Mem_Acc_9_16)|=0) & (|marking(Ext_Mem_Acc_4_27)|=0) & (|marking(Ext_Mem_Acc_42_49)|=0) & (|marking(Ext_Mem_Acc_3_17)|=0) & (|marking(Ext_Mem_Acc_41_33)|=0) & (|marking(Ext_Mem_Acc_43_40)|=0) & (|marking(Ext_Mem_Acc_19_34)|=0) & (|marking(Ext_Mem_Acc_27_20)|=0) & (|marking(Ext_Mem_Acc_35_46)|=0) & (|marking(Ext_Mem_Acc_20_16)|=0) & (|marking(Ext_Mem_Acc_21_37)|=0) & (|marking(Ext_Mem_Acc_15_35)|=0) & (|marking(Ext_Mem_Acc_48_36)|=0) & (|marking(Ext_Mem_Acc_46_15)|=0) & (|marking(Ext_Mem_Acc_23_25)|=0) & (|marking(Ext_Mem_Acc_40_43)|=0) & (|marking(Ext_Mem_Acc_18_16)|=0) & (|marking(Ext_Mem_Acc_11_5)|=0) & (|marking(Ext_Mem_Acc_13_37)|=0) & (|marking(Ext_Mem_Acc_35_47)|=0) & (|marking(Ext_Mem_Acc_35_49)|=0) & (|marking(Ext_Mem_Acc_33_40)|=0) & (|marking(Ext_Mem_Acc_36_46)|=0) & (|marking(Ext_Mem_Acc_13_22)|=0) & (|marking(Ext_Mem_Acc_44_13)|=0) & (|marking(Ext_Mem_Acc_31_21)|=0) & (|marking(Ext_Mem_Acc_47_23)|=0) & (|marking(Ext_Mem_Acc_3_22)|=0) & (|marking(Ext_Mem_Acc_8_41)|=0) & (|marking(Ext_Mem_Acc_19_21)|=0) & (|marking(Ext_Mem_Acc_50_31)|=0) & (|marking(Ext_Mem_Acc_34_5)|=0) & (|marking(Ext_Mem_Acc_9_29)|=0) & (|marking(Ext_Mem_Acc_41_46)|=0) & (|marking(Ext_Mem_Acc_41_12)|=0) & (|marking(Ext_Mem_Acc_22_29)|=0) & (|marking(Ext_Mem_Acc_16_17)|=0) & (|marking(Ext_Mem_Acc_40_50)|=0) & (|marking(Ext_Mem_Acc_39_11)|=0) & (|marking(Ext_Mem_Acc_24_34)|=0) & (|marking(Ext_Mem_Acc_47_25)|=0) & (|marking(Ext_Mem_Acc_5_19)|=0) & (|marking(Ext_Mem_Acc_46_36)|=0) & (|marking(Ext_Mem_Acc_17_49)|=0) & (|marking(Ext_Mem_Acc_17_30)|=0) & (|marking(Ext_Mem_Acc_9_33)|=0) & (|marking(Ext_Mem_Acc_49_19)|=0) & (|marking(Ext_Mem_Acc_7_27)|=0) & (|marking(Ext_Mem_Acc_20_24)|=0) & (|marking(Ext_Mem_Acc_9_18)|=0) & (|marking(Ext_Mem_Acc_33_8)|=0) & (|marking(Ext_Mem_Acc_40_25)|=0) & (|marking(Ext_Mem_Acc_30_8)|=0) & (|marking(Ext_Mem_Acc_22_20)|=0) & (|marking(Ext_Mem_Acc_25_33)|=0) & (|marking(Ext_Mem_Acc_3_50)|=0) & (|marking(Ext_Mem_Acc_26_44)|=0) & (|marking(Ext_Mem_Acc_32_47)|=0) & (|marking(Ext_Mem_Acc_20_21)|=0) & (|marking(Ext_Mem_Acc_40_16)|=0) & (|marking(Ext_Mem_Acc_27_7)|=0) & (|marking(Ext_Mem_Acc_36_10)|=0) & (|marking(Ext_Mem_Acc_3_19)|=0) & (|marking(Ext_Mem_Acc_48_28)|=0) & (|marking(Ext_Mem_Acc_36_33)|=0) & (|marking(Ext_Mem_Acc_47_12)|=0) & (|marking(Ext_Mem_Acc_32_42)|=0) & (|marking(Ext_Mem_Acc_42_9)|=0) & (|marking(Ext_Mem_Acc_35_41)|=0) & (|marking(Ext_Mem_Acc_22_11)|=0) & (|marking(Ext_Mem_Acc_2_43)|=0) & (|marking(Ext_Mem_Acc_19_25)|=0) & (|marking(Ext_Mem_Acc_34_28)|=0) & (|marking(Ext_Mem_Acc_49_24)|=0) & (|marking(Ext_Mem_Acc_47_43)|=0) & (|marking(Ext_Mem_Acc_36_8)|=0) & (|marking(Ext_Mem_Acc_10_35)|=0) & (|marking(Ext_Mem_Acc_13_48)|=0) & (|marking(Ext_Mem_Acc_2_21)|=0) & (|marking(Ext_Mem_Acc_42_50)|=0) & (|marking(Ext_Mem_Acc_41_2)|=0) & (|marking(Ext_Mem_Acc_12_2)|=0) & (|marking(Ext_Mem_Acc_12_41)|=0) & (|marking(Ext_Mem_Acc_12_18)|=0) & (|marking(Ext_Mem_Acc_34_37)|=0) & (|marking(Ext_Mem_Acc_14_26)|=0) & (|marking(Ext_Mem_Acc_16_35)|=0) & (|marking(Ext_Mem_Acc_15_39)|=0) & (|marking(Ext_Mem_Acc_6_41)|=0) & (|marking(Ext_Mem_Acc_35_5)|=0) & (|marking(Ext_Mem_Acc_30_37)|=0) & (|marking(Ext_Mem_Acc_39_36)|=0) & (|marking(Ext_Mem_Acc_30_43)|=0) & (|marking(Ext_Mem_Acc_40_20)|=0) & (|marking(Ext_Mem_Acc_27_19)|=0) & (|marking(Ext_Mem_Acc_7_13)|=0) & (|marking(Ext_Mem_Acc_8_36)|=0) & (|marking(Ext_Mem_Acc_13_30)|=0) & (|marking(Ext_Mem_Acc_28_43)|=0) & (|marking(Ext_Mem_Acc_18_47)|=0) & (|marking(Ext_Mem_Acc_50_3)|=0) & (|marking(Ext_Mem_Acc_50_21)|=0) & (|marking(Ext_Mem_Acc_50_7)|=0) & (|marking(Ext_Mem_Acc_12_50)|=0) & (|marking(Ext_Mem_Acc_12_26)|=0) & (|marking(Ext_Mem_Acc_49_44)|=0) & (|marking(Ext_Mem_Acc_34_27)|=0) & (|marking(Ext_Mem_Acc_42_6)|=0) & (|marking(Ext_Mem_Acc_10_32)|=0) & (|marking(Ext_Mem_Acc_35_48)|=0) & (|marking(Ext_Mem_Acc_30_34)|=0) & (|marking(Ext_Mem_Acc_19_49)|=0) & (|marking(Ext_Mem_Acc_22_50)|=0) & (|marking(Ext_Mem_Acc_5_13)|=0) & (|marking(Ext_Mem_Acc_29_4)|=0) & (|marking(Ext_Mem_Acc_38_43)|=0) & (|marking(Ext_Mem_Acc_46_22)|=0) & (|marking(Ext_Mem_Acc_14_8)|=0) & (|marking(Ext_Mem_Acc_19_30)|=0) & (|marking(Ext_Mem_Acc_42_5)|=0) & (|marking(Ext_Mem_Acc_8_18)|=0) & (|marking(Ext_Mem_Acc_33_7)|=0) & (|marking(Ext_Mem_Acc_13_34)|=0) & (|marking(Ext_Mem_Acc_37_46)|=0) & (|marking(Ext_Mem_Acc_5_22)|=0) & (|marking(Ext_Mem_Acc_46_34)|=0) & (|marking(Ext_Mem_Acc_11_42)|=0) & (|marking(Ext_Mem_Acc_16_11)|=0) & (|marking(Ext_Mem_Acc_37_38)|=0) & (|marking(Ext_Mem_Acc_34_2)|=0) & (|marking(Ext_Mem_Acc_42_48)|=0) & (|marking(Ext_Mem_Acc_24_36)|=0) & (|marking(Ext_Mem_Acc_17_26)|=0) & (|marking(Ext_Mem_Acc_39_1)|=0) & (|marking(Ext_Mem_Acc_2_1)|=0) & (|marking(Ext_Mem_Acc_39_24)|=0) & (|marking(Ext_Mem_Acc_35_40)|=0) & (|marking(Ext_Mem_Acc_32_12)|=0) & (|marking(Ext_Mem_Acc_21_20)|=0) & (|marking(Ext_Mem_Acc_23_12)|=0) & (|marking(Ext_Mem_Acc_5_20)|=0) & (|marking(Ext_Mem_Acc_6_23)|=0) & (|marking(Ext_Mem_Acc_23_1)|=0) & (|marking(Ext_Mem_Acc_1_25)|=0) & (|marking(Ext_Mem_Acc_16_38)|=0) & (|marking(Ext_Mem_Acc_32_25)|=0) & (|marking(Ext_Mem_Acc_12_5)|=0) & (|marking(Ext_Mem_Acc_27_11)|=0) & (|marking(Ext_Mem_Acc_28_16)|=0) & (|marking(Ext_Mem_Acc_17_15)|=0) & (|marking(Ext_Mem_Acc_3_34)|=0) & (|marking(Ext_Mem_Acc_28_23)|=0) & (|marking(Ext_Mem_Acc_29_35)|=0) & (|marking(Ext_Mem_Acc_35_11)|=0) & (|marking(Ext_Mem_Acc_4_39)|=0) & (|marking(Ext_Mem_Acc_22_19)|=0) & (|marking(Ext_Mem_Acc_4_31)|=0) & (|marking(Ext_Mem_Acc_23_37)|=0) & (|marking(Ext_Mem_Acc_23_49)|=0) & (|marking(Ext_Mem_Acc_27_16)|=0) & (|marking(Ext_Mem_Acc_19_16)|=0) & (|marking(Ext_Mem_Acc_23_3)|=0) & (|marking(Ext_Mem_Acc_48_39)|=0) & (|marking(Ext_Mem_Acc_44_32)|=0) & (|marking(Ext_Mem_Acc_21_38)|=0) & (|marking(Ext_Mem_Acc_36_41)|=0) & (|marking(Ext_Mem_Acc_8_39)|=0) & (|marking(Ext_Mem_Acc_11_13)|=0) & (|marking(Ext_Mem_Acc_35_30)|=0) & (|marking(Ext_Mem_Acc_12_14)|=0) & (|marking(Ext_Mem_Acc_40_9)|=0) & (|marking(Ext_Mem_Acc_48_7)|=0) & (|marking(Ext_Mem_Acc_48_17)|=0) & (|marking(Ext_Mem_Acc_25_22)|=0) & (|marking(Ext_Mem_Acc_3_40)|=0) & (|marking(Ext_Mem_Acc_50_25)|=0) & (|marking(Ext_Mem_Acc_21_31)|=0) & (|marking(Ext_Mem_Acc_6_5)|=0) & (|marking(Ext_Mem_Acc_36_12)|=0) & (|marking(Ext_Mem_Acc_35_1)|=0) & (|marking(Ext_Mem_Acc_35_43)|=0) & (|marking(Ext_Mem_Acc_30_31)|=0) & (|marking(Ext_Mem_Acc_2_44)|=0) & (|marking(Ext_Mem_Acc_38_33)|=0) & (|marking(Ext_Mem_Acc_41_13)|=0) & (|marking(Ext_Mem_Acc_32_41)|=0) & (|marking(Ext_Mem_Acc_47_6)|=0) & (|marking(Ext_Mem_Acc_40_6)|=0) & (|marking(Ext_Mem_Acc_48_35)|=0) & (|marking(Ext_Mem_Acc_16_7)|=0) & (|marking(Ext_Mem_Acc_18_6)|=0) & (|marking(Ext_Mem_Acc_13_32)|=0) & (|marking(Ext_Mem_Acc_17_4)|=0) & (|marking(Ext_Mem_Acc_11_36)|=0) & (|marking(Ext_Mem_Acc_21_33)|=0) & (|marking(Ext_Mem_Acc_47_17)|=0) & (|marking(Ext_Mem_Acc_17_29)|=0) & (|marking(Ext_Mem_Acc_18_22)|=0) & (|marking(Ext_Mem_Acc_50_22)|=0) & (|marking(Ext_Mem_Acc_50_18)|=0) & (|marking(Ext_Mem_Acc_6_17)|=0) & (|marking(Ext_Mem_Acc_24_46)|=0) & (|marking(Ext_Mem_Acc_12_8)|=0) & (|marking(Ext_Mem_Acc_5_46)|=0) & (|marking(Ext_Mem_Acc_34_47)|=0) & (|marking(Ext_Mem_Acc_24_11)|=0) & (|marking(Ext_Mem_Acc_13_3)|=0) & (|marking(Ext_Mem_Acc_14_33)|=0) & (|marking(Ext_Mem_Acc_2_14)|=0) & (|marking(Ext_Mem_Acc_40_1)|=0) & (|marking(Ext_Mem_Acc_48_33)|=0) & (|marking(Ext_Mem_Acc_5_40)|=0) & (|marking(Ext_Mem_Acc_6_25)|=0) & (|marking(Ext_Mem_Acc_19_6)|=0) & (|marking(Ext_Mem_Acc_50_35)|=0) & (|marking(Ext_Mem_Acc_1_26)|=0) & (|marking(Ext_Mem_Acc_20_6)|=0) & (|marking(Ext_Mem_Acc_49_5)|=0) & (|marking(Ext_Mem_Acc_22_32)|=0) & (|marking(Ext_Mem_Acc_1_41)|=0) & (|marking(Ext_Mem_Acc_1_35)|=0) & (|marking(Ext_Mem_Acc_49_35)|=0) & (|marking(Ext_Mem_Acc_2_3)|=0) & (|marking(Ext_Mem_Acc_9_12)|=0) & (|marking(Ext_Mem_Acc_10_41)|=0) & (|marking(Ext_Mem_Acc_46_27)|=0) & (|marking(Ext_Mem_Acc_49_6)|=0) & (|marking(Ext_Mem_Acc_37_18)|=0) & (|marking(Ext_Mem_Acc_43_30)|=0) & (|marking(Ext_Mem_Acc_7_4)|=0) & (|marking(Ext_Mem_Acc_37_8)|=0) & (|marking(Ext_Mem_Acc_45_2)|=0) & (|marking(Ext_Mem_Acc_41_20)|=0) & (|marking(Ext_Mem_Acc_11_29)|=0) & (|marking(Ext_Mem_Acc_25_29)|=0) & (|marking(Ext_Mem_Acc_19_4)|=0) & (|marking(Ext_Mem_Acc_25_9)|=0) & (|marking(Ext_Mem_Acc_44_47)|=0) & (|marking(Ext_Mem_Acc_20_27)|=0) & (|marking(Ext_Mem_Acc_15_6)|=0) & (|marking(Ext_Mem_Acc_8_4)|=0) & (|marking(Ext_Mem_Acc_18_44)|=0) & (|marking(Ext_Mem_Acc_37_2)|=0) & (|marking(Ext_Mem_Acc_14_41)|=0) & (|marking(Ext_Mem_Acc_12_11)|=0) & (|marking(Ext_Mem_Acc_38_26)|=0) & (|marking(Ext_Mem_Acc_3_7)|=0) & (|marking(Ext_Mem_Acc_6_44)|=0) & (|marking(Ext_Mem_Acc_6_30)|=0) & (|marking(Ext_Mem_Acc_15_7)|=0) & (|marking(Ext_Mem_Acc_42_18)|=0) & (|marking(Ext_Mem_Acc_42_22)|=0) & (|marking(Ext_Mem_Acc_2_36)|=0) & (|marking(Ext_Mem_Acc_46_10)|=0) & (|marking(Ext_Mem_Acc_21_14)|=0) & (|marking(Ext_Mem_Acc_14_9)|=0) & (|marking(Ext_Mem_Acc_45_26)|=0) & (|marking(Ext_Mem_Acc_10_2)|=0) & (|marking(Ext_Mem_Acc_45_17)|=0) & (|marking(Ext_Mem_Acc_31_19)|=0) & (|marking(Ext_Mem_Acc_30_21)|=0) & (|marking(Ext_Mem_Acc_30_5)|=0) & (|marking(Ext_Mem_Acc_36_48)|=0) & (|marking(Ext_Mem_Acc_31_5)|=0) & (|marking(Ext_Mem_Acc_31_15)|=0) & (|marking(Ext_Mem_Acc_41_9)|=0) & (|marking(Ext_Mem_Acc_16_18)|=0) & (|marking(Ext_Mem_Acc_19_33)|=0) & (|marking(Ext_Mem_Acc_34_44)|=0) & (|marking(Ext_Mem_Acc_34_50)|=0) & (|marking(Ext_Mem_Acc_5_6)|=0) & (|marking(Ext_Mem_Acc_16_50)|=0) & (|marking(Ext_Mem_Acc_47_16)|=0) & (|marking(Ext_Mem_Acc_36_9)|=0) & (|marking(Ext_Mem_Acc_41_37)|=0) & (|marking(Ext_Mem_Acc_44_7)|=0) & (|marking(Ext_Mem_Acc_3_43)|=0) & (|marking(Ext_Mem_Acc_5_45)|=0) & (|marking(Ext_Mem_Acc_7_8)|=0) & (|marking(Ext_Mem_Acc_2_40)|=0) & (|marking(Ext_Mem_Acc_29_44)|=0)))
ctl p_1871_markingcomparison_full_and: E G (((true & (|marking(Active_29)|=0) & (|marking(Active_50)|=0) & (|marking(Active_38)|=0) & (|marking(Active_11)|=0) & (|marking(Active_8)|=0) & (|marking(Active_35)|=0) & (|marking(Active_26)|=0) & (|marking(Active_46)|=0) & (|marking(Active_22)|=0) & (|marking(Active_13)|=0) & (|marking(Active_33)|=0) & (|marking(Active_19)|=0) & (|marking(Active_3)|=0) & (|marking(Active_7)|=0) & (|marking(Active_15)|=0) & (|marking(Active_10)|=0) & (|marking(Active_43)|=0) & (|marking(Active_1)|=0) & (|marking(Active_47)|=0) & (|marking(Active_42)|=0) & (|marking(Active_44)|=0) & (|marking(Active_41)|=0) & (|marking(Active_18)|=0) & (|marking(Active_23)|=0) & (|marking(Active_4)|=0) & (|marking(Active_24)|=0) & (|marking(Active_21)|=0) & (|marking(Active_39)|=0) & (|marking(Active_49)|=0) & (|marking(Active_6)|=0) & (|marking(Active_28)|=0) & (|marking(Active_31)|=0) & (|marking(Active_9)|=0) & (|marking(Active_14)|=0) & (|marking(Active_32)|=0) & (|marking(Active_45)|=0) & (|marking(Active_16)|=0) & (|marking(Active_20)|=0) & (|marking(Active_40)|=0) & (|marking(Active_5)|=0) & (|marking(Active_27)|=0) & (|marking(Active_12)|=0) & (|marking(Active_2)|=0) & (|marking(Active_17)|=0) & (|marking(Active_34)|=0) & (|marking(Active_30)|=0) & (|marking(Active_48)|=0) & (|marking(Active_25)|=0) & (|marking(Active_37)|=0)) & (true & (1>|marking(Active_36)|))) & (((true) & (true & (1>|marking(Ext_Bus)|))) & ((false | (1>|marking(Ext_Bus)|)) | (false))))
ctl p_1872_markingcomparison_full_or: A G (((true & (|marking(Active_29)|=0) & (|marking(Active_50)|=0) & (|marking(Active_38)|=0) & (|marking(Active_11)|=0) & (|marking(Active_8)|=0) & (|marking(Active_35)|=0) & (|marking(Active_26)|=0) & (|marking(Active_46)|=0) & (|marking(Active_22)|=0) & (|marking(Active_13)|=0) & (|marking(Active_33)|=0) & (|marking(Active_19)|=0) & (|marking(Active_3)|=0) & (|marking(Active_7)|=0) & (|marking(Active_15)|=0) & (|marking(Active_10)|=0) & (|marking(Active_43)|=0) & (|marking(Active_1)|=0) & (|marking(Active_47)|=0) & (|marking(Active_42)|=0) & (|marking(Active_44)|=0) & (|marking(Active_41)|=0) & (|marking(Active_18)|=0) & (|marking(Active_23)|=0) & (|marking(Active_4)|=0) & (|marking(Active_24)|=0) & (|marking(Active_21)|=0) & (|marking(Active_39)|=0) & (|marking(Active_49)|=0) & (|marking(Active_6)|=0) & (|marking(Active_28)|=0) & (|marking(Active_31)|=0) & (|marking(Active_9)|=0) & (|marking(Active_14)|=0) & (|marking(Active_32)|=0) & (|marking(Active_45)|=0) & (|marking(Active_16)|=0) & (|marking(Active_20)|=0) & (|marking(Active_40)|=0) & (|marking(Active_5)|=0) & (|marking(Active_27)|=0) & (|marking(Active_12)|=0) & (|marking(Active_2)|=0) & (|marking(Active_17)|=0) & (|marking(Active_34)|=0) & (|marking(Active_30)|=0) & (|marking(Active_48)|=0) & (|marking(Active_25)|=0) & (|marking(Active_37)|=0)) & (true & (1>|marking(Active_36)|))) | (((true) & (true & (1>|marking(Ext_Bus)|))) & ((false | (1>|marking(Ext_Bus)|)) | (false))))
ctl p_1873_markingcomparison_full_and_notx: E F (((true & (|marking(Active_29)|=0) & (|marking(Active_50)|=0) & (|marking(Active_38)|=0) & (|marking(Active_11)|=0) & (|marking(Active_8)|=0) & (|marking(Active_35)|=0) & (|marking(Active_26)|=0) & (|marking(Active_46)|=0) & (|marking(Active_22)|=0) & (|marking(Active_13)|=0) & (|marking(Active_33)|=0) & (|marking(Active_19)|=0) & (|marking(Active_3)|=0) & (|marking(Active_7)|=0) & (|marking(Active_15)|=0) & (|marking(Active_10)|=0) & (|marking(Active_43)|=0) & (|marking(Active_1)|=0) & (|marking(Active_47)|=0) & (|marking(Active_42)|=0) & (|marking(Active_44)|=0) & (|marking(Active_41)|=0) & (|marking(Active_18)|=0) & (|marking(Active_23)|=0) & (|marking(Active_4)|=0) & (|marking(Active_24)|=0) & (|marking(Active_21)|=0) & (|marking(Active_39)|=0) & (|marking(Active_49)|=0) & (|marking(Active_6)|=0) & (|marking(Active_28)|=0) & (|marking(Active_31)|=0) & (|marking(Active_9)|=0) & (|marking(Active_14)|=0) & (|marking(Active_32)|=0) & (|marking(Active_45)|=0) & (|marking(Active_16)|=0) & (|marking(Active_20)|=0) & (|marking(Active_40)|=0) & (|marking(Active_5)|=0) & (|marking(Active_27)|=0) & (|marking(Active_12)|=0) & (|marking(Active_2)|=0) & (|marking(Active_17)|=0) & (|marking(Active_34)|=0) & (|marking(Active_30)|=0) & (|marking(Active_48)|=0) & (|marking(Active_25)|=0) & (|marking(Active_37)|=0)) & (true & (1>|marking(Active_36)|))) & (((true) & (true & (1>|marking(Ext_Bus)|))) & ((false | (1>|marking(Ext_Bus)|)) | (false))))


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