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

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

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

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

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

START 1369845514

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: 461 NrTr: 820)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369845515

--------------------
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: A F (A G (true & (1=|marking(Ext_Bus)|)) <=> X (true & (1!=|marking(Active_8)|) & (|marking(Active_7)|!=0) & (|marking(Active_6)|!=0) & (|marking(Active_1)|!=0) & (|marking(Active_9)|!=0) & (|marking(Active_4)|!=0) & (|marking(Active_3)|!=0) & (|marking(Active_13)|!=0) & (|marking(Active_20)|!=0) & (|marking(Active_2)|!=0) & (|marking(Active_14)|!=0) & (|marking(Active_12)|!=0) & (|marking(Active_17)|!=0) & (|marking(Active_10)|!=0) & (|marking(Active_19)|!=0) & (|marking(Active_5)|!=0) & (|marking(Active_11)|!=0) & (|marking(Active_18)|!=0) & (|marking(Active_15)|!=0) & (|marking(Active_16)|!=0)))
ctl p_1871_markingcomparison_full_and: A F ((((true & (|marking(Ext_Mem_Acc_15_1)|=0) & (|marking(Ext_Mem_Acc_4_13)|=0) & (|marking(Ext_Mem_Acc_2_13)|=0) & (|marking(Ext_Mem_Acc_4_16)|=0) & (|marking(Ext_Mem_Acc_9_12)|=0) & (|marking(Ext_Mem_Acc_13_5)|=0) & (|marking(Ext_Mem_Acc_18_2)|=0) & (|marking(Ext_Mem_Acc_15_19)|=0) & (|marking(Ext_Mem_Acc_8_3)|=0) & (|marking(Ext_Mem_Acc_13_12)|=0) & (|marking(Ext_Mem_Acc_6_14)|=0) & (|marking(Ext_Mem_Acc_9_15)|=0) & (|marking(Ext_Mem_Acc_10_5)|=0) & (|marking(Ext_Mem_Acc_4_8)|=0) & (|marking(Ext_Mem_Acc_18_15)|=0) & (|marking(Ext_Mem_Acc_2_17)|=0) & (|marking(Ext_Mem_Acc_6_19)|=0) & (|marking(Ext_Mem_Acc_18_5)|=0) & (|marking(Ext_Mem_Acc_13_8)|=0) & (|marking(Ext_Mem_Acc_16_12)|=0) & (|marking(Ext_Mem_Acc_9_19)|=0) & (|marking(Ext_Mem_Acc_9_2)|=0) & (|marking(Ext_Mem_Acc_19_8)|=0) & (|marking(Ext_Mem_Acc_6_15)|=0) & (|marking(Ext_Mem_Acc_1_8)|=0) & (|marking(Ext_Mem_Acc_4_3)|=0) & (|marking(Ext_Mem_Acc_10_17)|=0) & (|marking(Ext_Mem_Acc_12_7)|=0) & (|marking(Ext_Mem_Acc_2_1)|=0) & (|marking(Ext_Mem_Acc_17_15)|=0) & (|marking(Ext_Mem_Acc_3_10)|=0) & (|marking(Ext_Mem_Acc_9_8)|=0) & (|marking(Ext_Mem_Acc_6_11)|=0) & (|marking(Ext_Mem_Acc_1_14)|=0) & (|marking(Ext_Mem_Acc_5_3)|=0) & (|marking(Ext_Mem_Acc_17_20)|=0) & (|marking(Ext_Mem_Acc_12_3)|=0) & (|marking(Ext_Mem_Acc_20_12)|=0) & (|marking(Ext_Mem_Acc_19_2)|=0) & (|marking(Ext_Mem_Acc_5_12)|=0) & (|marking(Ext_Mem_Acc_2_9)|=0) & (|marking(Ext_Mem_Acc_18_17)|=0) & (|marking(Ext_Mem_Acc_19_18)|=0) & (|marking(Ext_Mem_Acc_19_13)|=0) & (|marking(Ext_Mem_Acc_3_8)|=0) & (|marking(Ext_Mem_Acc_3_19)|=0) & (|marking(Ext_Mem_Acc_10_14)|=0) & (|marking(Ext_Mem_Acc_16_20)|=0) & (|marking(Ext_Mem_Acc_15_4)|=0) & (|marking(Ext_Mem_Acc_16_9)|=0) & (|marking(Ext_Mem_Acc_14_8)|=0) & (|marking(Ext_Mem_Acc_8_1)|=0) & (|marking(Ext_Mem_Acc_20_19)|=0) & (|marking(Ext_Mem_Acc_3_13)|=0) & (|marking(Ext_Mem_Acc_19_5)|=0) & (|marking(Ext_Mem_Acc_11_17)|=0) & (|marking(Ext_Mem_Acc_11_13)|=0) & (|marking(Ext_Mem_Acc_20_2)|=0) & (|marking(Ext_Mem_Acc_8_7)|=0) & (|marking(Ext_Mem_Acc_18_1)|=0) & (|marking(Ext_Mem_Acc_15_2)|=0) & (|marking(Ext_Mem_Acc_19_9)|=0) & (|marking(Ext_Mem_Acc_18_9)|=0) & (|marking(Ext_Mem_Acc_10_4)|=0) & (|marking(Ext_Mem_Acc_13_15)|=0) & (|marking(Ext_Mem_Acc_12_9)|=0) & (|marking(Ext_Mem_Acc_12_4)|=0) & (|marking(Ext_Mem_Acc_11_20)|=0) & (|marking(Ext_Mem_Acc_2_19)|=0) & (|marking(Ext_Mem_Acc_12_5)|=0) & (|marking(Ext_Mem_Acc_9_4)|=0) & (|marking(Ext_Mem_Acc_20_13)|=0) & (|marking(Ext_Mem_Acc_5_9)|=0) & (|marking(Ext_Mem_Acc_13_17)|=0) & (|marking(Ext_Mem_Acc_20_1)|=0) & (|marking(Ext_Mem_Acc_10_1)|=0) & (|marking(Ext_Mem_Acc_17_12)|=0) & (|marking(Ext_Mem_Acc_4_17)|=0) & (|marking(Ext_Mem_Acc_9_5)|=0) & (|marking(Ext_Mem_Acc_20_7)|=0) & (|marking(Ext_Mem_Acc_3_5)|=0) & (|marking(Ext_Mem_Acc_11_16)|=0) & (|marking(Ext_Mem_Acc_4_11)|=0) & (|marking(Ext_Mem_Acc_2_10)|=0) & (|marking(Ext_Mem_Acc_1_4)|=0) & (|marking(Ext_Mem_Acc_16_2)|=0) & (|marking(Ext_Mem_Acc_19_14)|=0) & (|marking(Ext_Mem_Acc_1_7)|=0) & (|marking(Ext_Mem_Acc_9_3)|=0) & (|marking(Ext_Mem_Acc_1_10)|=0) & (|marking(Ext_Mem_Acc_6_13)|=0) & (|marking(Ext_Mem_Acc_11_5)|=0) & (|marking(Ext_Mem_Acc_2_11)|=0) & (|marking(Ext_Mem_Acc_8_4)|=0) & (|marking(Ext_Mem_Acc_5_17)|=0) & (|marking(Ext_Mem_Acc_1_11)|=0) & (|marking(Ext_Mem_Acc_11_1)|=0) & (|marking(Ext_Mem_Acc_14_12)|=0) & (|marking(Ext_Mem_Acc_19_1)|=0) & (|marking(Ext_Mem_Acc_8_6)|=0) & (|marking(Ext_Mem_Acc_15_5)|=0) & (|marking(Ext_Mem_Acc_18_10)|=0) & (|marking(Ext_Mem_Acc_4_5)|=0) & (|marking(Ext_Mem_Acc_12_8)|=0) & (|marking(Ext_Mem_Acc_7_1)|=0) & (|marking(Ext_Mem_Acc_8_14)|=0) & (|marking(Ext_Mem_Acc_8_15)|=0) & (|marking(Ext_Mem_Acc_6_17)|=0) & (|marking(Ext_Mem_Acc_11_19)|=0) & (|marking(Ext_Mem_Acc_15_9)|=0) & (|marking(Ext_Mem_Acc_10_18)|=0) & (|marking(Ext_Mem_Acc_4_18)|=0) & (|marking(Ext_Mem_Acc_15_17)|=0) & (|marking(Ext_Mem_Acc_16_19)|=0) & (|marking(Ext_Mem_Acc_17_11)|=0) & (|marking(Ext_Mem_Acc_12_1)|=0) & (|marking(Ext_Mem_Acc_10_9)|=0) & (|marking(Ext_Mem_Acc_13_10)|=0) & (|marking(Ext_Mem_Acc_7_11)|=0) & (|marking(Ext_Mem_Acc_11_4)|=0) & (|marking(Ext_Mem_Acc_3_7)|=0) & (|marking(Ext_Mem_Acc_17_3)|=0) & (|marking(Ext_Mem_Acc_2_15)|=0) & (|marking(Ext_Mem_Acc_16_17)|=0) & (|marking(Ext_Mem_Acc_20_14)|=0) & (|marking(Ext_Mem_Acc_19_20)|=0) & (|marking(Ext_Mem_Acc_20_11)|=0) & (|marking(Ext_Mem_Acc_11_3)|=0) & (|marking(Ext_Mem_Acc_1_12)|=0) & (|marking(Ext_Mem_Acc_15_11)|=0) & (|marking(Ext_Mem_Acc_6_10)|=0) & (|marking(Ext_Mem_Acc_7_6)|=0) & (|marking(Ext_Mem_Acc_1_18)|=0) & (|marking(Ext_Mem_Acc_10_3)|=0) & (|marking(Ext_Mem_Acc_7_16)|=0) & (|marking(Ext_Mem_Acc_18_6)|=0) & (|marking(Ext_Mem_Acc_15_8)|=0) & (|marking(Ext_Mem_Acc_15_6)|=0) & (|marking(Ext_Mem_Acc_5_6)|=0) & (|marking(Ext_Mem_Acc_13_7)|=0) & (|marking(Ext_Mem_Acc_2_20)|=0) & (|marking(Ext_Mem_Acc_7_10)|=0) & (|marking(Ext_Mem_Acc_16_18)|=0) & (|marking(Ext_Mem_Acc_9_16)|=0) & (|marking(Ext_Mem_Acc_5_13)|=0) & (|marking(Ext_Mem_Acc_19_6)|=0) & (|marking(Ext_Mem_Acc_20_16)|=0) & (|marking(Ext_Mem_Acc_8_18)|=0) & (|marking(Ext_Mem_Acc_14_13)|=0) & (|marking(Ext_Mem_Acc_9_7)|=0) & (|marking(Ext_Mem_Acc_4_20)|=0) & (|marking(Ext_Mem_Acc_8_9)|=0) & (|marking(Ext_Mem_Acc_8_16)|=0) & (|marking(Ext_Mem_Acc_11_7)|=0) & (|marking(Ext_Mem_Acc_3_12)|=0) & (|marking(Ext_Mem_Acc_12_20)|=0) & (|marking(Ext_Mem_Acc_13_18)|=0) & (|marking(Ext_Mem_Acc_10_7)|=0) & (|marking(Ext_Mem_Acc_1_13)|=0) & (|marking(Ext_Mem_Acc_15_10)|=0) & (|marking(Ext_Mem_Acc_16_8)|=0) & (|marking(Ext_Mem_Acc_17_5)|=0) & (|marking(Ext_Mem_Acc_3_18)|=0) & (|marking(Ext_Mem_Acc_6_2)|=0) & (|marking(Ext_Mem_Acc_20_10)|=0) & (|marking(Ext_Mem_Acc_13_16)|=0) & (|marking(Ext_Mem_Acc_8_11)|=0) & (|marking(Ext_Mem_Acc_12_6)|=0) & (|marking(Ext_Mem_Acc_5_15)|=0) & (|marking(Ext_Mem_Acc_17_10)|=0) & (|marking(Ext_Mem_Acc_4_12)|=0) & (|marking(Ext_Mem_Acc_17_7)|=0) & (|marking(Ext_Mem_Acc_14_17)|=0) & (|marking(Ext_Mem_Acc_5_1)|=0) & (|marking(Ext_Mem_Acc_4_19)|=0) & (|marking(Ext_Mem_Acc_9_6)|=0) & (|marking(Ext_Mem_Acc_17_2)|=0) & (|marking(Ext_Mem_Acc_16_13)|=0) & (|marking(Ext_Mem_Acc_5_7)|=0) & (|marking(Ext_Mem_Acc_1_9)|=0) & (|marking(Ext_Mem_Acc_6_16)|=0) & (|marking(Ext_Mem_Acc_1_2)|=0) & (|marking(Ext_Mem_Acc_10_16)|=0) & (|marking(Ext_Mem_Acc_4_2)|=0) & (|marking(Ext_Mem_Acc_12_16)|=0) & (|marking(Ext_Mem_Acc_2_3)|=0) & (|marking(Ext_Mem_Acc_16_3)|=0) & (|marking(Ext_Mem_Acc_15_18)|=0) & (|marking(Ext_Mem_Acc_20_4)|=0) & (|marking(Ext_Mem_Acc_2_18)|=0) & (|marking(Ext_Mem_Acc_2_14)|=0) & (|marking(Ext_Mem_Acc_11_6)|=0) & (|marking(Ext_Mem_Acc_18_13)|=0) & (|marking(Ext_Mem_Acc_14_5)|=0) & (|marking(Ext_Mem_Acc_18_8)|=0) & (|marking(Ext_Mem_Acc_15_12)|=0) & (|marking(Ext_Mem_Acc_9_10)|=0) & (|marking(Ext_Mem_Acc_7_20)|=0) & (|marking(Ext_Mem_Acc_12_11)|=0) & (|marking(Ext_Mem_Acc_12_2)|=0) & (|marking(Ext_Mem_Acc_18_16)|=0) & (|marking(Ext_Mem_Acc_3_16)|=0) & (|marking(Ext_Mem_Acc_16_11)|=0) & (|marking(Ext_Mem_Acc_6_5)|=0) & (|marking(Ext_Mem_Acc_7_17)|=0) & (|marking(Ext_Mem_Acc_13_9)|=0) & (|marking(Ext_Mem_Acc_18_3)|=0) & (|marking(Ext_Mem_Acc_16_14)|=0) & (|marking(Ext_Mem_Acc_19_16)|=0) & (|marking(Ext_Mem_Acc_14_16)|=0) & (|marking(Ext_Mem_Acc_12_19)|=0) & (|marking(Ext_Mem_Acc_3_4)|=0) & (|marking(Ext_Mem_Acc_3_15)|=0) & (|marking(Ext_Mem_Acc_17_13)|=0) & (|marking(Ext_Mem_Acc_7_2)|=0) & (|marking(Ext_Mem_Acc_1_16)|=0) & (|marking(Ext_Mem_Acc_12_17)|=0) & (|marking(Ext_Mem_Acc_4_6)|=0) & (|marking(Ext_Mem_Acc_16_6)|=0) & (|marking(Ext_Mem_Acc_9_17)|=0) & (|marking(Ext_Mem_Acc_11_9)|=0) & (|marking(Ext_Mem_Acc_10_6)|=0) & (|marking(Ext_Mem_Acc_8_10)|=0) & (|marking(Ext_Mem_Acc_6_20)|=0) & (|marking(Ext_Mem_Acc_5_19)|=0) & (|marking(Ext_Mem_Acc_4_14)|=0) & (|marking(Ext_Mem_Acc_13_2)|=0) & (|marking(Ext_Mem_Acc_11_12)|=0) & (|marking(Ext_Mem_Acc_17_16)|=0) & (|marking(Ext_Mem_Acc_9_1)|=0) & (|marking(Ext_Mem_Acc_3_20)|=0) & (|marking(Ext_Mem_Acc_7_9)|=0) & (|marking(Ext_Mem_Acc_10_19)|=0) & (|marking(Ext_Mem_Acc_17_8)|=0) & (|marking(Ext_Mem_Acc_5_10)|=0) & (|marking(Ext_Mem_Acc_11_15)|=0) & (|marking(Ext_Mem_Acc_1_19)|=0) & (|marking(Ext_Mem_Acc_7_19)|=0) & (|marking(Ext_Mem_Acc_14_10)|=0) & (|marking(Ext_Mem_Acc_20_17)|=0) & (|marking(Ext_Mem_Acc_17_4)|=0) & (|marking(Ext_Mem_Acc_9_13)|=0) & (|marking(Ext_Mem_Acc_18_4)|=0) & (|marking(Ext_Mem_Acc_8_2)|=0) & (|marking(Ext_Mem_Acc_10_13)|=0) & (|marking(Ext_Mem_Acc_19_17)|=0) & (|marking(Ext_Mem_Acc_2_7)|=0) & (|marking(Ext_Mem_Acc_14_1)|=0) & (|marking(Ext_Mem_Acc_7_12)|=0) & (|marking(Ext_Mem_Acc_1_17)|=0) & (|marking(Ext_Mem_Acc_10_11)|=0) & (|marking(Ext_Mem_Acc_10_2)|=0) & (|marking(Ext_Mem_Acc_14_2)|=0) & (|marking(Ext_Mem_Acc_8_17)|=0) & (|marking(Ext_Mem_Acc_13_3)|=0) & (|marking(Ext_Mem_Acc_8_5)|=0) & (|marking(Ext_Mem_Acc_19_3)|=0) & (|marking(Ext_Mem_Acc_18_7)|=0) & (|marking(Ext_Mem_Acc_4_10)|=0) & (|marking(Ext_Mem_Acc_11_18)|=0) & (|marking(Ext_Mem_Acc_15_7)|=0) & (|marking(Ext_Mem_Acc_16_4)|=0) & (|marking(Ext_Mem_Acc_2_6)|=0) & (|marking(Ext_Mem_Acc_15_13)|=0) & (|marking(Ext_Mem_Acc_3_2)|=0) & (|marking(Ext_Mem_Acc_8_20)|=0) & (|marking(Ext_Mem_Acc_17_18)|=0) & (|marking(Ext_Mem_Acc_19_11)|=0) & (|marking(Ext_Mem_Acc_6_3)|=0) & (|marking(Ext_Mem_Acc_20_8)|=0) & (|marking(Ext_Mem_Acc_8_13)|=0) & (|marking(Ext_Mem_Acc_6_1)|=0) & (|marking(Ext_Mem_Acc_10_15)|=0) & (|marking(Ext_Mem_Acc_4_9)|=0) & (|marking(Ext_Mem_Acc_3_11)|=0) & (|marking(Ext_Mem_Acc_15_16)|=0) & (|marking(Ext_Mem_Acc_1_20)|=0) & (|marking(Ext_Mem_Acc_20_15)|=0) & (|marking(Ext_Mem_Acc_13_19)|=0) & (|marking(Ext_Mem_Acc_13_6)|=0) & (|marking(Ext_Mem_Acc_5_4)|=0) & (|marking(Ext_Mem_Acc_1_5)|=0) & (|marking(Ext_Mem_Acc_6_18)|=0) & (|marking(Ext_Mem_Acc_6_9)|=0) & (|marking(Ext_Mem_Acc_9_11)|=0) & (|marking(Ext_Mem_Acc_16_10)|=0) & (|marking(Ext_Mem_Acc_7_14)|=0) & (|marking(Ext_Mem_Acc_14_4)|=0) & (|marking(Ext_Mem_Acc_3_1)|=0) & (|marking(Ext_Mem_Acc_18_11)|=0) & (|marking(Ext_Mem_Acc_3_14)|=0) & (|marking(Ext_Mem_Acc_15_14)|=0) & (|marking(Ext_Mem_Acc_1_6)|=0) & (|marking(Ext_Mem_Acc_2_4)|=0) & (|marking(Ext_Mem_Acc_20_9)|=0) & (|marking(Ext_Mem_Acc_9_20)|=0) & (|marking(Ext_Mem_Acc_18_19)|=0) & (|marking(Ext_Mem_Acc_11_2)|=0) & (|marking(Ext_Mem_Acc_2_5)|=0) & (|marking(Ext_Mem_Acc_1_3)|=0) & (|marking(Ext_Mem_Acc_9_14)|=0) & (|marking(Ext_Mem_Acc_7_15)|=0) & (|marking(Ext_Mem_Acc_5_11)|=0) & (|marking(Ext_Mem_Acc_7_5)|=0) & (|marking(Ext_Mem_Acc_6_8)|=0) & (|marking(Ext_Mem_Acc_12_14)|=0) & (|marking(Ext_Mem_Acc_12_18)|=0) & (|marking(Ext_Mem_Acc_6_7)|=0) & (|marking(Ext_Mem_Acc_17_1)|=0) & (|marking(Ext_Mem_Acc_4_1)|=0) & (|marking(Ext_Mem_Acc_11_8)|=0) & (|marking(Ext_Mem_Acc_6_4)|=0) & (|marking(Ext_Mem_Acc_10_12)|=0) & (|marking(Ext_Mem_Acc_5_20)|=0) & (|marking(Ext_Mem_Acc_4_15)|=0) & (|marking(Ext_Mem_Acc_12_13)|=0) & (|marking(Ext_Mem_Acc_19_10)|=0) & (|marking(Ext_Mem_Acc_19_15)|=0) & (|marking(Ext_Mem_Acc_16_5)|=0) & (|marking(Ext_Mem_Acc_14_18)|=0) & (|marking(Ext_Mem_Acc_6_12)|=0) & (|marking(Ext_Mem_Acc_20_18)|=0) & (|marking(Ext_Mem_Acc_14_11)|=0) & (|marking(Ext_Mem_Acc_19_4)|=0) & (|marking(Ext_Mem_Acc_2_12)|=0) & (|marking(Ext_Mem_Acc_11_14)|=0) & (|marking(Ext_Mem_Acc_3_6)|=0) & (|marking(Ext_Mem_Acc_7_13)|=0) & (|marking(Ext_Mem_Acc_5_8)|=0) & (|marking(Ext_Mem_Acc_13_20)|=0) & (|marking(Ext_Mem_Acc_5_18)|=0) & (|marking(Ext_Mem_Acc_10_20)|=0) & (|marking(Ext_Mem_Acc_12_10)|=0) & (|marking(Ext_Mem_Acc_5_16)|=0) & (|marking(Ext_Mem_Acc_14_3)|=0) & (|marking(Ext_Mem_Acc_7_3)|=0) & (|marking(Ext_Mem_Acc_7_18)|=0) & (|marking(Ext_Mem_Acc_8_12)|=0) & (|marking(Ext_Mem_Acc_2_8)|=0) & (|marking(Ext_Mem_Acc_14_15)|=0) & (|marking(Ext_Mem_Acc_14_6)|=0) & (|marking(Ext_Mem_Acc_20_5)|=0) & (|marking(Ext_Mem_Acc_5_14)|=0) & (|marking(Ext_Mem_Acc_14_7)|=0) & (|marking(Ext_Mem_Acc_11_10)|=0) & (|marking(Ext_Mem_Acc_9_18)|=0) & (|marking(Ext_Mem_Acc_13_11)|=0) & (|marking(Ext_Mem_Acc_13_4)|=0) & (|marking(Ext_Mem_Acc_17_14)|=0) & (|marking(Ext_Mem_Acc_18_14)|=0) & (|marking(Ext_Mem_Acc_3_17)|=0) & (|marking(Ext_Mem_Acc_17_19)|=0) & (|marking(Ext_Mem_Acc_20_6)|=0) & (|marking(Ext_Mem_Acc_19_12)|=0) & (|marking(Ext_Mem_Acc_19_7)|=0) & (|marking(Ext_Mem_Acc_18_12)|=0) & (|marking(Ext_Mem_Acc_1_15)|=0) & (|marking(Ext_Mem_Acc_10_8)|=0) & (|marking(Ext_Mem_Acc_5_2)|=0) & (|marking(Ext_Mem_Acc_14_9)|=0) & (|marking(Ext_Mem_Acc_3_9)|=0) & (|marking(Ext_Mem_Acc_7_8)|=0) & (|marking(Ext_Mem_Acc_17_9)|=0) & (|marking(Ext_Mem_Acc_16_7)|=0) & (|marking(Ext_Mem_Acc_20_3)|=0) & (|marking(Ext_Mem_Acc_12_15)|=0) & (|marking(Ext_Mem_Acc_8_19)|=0) & (|marking(Ext_Mem_Acc_13_1)|=0) & (|marking(Ext_Mem_Acc_15_20)|=0) & (|marking(Ext_Mem_Acc_15_3)|=0) & (|marking(Ext_Mem_Acc_18_20)|=0) & (|marking(Ext_Mem_Acc_17_6)|=0) & (|marking(Ext_Mem_Acc_4_7)|=0) & (|marking(Ext_Mem_Acc_16_1)|=0) & (|marking(Ext_Mem_Acc_16_15)|=0) & (|marking(Ext_Mem_Acc_14_19)|=0) & (|marking(Ext_Mem_Acc_7_4)|=0) & (|marking(Ext_Mem_Acc_14_20)|=0) & (|marking(Ext_Mem_Acc_13_14)|=0)) & (true & (1>|marking(Ext_Mem_Acc_2_16)|))) & ((false | (1>|marking(Ext_Mem_Acc_2_16)|)) | (false))) & (true & (1=|marking(Ext_Bus)|)))
ctl p_1872_markingcomparison_full_or: E F ((((true & (|marking(Ext_Mem_Acc_15_1)|=0) & (|marking(Ext_Mem_Acc_4_13)|=0) & (|marking(Ext_Mem_Acc_2_13)|=0) & (|marking(Ext_Mem_Acc_4_16)|=0) & (|marking(Ext_Mem_Acc_9_12)|=0) & (|marking(Ext_Mem_Acc_13_5)|=0) & (|marking(Ext_Mem_Acc_18_2)|=0) & (|marking(Ext_Mem_Acc_15_19)|=0) & (|marking(Ext_Mem_Acc_8_3)|=0) & (|marking(Ext_Mem_Acc_13_12)|=0) & (|marking(Ext_Mem_Acc_6_14)|=0) & (|marking(Ext_Mem_Acc_9_15)|=0) & (|marking(Ext_Mem_Acc_10_5)|=0) & (|marking(Ext_Mem_Acc_4_8)|=0) & (|marking(Ext_Mem_Acc_18_15)|=0) & (|marking(Ext_Mem_Acc_2_17)|=0) & (|marking(Ext_Mem_Acc_6_19)|=0) & (|marking(Ext_Mem_Acc_18_5)|=0) & (|marking(Ext_Mem_Acc_13_8)|=0) & (|marking(Ext_Mem_Acc_16_12)|=0) & (|marking(Ext_Mem_Acc_9_19)|=0) & (|marking(Ext_Mem_Acc_9_2)|=0) & (|marking(Ext_Mem_Acc_19_8)|=0) & (|marking(Ext_Mem_Acc_6_15)|=0) & (|marking(Ext_Mem_Acc_1_8)|=0) & (|marking(Ext_Mem_Acc_4_3)|=0) & (|marking(Ext_Mem_Acc_10_17)|=0) & (|marking(Ext_Mem_Acc_12_7)|=0) & (|marking(Ext_Mem_Acc_2_1)|=0) & (|marking(Ext_Mem_Acc_17_15)|=0) & (|marking(Ext_Mem_Acc_3_10)|=0) & (|marking(Ext_Mem_Acc_9_8)|=0) & (|marking(Ext_Mem_Acc_6_11)|=0) & (|marking(Ext_Mem_Acc_1_14)|=0) & (|marking(Ext_Mem_Acc_5_3)|=0) & (|marking(Ext_Mem_Acc_17_20)|=0) & (|marking(Ext_Mem_Acc_12_3)|=0) & (|marking(Ext_Mem_Acc_20_12)|=0) & (|marking(Ext_Mem_Acc_19_2)|=0) & (|marking(Ext_Mem_Acc_5_12)|=0) & (|marking(Ext_Mem_Acc_2_9)|=0) & (|marking(Ext_Mem_Acc_18_17)|=0) & (|marking(Ext_Mem_Acc_19_18)|=0) & (|marking(Ext_Mem_Acc_19_13)|=0) & (|marking(Ext_Mem_Acc_3_8)|=0) & (|marking(Ext_Mem_Acc_3_19)|=0) & (|marking(Ext_Mem_Acc_10_14)|=0) & (|marking(Ext_Mem_Acc_16_20)|=0) & (|marking(Ext_Mem_Acc_15_4)|=0) & (|marking(Ext_Mem_Acc_16_9)|=0) & (|marking(Ext_Mem_Acc_14_8)|=0) & (|marking(Ext_Mem_Acc_8_1)|=0) & (|marking(Ext_Mem_Acc_20_19)|=0) & (|marking(Ext_Mem_Acc_3_13)|=0) & (|marking(Ext_Mem_Acc_19_5)|=0) & (|marking(Ext_Mem_Acc_11_17)|=0) & (|marking(Ext_Mem_Acc_11_13)|=0) & (|marking(Ext_Mem_Acc_20_2)|=0) & (|marking(Ext_Mem_Acc_8_7)|=0) & (|marking(Ext_Mem_Acc_18_1)|=0) & (|marking(Ext_Mem_Acc_15_2)|=0) & (|marking(Ext_Mem_Acc_19_9)|=0) & (|marking(Ext_Mem_Acc_18_9)|=0) & (|marking(Ext_Mem_Acc_10_4)|=0) & (|marking(Ext_Mem_Acc_13_15)|=0) & (|marking(Ext_Mem_Acc_12_9)|=0) & (|marking(Ext_Mem_Acc_12_4)|=0) & (|marking(Ext_Mem_Acc_11_20)|=0) & (|marking(Ext_Mem_Acc_2_19)|=0) & (|marking(Ext_Mem_Acc_12_5)|=0) & (|marking(Ext_Mem_Acc_9_4)|=0) & (|marking(Ext_Mem_Acc_20_13)|=0) & (|marking(Ext_Mem_Acc_5_9)|=0) & (|marking(Ext_Mem_Acc_13_17)|=0) & (|marking(Ext_Mem_Acc_20_1)|=0) & (|marking(Ext_Mem_Acc_10_1)|=0) & (|marking(Ext_Mem_Acc_17_12)|=0) & (|marking(Ext_Mem_Acc_4_17)|=0) & (|marking(Ext_Mem_Acc_9_5)|=0) & (|marking(Ext_Mem_Acc_20_7)|=0) & (|marking(Ext_Mem_Acc_3_5)|=0) & (|marking(Ext_Mem_Acc_11_16)|=0) & (|marking(Ext_Mem_Acc_4_11)|=0) & (|marking(Ext_Mem_Acc_2_10)|=0) & (|marking(Ext_Mem_Acc_1_4)|=0) & (|marking(Ext_Mem_Acc_16_2)|=0) & (|marking(Ext_Mem_Acc_19_14)|=0) & (|marking(Ext_Mem_Acc_1_7)|=0) & (|marking(Ext_Mem_Acc_9_3)|=0) & (|marking(Ext_Mem_Acc_1_10)|=0) & (|marking(Ext_Mem_Acc_6_13)|=0) & (|marking(Ext_Mem_Acc_11_5)|=0) & (|marking(Ext_Mem_Acc_2_11)|=0) & (|marking(Ext_Mem_Acc_8_4)|=0) & (|marking(Ext_Mem_Acc_5_17)|=0) & (|marking(Ext_Mem_Acc_1_11)|=0) & (|marking(Ext_Mem_Acc_11_1)|=0) & (|marking(Ext_Mem_Acc_14_12)|=0) & (|marking(Ext_Mem_Acc_19_1)|=0) & (|marking(Ext_Mem_Acc_8_6)|=0) & (|marking(Ext_Mem_Acc_15_5)|=0) & (|marking(Ext_Mem_Acc_18_10)|=0) & (|marking(Ext_Mem_Acc_4_5)|=0) & (|marking(Ext_Mem_Acc_12_8)|=0) & (|marking(Ext_Mem_Acc_7_1)|=0) & (|marking(Ext_Mem_Acc_8_14)|=0) & (|marking(Ext_Mem_Acc_8_15)|=0) & (|marking(Ext_Mem_Acc_6_17)|=0) & (|marking(Ext_Mem_Acc_11_19)|=0) & (|marking(Ext_Mem_Acc_15_9)|=0) & (|marking(Ext_Mem_Acc_10_18)|=0) & (|marking(Ext_Mem_Acc_4_18)|=0) & (|marking(Ext_Mem_Acc_15_17)|=0) & (|marking(Ext_Mem_Acc_16_19)|=0) & (|marking(Ext_Mem_Acc_17_11)|=0) & (|marking(Ext_Mem_Acc_12_1)|=0) & (|marking(Ext_Mem_Acc_10_9)|=0) & (|marking(Ext_Mem_Acc_13_10)|=0) & (|marking(Ext_Mem_Acc_7_11)|=0) & (|marking(Ext_Mem_Acc_11_4)|=0) & (|marking(Ext_Mem_Acc_3_7)|=0) & (|marking(Ext_Mem_Acc_17_3)|=0) & (|marking(Ext_Mem_Acc_2_15)|=0) & (|marking(Ext_Mem_Acc_16_17)|=0) & (|marking(Ext_Mem_Acc_20_14)|=0) & (|marking(Ext_Mem_Acc_19_20)|=0) & (|marking(Ext_Mem_Acc_20_11)|=0) & (|marking(Ext_Mem_Acc_11_3)|=0) & (|marking(Ext_Mem_Acc_1_12)|=0) & (|marking(Ext_Mem_Acc_15_11)|=0) & (|marking(Ext_Mem_Acc_6_10)|=0) & (|marking(Ext_Mem_Acc_7_6)|=0) & (|marking(Ext_Mem_Acc_1_18)|=0) & (|marking(Ext_Mem_Acc_10_3)|=0) & (|marking(Ext_Mem_Acc_7_16)|=0) & (|marking(Ext_Mem_Acc_18_6)|=0) & (|marking(Ext_Mem_Acc_15_8)|=0) & (|marking(Ext_Mem_Acc_15_6)|=0) & (|marking(Ext_Mem_Acc_5_6)|=0) & (|marking(Ext_Mem_Acc_13_7)|=0) & (|marking(Ext_Mem_Acc_2_20)|=0) & (|marking(Ext_Mem_Acc_7_10)|=0) & (|marking(Ext_Mem_Acc_16_18)|=0) & (|marking(Ext_Mem_Acc_9_16)|=0) & (|marking(Ext_Mem_Acc_5_13)|=0) & (|marking(Ext_Mem_Acc_19_6)|=0) & (|marking(Ext_Mem_Acc_20_16)|=0) & (|marking(Ext_Mem_Acc_8_18)|=0) & (|marking(Ext_Mem_Acc_14_13)|=0) & (|marking(Ext_Mem_Acc_9_7)|=0) & (|marking(Ext_Mem_Acc_4_20)|=0) & (|marking(Ext_Mem_Acc_8_9)|=0) & (|marking(Ext_Mem_Acc_8_16)|=0) & (|marking(Ext_Mem_Acc_11_7)|=0) & (|marking(Ext_Mem_Acc_3_12)|=0) & (|marking(Ext_Mem_Acc_12_20)|=0) & (|marking(Ext_Mem_Acc_13_18)|=0) & (|marking(Ext_Mem_Acc_10_7)|=0) & (|marking(Ext_Mem_Acc_1_13)|=0) & (|marking(Ext_Mem_Acc_15_10)|=0) & (|marking(Ext_Mem_Acc_16_8)|=0) & (|marking(Ext_Mem_Acc_17_5)|=0) & (|marking(Ext_Mem_Acc_3_18)|=0) & (|marking(Ext_Mem_Acc_6_2)|=0) & (|marking(Ext_Mem_Acc_20_10)|=0) & (|marking(Ext_Mem_Acc_13_16)|=0) & (|marking(Ext_Mem_Acc_8_11)|=0) & (|marking(Ext_Mem_Acc_12_6)|=0) & (|marking(Ext_Mem_Acc_5_15)|=0) & (|marking(Ext_Mem_Acc_17_10)|=0) & (|marking(Ext_Mem_Acc_4_12)|=0) & (|marking(Ext_Mem_Acc_17_7)|=0) & (|marking(Ext_Mem_Acc_14_17)|=0) & (|marking(Ext_Mem_Acc_5_1)|=0) & (|marking(Ext_Mem_Acc_4_19)|=0) & (|marking(Ext_Mem_Acc_9_6)|=0) & (|marking(Ext_Mem_Acc_17_2)|=0) & (|marking(Ext_Mem_Acc_16_13)|=0) & (|marking(Ext_Mem_Acc_5_7)|=0) & (|marking(Ext_Mem_Acc_1_9)|=0) & (|marking(Ext_Mem_Acc_6_16)|=0) & (|marking(Ext_Mem_Acc_1_2)|=0) & (|marking(Ext_Mem_Acc_10_16)|=0) & (|marking(Ext_Mem_Acc_4_2)|=0) & (|marking(Ext_Mem_Acc_12_16)|=0) & (|marking(Ext_Mem_Acc_2_3)|=0) & (|marking(Ext_Mem_Acc_16_3)|=0) & (|marking(Ext_Mem_Acc_15_18)|=0) & (|marking(Ext_Mem_Acc_20_4)|=0) & (|marking(Ext_Mem_Acc_2_18)|=0) & (|marking(Ext_Mem_Acc_2_14)|=0) & (|marking(Ext_Mem_Acc_11_6)|=0) & (|marking(Ext_Mem_Acc_18_13)|=0) & (|marking(Ext_Mem_Acc_14_5)|=0) & (|marking(Ext_Mem_Acc_18_8)|=0) & (|marking(Ext_Mem_Acc_15_12)|=0) & (|marking(Ext_Mem_Acc_9_10)|=0) & (|marking(Ext_Mem_Acc_7_20)|=0) & (|marking(Ext_Mem_Acc_12_11)|=0) & (|marking(Ext_Mem_Acc_12_2)|=0) & (|marking(Ext_Mem_Acc_18_16)|=0) & (|marking(Ext_Mem_Acc_3_16)|=0) & (|marking(Ext_Mem_Acc_16_11)|=0) & (|marking(Ext_Mem_Acc_6_5)|=0) & (|marking(Ext_Mem_Acc_7_17)|=0) & (|marking(Ext_Mem_Acc_13_9)|=0) & (|marking(Ext_Mem_Acc_18_3)|=0) & (|marking(Ext_Mem_Acc_16_14)|=0) & (|marking(Ext_Mem_Acc_19_16)|=0) & (|marking(Ext_Mem_Acc_14_16)|=0) & (|marking(Ext_Mem_Acc_12_19)|=0) & (|marking(Ext_Mem_Acc_3_4)|=0) & (|marking(Ext_Mem_Acc_3_15)|=0) & (|marking(Ext_Mem_Acc_17_13)|=0) & (|marking(Ext_Mem_Acc_7_2)|=0) & (|marking(Ext_Mem_Acc_1_16)|=0) & (|marking(Ext_Mem_Acc_12_17)|=0) & (|marking(Ext_Mem_Acc_4_6)|=0) & (|marking(Ext_Mem_Acc_16_6)|=0) & (|marking(Ext_Mem_Acc_9_17)|=0) & (|marking(Ext_Mem_Acc_11_9)|=0) & (|marking(Ext_Mem_Acc_10_6)|=0) & (|marking(Ext_Mem_Acc_8_10)|=0) & (|marking(Ext_Mem_Acc_6_20)|=0) & (|marking(Ext_Mem_Acc_5_19)|=0) & (|marking(Ext_Mem_Acc_4_14)|=0) & (|marking(Ext_Mem_Acc_13_2)|=0) & (|marking(Ext_Mem_Acc_11_12)|=0) & (|marking(Ext_Mem_Acc_17_16)|=0) & (|marking(Ext_Mem_Acc_9_1)|=0) & (|marking(Ext_Mem_Acc_3_20)|=0) & (|marking(Ext_Mem_Acc_7_9)|=0) & (|marking(Ext_Mem_Acc_10_19)|=0) & (|marking(Ext_Mem_Acc_17_8)|=0) & (|marking(Ext_Mem_Acc_5_10)|=0) & (|marking(Ext_Mem_Acc_11_15)|=0) & (|marking(Ext_Mem_Acc_1_19)|=0) & (|marking(Ext_Mem_Acc_7_19)|=0) & (|marking(Ext_Mem_Acc_14_10)|=0) & (|marking(Ext_Mem_Acc_20_17)|=0) & (|marking(Ext_Mem_Acc_17_4)|=0) & (|marking(Ext_Mem_Acc_9_13)|=0) & (|marking(Ext_Mem_Acc_18_4)|=0) & (|marking(Ext_Mem_Acc_8_2)|=0) & (|marking(Ext_Mem_Acc_10_13)|=0) & (|marking(Ext_Mem_Acc_19_17)|=0) & (|marking(Ext_Mem_Acc_2_7)|=0) & (|marking(Ext_Mem_Acc_14_1)|=0) & (|marking(Ext_Mem_Acc_7_12)|=0) & (|marking(Ext_Mem_Acc_1_17)|=0) & (|marking(Ext_Mem_Acc_10_11)|=0) & (|marking(Ext_Mem_Acc_10_2)|=0) & (|marking(Ext_Mem_Acc_14_2)|=0) & (|marking(Ext_Mem_Acc_8_17)|=0) & (|marking(Ext_Mem_Acc_13_3)|=0) & (|marking(Ext_Mem_Acc_8_5)|=0) & (|marking(Ext_Mem_Acc_19_3)|=0) & (|marking(Ext_Mem_Acc_18_7)|=0) & (|marking(Ext_Mem_Acc_4_10)|=0) & (|marking(Ext_Mem_Acc_11_18)|=0) & (|marking(Ext_Mem_Acc_15_7)|=0) & (|marking(Ext_Mem_Acc_16_4)|=0) & (|marking(Ext_Mem_Acc_2_6)|=0) & (|marking(Ext_Mem_Acc_15_13)|=0) & (|marking(Ext_Mem_Acc_3_2)|=0) & (|marking(Ext_Mem_Acc_8_20)|=0) & (|marking(Ext_Mem_Acc_17_18)|=0) & (|marking(Ext_Mem_Acc_19_11)|=0) & (|marking(Ext_Mem_Acc_6_3)|=0) & (|marking(Ext_Mem_Acc_20_8)|=0) & (|marking(Ext_Mem_Acc_8_13)|=0) & (|marking(Ext_Mem_Acc_6_1)|=0) & (|marking(Ext_Mem_Acc_10_15)|=0) & (|marking(Ext_Mem_Acc_4_9)|=0) & (|marking(Ext_Mem_Acc_3_11)|=0) & (|marking(Ext_Mem_Acc_15_16)|=0) & (|marking(Ext_Mem_Acc_1_20)|=0) & (|marking(Ext_Mem_Acc_20_15)|=0) & (|marking(Ext_Mem_Acc_13_19)|=0) & (|marking(Ext_Mem_Acc_13_6)|=0) & (|marking(Ext_Mem_Acc_5_4)|=0) & (|marking(Ext_Mem_Acc_1_5)|=0) & (|marking(Ext_Mem_Acc_6_18)|=0) & (|marking(Ext_Mem_Acc_6_9)|=0) & (|marking(Ext_Mem_Acc_9_11)|=0) & (|marking(Ext_Mem_Acc_16_10)|=0) & (|marking(Ext_Mem_Acc_7_14)|=0) & (|marking(Ext_Mem_Acc_14_4)|=0) & (|marking(Ext_Mem_Acc_3_1)|=0) & (|marking(Ext_Mem_Acc_18_11)|=0) & (|marking(Ext_Mem_Acc_3_14)|=0) & (|marking(Ext_Mem_Acc_15_14)|=0) & (|marking(Ext_Mem_Acc_1_6)|=0) & (|marking(Ext_Mem_Acc_2_4)|=0) & (|marking(Ext_Mem_Acc_20_9)|=0) & (|marking(Ext_Mem_Acc_9_20)|=0) & (|marking(Ext_Mem_Acc_18_19)|=0) & (|marking(Ext_Mem_Acc_11_2)|=0) & (|marking(Ext_Mem_Acc_2_5)|=0) & (|marking(Ext_Mem_Acc_1_3)|=0) & (|marking(Ext_Mem_Acc_9_14)|=0) & (|marking(Ext_Mem_Acc_7_15)|=0) & (|marking(Ext_Mem_Acc_5_11)|=0) & (|marking(Ext_Mem_Acc_7_5)|=0) & (|marking(Ext_Mem_Acc_6_8)|=0) & (|marking(Ext_Mem_Acc_12_14)|=0) & (|marking(Ext_Mem_Acc_12_18)|=0) & (|marking(Ext_Mem_Acc_6_7)|=0) & (|marking(Ext_Mem_Acc_17_1)|=0) & (|marking(Ext_Mem_Acc_4_1)|=0) & (|marking(Ext_Mem_Acc_11_8)|=0) & (|marking(Ext_Mem_Acc_6_4)|=0) & (|marking(Ext_Mem_Acc_10_12)|=0) & (|marking(Ext_Mem_Acc_5_20)|=0) & (|marking(Ext_Mem_Acc_4_15)|=0) & (|marking(Ext_Mem_Acc_12_13)|=0) & (|marking(Ext_Mem_Acc_19_10)|=0) & (|marking(Ext_Mem_Acc_19_15)|=0) & (|marking(Ext_Mem_Acc_16_5)|=0) & (|marking(Ext_Mem_Acc_14_18)|=0) & (|marking(Ext_Mem_Acc_6_12)|=0) & (|marking(Ext_Mem_Acc_20_18)|=0) & (|marking(Ext_Mem_Acc_14_11)|=0) & (|marking(Ext_Mem_Acc_19_4)|=0) & (|marking(Ext_Mem_Acc_2_12)|=0) & (|marking(Ext_Mem_Acc_11_14)|=0) & (|marking(Ext_Mem_Acc_3_6)|=0) & (|marking(Ext_Mem_Acc_7_13)|=0) & (|marking(Ext_Mem_Acc_5_8)|=0) & (|marking(Ext_Mem_Acc_13_20)|=0) & (|marking(Ext_Mem_Acc_5_18)|=0) & (|marking(Ext_Mem_Acc_10_20)|=0) & (|marking(Ext_Mem_Acc_12_10)|=0) & (|marking(Ext_Mem_Acc_5_16)|=0) & (|marking(Ext_Mem_Acc_14_3)|=0) & (|marking(Ext_Mem_Acc_7_3)|=0) & (|marking(Ext_Mem_Acc_7_18)|=0) & (|marking(Ext_Mem_Acc_8_12)|=0) & (|marking(Ext_Mem_Acc_2_8)|=0) & (|marking(Ext_Mem_Acc_14_15)|=0) & (|marking(Ext_Mem_Acc_14_6)|=0) & (|marking(Ext_Mem_Acc_20_5)|=0) & (|marking(Ext_Mem_Acc_5_14)|=0) & (|marking(Ext_Mem_Acc_14_7)|=0) & (|marking(Ext_Mem_Acc_11_10)|=0) & (|marking(Ext_Mem_Acc_9_18)|=0) & (|marking(Ext_Mem_Acc_13_11)|=0) & (|marking(Ext_Mem_Acc_13_4)|=0) & (|marking(Ext_Mem_Acc_17_14)|=0) & (|marking(Ext_Mem_Acc_18_14)|=0) & (|marking(Ext_Mem_Acc_3_17)|=0) & (|marking(Ext_Mem_Acc_17_19)|=0) & (|marking(Ext_Mem_Acc_20_6)|=0) & (|marking(Ext_Mem_Acc_19_12)|=0) & (|marking(Ext_Mem_Acc_19_7)|=0) & (|marking(Ext_Mem_Acc_18_12)|=0) & (|marking(Ext_Mem_Acc_1_15)|=0) & (|marking(Ext_Mem_Acc_10_8)|=0) & (|marking(Ext_Mem_Acc_5_2)|=0) & (|marking(Ext_Mem_Acc_14_9)|=0) & (|marking(Ext_Mem_Acc_3_9)|=0) & (|marking(Ext_Mem_Acc_7_8)|=0) & (|marking(Ext_Mem_Acc_17_9)|=0) & (|marking(Ext_Mem_Acc_16_7)|=0) & (|marking(Ext_Mem_Acc_20_3)|=0) & (|marking(Ext_Mem_Acc_12_15)|=0) & (|marking(Ext_Mem_Acc_8_19)|=0) & (|marking(Ext_Mem_Acc_13_1)|=0) & (|marking(Ext_Mem_Acc_15_20)|=0) & (|marking(Ext_Mem_Acc_15_3)|=0) & (|marking(Ext_Mem_Acc_18_20)|=0) & (|marking(Ext_Mem_Acc_17_6)|=0) & (|marking(Ext_Mem_Acc_4_7)|=0) & (|marking(Ext_Mem_Acc_16_1)|=0) & (|marking(Ext_Mem_Acc_16_15)|=0) & (|marking(Ext_Mem_Acc_14_19)|=0) & (|marking(Ext_Mem_Acc_7_4)|=0) & (|marking(Ext_Mem_Acc_14_20)|=0) & (|marking(Ext_Mem_Acc_13_14)|=0)) & (true & (1>|marking(Ext_Mem_Acc_2_16)|))) & ((false | (1>|marking(Ext_Mem_Acc_2_16)|)) | (false))) | (true & (1=|marking(Ext_Bus)|)))
ctl p_1873_markingcomparison_full_and_notx: A G ((((true & (|marking(Ext_Mem_Acc_15_1)|=0) & (|marking(Ext_Mem_Acc_4_13)|=0) & (|marking(Ext_Mem_Acc_2_13)|=0) & (|marking(Ext_Mem_Acc_4_16)|=0) & (|marking(Ext_Mem_Acc_9_12)|=0) & (|marking(Ext_Mem_Acc_13_5)|=0) & (|marking(Ext_Mem_Acc_18_2)|=0) & (|marking(Ext_Mem_Acc_15_19)|=0) & (|marking(Ext_Mem_Acc_8_3)|=0) & (|marking(Ext_Mem_Acc_13_12)|=0) & (|marking(Ext_Mem_Acc_6_14)|=0) & (|marking(Ext_Mem_Acc_9_15)|=0) & (|marking(Ext_Mem_Acc_10_5)|=0) & (|marking(Ext_Mem_Acc_4_8)|=0) & (|marking(Ext_Mem_Acc_18_15)|=0) & (|marking(Ext_Mem_Acc_2_17)|=0) & (|marking(Ext_Mem_Acc_6_19)|=0) & (|marking(Ext_Mem_Acc_18_5)|=0) & (|marking(Ext_Mem_Acc_13_8)|=0) & (|marking(Ext_Mem_Acc_16_12)|=0) & (|marking(Ext_Mem_Acc_9_19)|=0) & (|marking(Ext_Mem_Acc_9_2)|=0) & (|marking(Ext_Mem_Acc_19_8)|=0) & (|marking(Ext_Mem_Acc_6_15)|=0) & (|marking(Ext_Mem_Acc_1_8)|=0) & (|marking(Ext_Mem_Acc_4_3)|=0) & (|marking(Ext_Mem_Acc_10_17)|=0) & (|marking(Ext_Mem_Acc_12_7)|=0) & (|marking(Ext_Mem_Acc_2_1)|=0) & (|marking(Ext_Mem_Acc_17_15)|=0) & (|marking(Ext_Mem_Acc_3_10)|=0) & (|marking(Ext_Mem_Acc_9_8)|=0) & (|marking(Ext_Mem_Acc_6_11)|=0) & (|marking(Ext_Mem_Acc_1_14)|=0) & (|marking(Ext_Mem_Acc_5_3)|=0) & (|marking(Ext_Mem_Acc_17_20)|=0) & (|marking(Ext_Mem_Acc_12_3)|=0) & (|marking(Ext_Mem_Acc_20_12)|=0) & (|marking(Ext_Mem_Acc_19_2)|=0) & (|marking(Ext_Mem_Acc_5_12)|=0) & (|marking(Ext_Mem_Acc_2_9)|=0) & (|marking(Ext_Mem_Acc_18_17)|=0) & (|marking(Ext_Mem_Acc_19_18)|=0) & (|marking(Ext_Mem_Acc_19_13)|=0) & (|marking(Ext_Mem_Acc_3_8)|=0) & (|marking(Ext_Mem_Acc_3_19)|=0) & (|marking(Ext_Mem_Acc_10_14)|=0) & (|marking(Ext_Mem_Acc_16_20)|=0) & (|marking(Ext_Mem_Acc_15_4)|=0) & (|marking(Ext_Mem_Acc_16_9)|=0) & (|marking(Ext_Mem_Acc_14_8)|=0) & (|marking(Ext_Mem_Acc_8_1)|=0) & (|marking(Ext_Mem_Acc_20_19)|=0) & (|marking(Ext_Mem_Acc_3_13)|=0) & (|marking(Ext_Mem_Acc_19_5)|=0) & (|marking(Ext_Mem_Acc_11_17)|=0) & (|marking(Ext_Mem_Acc_11_13)|=0) & (|marking(Ext_Mem_Acc_20_2)|=0) & (|marking(Ext_Mem_Acc_8_7)|=0) & (|marking(Ext_Mem_Acc_18_1)|=0) & (|marking(Ext_Mem_Acc_15_2)|=0) & (|marking(Ext_Mem_Acc_19_9)|=0) & (|marking(Ext_Mem_Acc_18_9)|=0) & (|marking(Ext_Mem_Acc_10_4)|=0) & (|marking(Ext_Mem_Acc_13_15)|=0) & (|marking(Ext_Mem_Acc_12_9)|=0) & (|marking(Ext_Mem_Acc_12_4)|=0) & (|marking(Ext_Mem_Acc_11_20)|=0) & (|marking(Ext_Mem_Acc_2_19)|=0) & (|marking(Ext_Mem_Acc_12_5)|=0) & (|marking(Ext_Mem_Acc_9_4)|=0) & (|marking(Ext_Mem_Acc_20_13)|=0) & (|marking(Ext_Mem_Acc_5_9)|=0) & (|marking(Ext_Mem_Acc_13_17)|=0) & (|marking(Ext_Mem_Acc_20_1)|=0) & (|marking(Ext_Mem_Acc_10_1)|=0) & (|marking(Ext_Mem_Acc_17_12)|=0) & (|marking(Ext_Mem_Acc_4_17)|=0) & (|marking(Ext_Mem_Acc_9_5)|=0) & (|marking(Ext_Mem_Acc_20_7)|=0) & (|marking(Ext_Mem_Acc_3_5)|=0) & (|marking(Ext_Mem_Acc_11_16)|=0) & (|marking(Ext_Mem_Acc_4_11)|=0) & (|marking(Ext_Mem_Acc_2_10)|=0) & (|marking(Ext_Mem_Acc_1_4)|=0) & (|marking(Ext_Mem_Acc_16_2)|=0) & (|marking(Ext_Mem_Acc_19_14)|=0) & (|marking(Ext_Mem_Acc_1_7)|=0) & (|marking(Ext_Mem_Acc_9_3)|=0) & (|marking(Ext_Mem_Acc_1_10)|=0) & (|marking(Ext_Mem_Acc_6_13)|=0) & (|marking(Ext_Mem_Acc_11_5)|=0) & (|marking(Ext_Mem_Acc_2_11)|=0) & (|marking(Ext_Mem_Acc_8_4)|=0) & (|marking(Ext_Mem_Acc_5_17)|=0) & (|marking(Ext_Mem_Acc_1_11)|=0) & (|marking(Ext_Mem_Acc_11_1)|=0) & (|marking(Ext_Mem_Acc_14_12)|=0) & (|marking(Ext_Mem_Acc_19_1)|=0) & (|marking(Ext_Mem_Acc_8_6)|=0) & (|marking(Ext_Mem_Acc_15_5)|=0) & (|marking(Ext_Mem_Acc_18_10)|=0) & (|marking(Ext_Mem_Acc_4_5)|=0) & (|marking(Ext_Mem_Acc_12_8)|=0) & (|marking(Ext_Mem_Acc_7_1)|=0) & (|marking(Ext_Mem_Acc_8_14)|=0) & (|marking(Ext_Mem_Acc_8_15)|=0) & (|marking(Ext_Mem_Acc_6_17)|=0) & (|marking(Ext_Mem_Acc_11_19)|=0) & (|marking(Ext_Mem_Acc_15_9)|=0) & (|marking(Ext_Mem_Acc_10_18)|=0) & (|marking(Ext_Mem_Acc_4_18)|=0) & (|marking(Ext_Mem_Acc_15_17)|=0) & (|marking(Ext_Mem_Acc_16_19)|=0) & (|marking(Ext_Mem_Acc_17_11)|=0) & (|marking(Ext_Mem_Acc_12_1)|=0) & (|marking(Ext_Mem_Acc_10_9)|=0) & (|marking(Ext_Mem_Acc_13_10)|=0) & (|marking(Ext_Mem_Acc_7_11)|=0) & (|marking(Ext_Mem_Acc_11_4)|=0) & (|marking(Ext_Mem_Acc_3_7)|=0) & (|marking(Ext_Mem_Acc_17_3)|=0) & (|marking(Ext_Mem_Acc_2_15)|=0) & (|marking(Ext_Mem_Acc_16_17)|=0) & (|marking(Ext_Mem_Acc_20_14)|=0) & (|marking(Ext_Mem_Acc_19_20)|=0) & (|marking(Ext_Mem_Acc_20_11)|=0) & (|marking(Ext_Mem_Acc_11_3)|=0) & (|marking(Ext_Mem_Acc_1_12)|=0) & (|marking(Ext_Mem_Acc_15_11)|=0) & (|marking(Ext_Mem_Acc_6_10)|=0) & (|marking(Ext_Mem_Acc_7_6)|=0) & (|marking(Ext_Mem_Acc_1_18)|=0) & (|marking(Ext_Mem_Acc_10_3)|=0) & (|marking(Ext_Mem_Acc_7_16)|=0) & (|marking(Ext_Mem_Acc_18_6)|=0) & (|marking(Ext_Mem_Acc_15_8)|=0) & (|marking(Ext_Mem_Acc_15_6)|=0) & (|marking(Ext_Mem_Acc_5_6)|=0) & (|marking(Ext_Mem_Acc_13_7)|=0) & (|marking(Ext_Mem_Acc_2_20)|=0) & (|marking(Ext_Mem_Acc_7_10)|=0) & (|marking(Ext_Mem_Acc_16_18)|=0) & (|marking(Ext_Mem_Acc_9_16)|=0) & (|marking(Ext_Mem_Acc_5_13)|=0) & (|marking(Ext_Mem_Acc_19_6)|=0) & (|marking(Ext_Mem_Acc_20_16)|=0) & (|marking(Ext_Mem_Acc_8_18)|=0) & (|marking(Ext_Mem_Acc_14_13)|=0) & (|marking(Ext_Mem_Acc_9_7)|=0) & (|marking(Ext_Mem_Acc_4_20)|=0) & (|marking(Ext_Mem_Acc_8_9)|=0) & (|marking(Ext_Mem_Acc_8_16)|=0) & (|marking(Ext_Mem_Acc_11_7)|=0) & (|marking(Ext_Mem_Acc_3_12)|=0) & (|marking(Ext_Mem_Acc_12_20)|=0) & (|marking(Ext_Mem_Acc_13_18)|=0) & (|marking(Ext_Mem_Acc_10_7)|=0) & (|marking(Ext_Mem_Acc_1_13)|=0) & (|marking(Ext_Mem_Acc_15_10)|=0) & (|marking(Ext_Mem_Acc_16_8)|=0) & (|marking(Ext_Mem_Acc_17_5)|=0) & (|marking(Ext_Mem_Acc_3_18)|=0) & (|marking(Ext_Mem_Acc_6_2)|=0) & (|marking(Ext_Mem_Acc_20_10)|=0) & (|marking(Ext_Mem_Acc_13_16)|=0) & (|marking(Ext_Mem_Acc_8_11)|=0) & (|marking(Ext_Mem_Acc_12_6)|=0) & (|marking(Ext_Mem_Acc_5_15)|=0) & (|marking(Ext_Mem_Acc_17_10)|=0) & (|marking(Ext_Mem_Acc_4_12)|=0) & (|marking(Ext_Mem_Acc_17_7)|=0) & (|marking(Ext_Mem_Acc_14_17)|=0) & (|marking(Ext_Mem_Acc_5_1)|=0) & (|marking(Ext_Mem_Acc_4_19)|=0) & (|marking(Ext_Mem_Acc_9_6)|=0) & (|marking(Ext_Mem_Acc_17_2)|=0) & (|marking(Ext_Mem_Acc_16_13)|=0) & (|marking(Ext_Mem_Acc_5_7)|=0) & (|marking(Ext_Mem_Acc_1_9)|=0) & (|marking(Ext_Mem_Acc_6_16)|=0) & (|marking(Ext_Mem_Acc_1_2)|=0) & (|marking(Ext_Mem_Acc_10_16)|=0) & (|marking(Ext_Mem_Acc_4_2)|=0) & (|marking(Ext_Mem_Acc_12_16)|=0) & (|marking(Ext_Mem_Acc_2_3)|=0) & (|marking(Ext_Mem_Acc_16_3)|=0) & (|marking(Ext_Mem_Acc_15_18)|=0) & (|marking(Ext_Mem_Acc_20_4)|=0) & (|marking(Ext_Mem_Acc_2_18)|=0) & (|marking(Ext_Mem_Acc_2_14)|=0) & (|marking(Ext_Mem_Acc_11_6)|=0) & (|marking(Ext_Mem_Acc_18_13)|=0) & (|marking(Ext_Mem_Acc_14_5)|=0) & (|marking(Ext_Mem_Acc_18_8)|=0) & (|marking(Ext_Mem_Acc_15_12)|=0) & (|marking(Ext_Mem_Acc_9_10)|=0) & (|marking(Ext_Mem_Acc_7_20)|=0) & (|marking(Ext_Mem_Acc_12_11)|=0) & (|marking(Ext_Mem_Acc_12_2)|=0) & (|marking(Ext_Mem_Acc_18_16)|=0) & (|marking(Ext_Mem_Acc_3_16)|=0) & (|marking(Ext_Mem_Acc_16_11)|=0) & (|marking(Ext_Mem_Acc_6_5)|=0) & (|marking(Ext_Mem_Acc_7_17)|=0) & (|marking(Ext_Mem_Acc_13_9)|=0) & (|marking(Ext_Mem_Acc_18_3)|=0) & (|marking(Ext_Mem_Acc_16_14)|=0) & (|marking(Ext_Mem_Acc_19_16)|=0) & (|marking(Ext_Mem_Acc_14_16)|=0) & (|marking(Ext_Mem_Acc_12_19)|=0) & (|marking(Ext_Mem_Acc_3_4)|=0) & (|marking(Ext_Mem_Acc_3_15)|=0) & (|marking(Ext_Mem_Acc_17_13)|=0) & (|marking(Ext_Mem_Acc_7_2)|=0) & (|marking(Ext_Mem_Acc_1_16)|=0) & (|marking(Ext_Mem_Acc_12_17)|=0) & (|marking(Ext_Mem_Acc_4_6)|=0) & (|marking(Ext_Mem_Acc_16_6)|=0) & (|marking(Ext_Mem_Acc_9_17)|=0) & (|marking(Ext_Mem_Acc_11_9)|=0) & (|marking(Ext_Mem_Acc_10_6)|=0) & (|marking(Ext_Mem_Acc_8_10)|=0) & (|marking(Ext_Mem_Acc_6_20)|=0) & (|marking(Ext_Mem_Acc_5_19)|=0) & (|marking(Ext_Mem_Acc_4_14)|=0) & (|marking(Ext_Mem_Acc_13_2)|=0) & (|marking(Ext_Mem_Acc_11_12)|=0) & (|marking(Ext_Mem_Acc_17_16)|=0) & (|marking(Ext_Mem_Acc_9_1)|=0) & (|marking(Ext_Mem_Acc_3_20)|=0) & (|marking(Ext_Mem_Acc_7_9)|=0) & (|marking(Ext_Mem_Acc_10_19)|=0) & (|marking(Ext_Mem_Acc_17_8)|=0) & (|marking(Ext_Mem_Acc_5_10)|=0) & (|marking(Ext_Mem_Acc_11_15)|=0) & (|marking(Ext_Mem_Acc_1_19)|=0) & (|marking(Ext_Mem_Acc_7_19)|=0) & (|marking(Ext_Mem_Acc_14_10)|=0) & (|marking(Ext_Mem_Acc_20_17)|=0) & (|marking(Ext_Mem_Acc_17_4)|=0) & (|marking(Ext_Mem_Acc_9_13)|=0) & (|marking(Ext_Mem_Acc_18_4)|=0) & (|marking(Ext_Mem_Acc_8_2)|=0) & (|marking(Ext_Mem_Acc_10_13)|=0) & (|marking(Ext_Mem_Acc_19_17)|=0) & (|marking(Ext_Mem_Acc_2_7)|=0) & (|marking(Ext_Mem_Acc_14_1)|=0) & (|marking(Ext_Mem_Acc_7_12)|=0) & (|marking(Ext_Mem_Acc_1_17)|=0) & (|marking(Ext_Mem_Acc_10_11)|=0) & (|marking(Ext_Mem_Acc_10_2)|=0) & (|marking(Ext_Mem_Acc_14_2)|=0) & (|marking(Ext_Mem_Acc_8_17)|=0) & (|marking(Ext_Mem_Acc_13_3)|=0) & (|marking(Ext_Mem_Acc_8_5)|=0) & (|marking(Ext_Mem_Acc_19_3)|=0) & (|marking(Ext_Mem_Acc_18_7)|=0) & (|marking(Ext_Mem_Acc_4_10)|=0) & (|marking(Ext_Mem_Acc_11_18)|=0) & (|marking(Ext_Mem_Acc_15_7)|=0) & (|marking(Ext_Mem_Acc_16_4)|=0) & (|marking(Ext_Mem_Acc_2_6)|=0) & (|marking(Ext_Mem_Acc_15_13)|=0) & (|marking(Ext_Mem_Acc_3_2)|=0) & (|marking(Ext_Mem_Acc_8_20)|=0) & (|marking(Ext_Mem_Acc_17_18)|=0) & (|marking(Ext_Mem_Acc_19_11)|=0) & (|marking(Ext_Mem_Acc_6_3)|=0) & (|marking(Ext_Mem_Acc_20_8)|=0) & (|marking(Ext_Mem_Acc_8_13)|=0) & (|marking(Ext_Mem_Acc_6_1)|=0) & (|marking(Ext_Mem_Acc_10_15)|=0) & (|marking(Ext_Mem_Acc_4_9)|=0) & (|marking(Ext_Mem_Acc_3_11)|=0) & (|marking(Ext_Mem_Acc_15_16)|=0) & (|marking(Ext_Mem_Acc_1_20)|=0) & (|marking(Ext_Mem_Acc_20_15)|=0) & (|marking(Ext_Mem_Acc_13_19)|=0) & (|marking(Ext_Mem_Acc_13_6)|=0) & (|marking(Ext_Mem_Acc_5_4)|=0) & (|marking(Ext_Mem_Acc_1_5)|=0) & (|marking(Ext_Mem_Acc_6_18)|=0) & (|marking(Ext_Mem_Acc_6_9)|=0) & (|marking(Ext_Mem_Acc_9_11)|=0) & (|marking(Ext_Mem_Acc_16_10)|=0) & (|marking(Ext_Mem_Acc_7_14)|=0) & (|marking(Ext_Mem_Acc_14_4)|=0) & (|marking(Ext_Mem_Acc_3_1)|=0) & (|marking(Ext_Mem_Acc_18_11)|=0) & (|marking(Ext_Mem_Acc_3_14)|=0) & (|marking(Ext_Mem_Acc_15_14)|=0) & (|marking(Ext_Mem_Acc_1_6)|=0) & (|marking(Ext_Mem_Acc_2_4)|=0) & (|marking(Ext_Mem_Acc_20_9)|=0) & (|marking(Ext_Mem_Acc_9_20)|=0) & (|marking(Ext_Mem_Acc_18_19)|=0) & (|marking(Ext_Mem_Acc_11_2)|=0) & (|marking(Ext_Mem_Acc_2_5)|=0) & (|marking(Ext_Mem_Acc_1_3)|=0) & (|marking(Ext_Mem_Acc_9_14)|=0) & (|marking(Ext_Mem_Acc_7_15)|=0) & (|marking(Ext_Mem_Acc_5_11)|=0) & (|marking(Ext_Mem_Acc_7_5)|=0) & (|marking(Ext_Mem_Acc_6_8)|=0) & (|marking(Ext_Mem_Acc_12_14)|=0) & (|marking(Ext_Mem_Acc_12_18)|=0) & (|marking(Ext_Mem_Acc_6_7)|=0) & (|marking(Ext_Mem_Acc_17_1)|=0) & (|marking(Ext_Mem_Acc_4_1)|=0) & (|marking(Ext_Mem_Acc_11_8)|=0) & (|marking(Ext_Mem_Acc_6_4)|=0) & (|marking(Ext_Mem_Acc_10_12)|=0) & (|marking(Ext_Mem_Acc_5_20)|=0) & (|marking(Ext_Mem_Acc_4_15)|=0) & (|marking(Ext_Mem_Acc_12_13)|=0) & (|marking(Ext_Mem_Acc_19_10)|=0) & (|marking(Ext_Mem_Acc_19_15)|=0) & (|marking(Ext_Mem_Acc_16_5)|=0) & (|marking(Ext_Mem_Acc_14_18)|=0) & (|marking(Ext_Mem_Acc_6_12)|=0) & (|marking(Ext_Mem_Acc_20_18)|=0) & (|marking(Ext_Mem_Acc_14_11)|=0) & (|marking(Ext_Mem_Acc_19_4)|=0) & (|marking(Ext_Mem_Acc_2_12)|=0) & (|marking(Ext_Mem_Acc_11_14)|=0) & (|marking(Ext_Mem_Acc_3_6)|=0) & (|marking(Ext_Mem_Acc_7_13)|=0) & (|marking(Ext_Mem_Acc_5_8)|=0) & (|marking(Ext_Mem_Acc_13_20)|=0) & (|marking(Ext_Mem_Acc_5_18)|=0) & (|marking(Ext_Mem_Acc_10_20)|=0) & (|marking(Ext_Mem_Acc_12_10)|=0) & (|marking(Ext_Mem_Acc_5_16)|=0) & (|marking(Ext_Mem_Acc_14_3)|=0) & (|marking(Ext_Mem_Acc_7_3)|=0) & (|marking(Ext_Mem_Acc_7_18)|=0) & (|marking(Ext_Mem_Acc_8_12)|=0) & (|marking(Ext_Mem_Acc_2_8)|=0) & (|marking(Ext_Mem_Acc_14_15)|=0) & (|marking(Ext_Mem_Acc_14_6)|=0) & (|marking(Ext_Mem_Acc_20_5)|=0) & (|marking(Ext_Mem_Acc_5_14)|=0) & (|marking(Ext_Mem_Acc_14_7)|=0) & (|marking(Ext_Mem_Acc_11_10)|=0) & (|marking(Ext_Mem_Acc_9_18)|=0) & (|marking(Ext_Mem_Acc_13_11)|=0) & (|marking(Ext_Mem_Acc_13_4)|=0) & (|marking(Ext_Mem_Acc_17_14)|=0) & (|marking(Ext_Mem_Acc_18_14)|=0) & (|marking(Ext_Mem_Acc_3_17)|=0) & (|marking(Ext_Mem_Acc_17_19)|=0) & (|marking(Ext_Mem_Acc_20_6)|=0) & (|marking(Ext_Mem_Acc_19_12)|=0) & (|marking(Ext_Mem_Acc_19_7)|=0) & (|marking(Ext_Mem_Acc_18_12)|=0) & (|marking(Ext_Mem_Acc_1_15)|=0) & (|marking(Ext_Mem_Acc_10_8)|=0) & (|marking(Ext_Mem_Acc_5_2)|=0) & (|marking(Ext_Mem_Acc_14_9)|=0) & (|marking(Ext_Mem_Acc_3_9)|=0) & (|marking(Ext_Mem_Acc_7_8)|=0) & (|marking(Ext_Mem_Acc_17_9)|=0) & (|marking(Ext_Mem_Acc_16_7)|=0) & (|marking(Ext_Mem_Acc_20_3)|=0) & (|marking(Ext_Mem_Acc_12_15)|=0) & (|marking(Ext_Mem_Acc_8_19)|=0) & (|marking(Ext_Mem_Acc_13_1)|=0) & (|marking(Ext_Mem_Acc_15_20)|=0) & (|marking(Ext_Mem_Acc_15_3)|=0) & (|marking(Ext_Mem_Acc_18_20)|=0) & (|marking(Ext_Mem_Acc_17_6)|=0) & (|marking(Ext_Mem_Acc_4_7)|=0) & (|marking(Ext_Mem_Acc_16_1)|=0) & (|marking(Ext_Mem_Acc_16_15)|=0) & (|marking(Ext_Mem_Acc_14_19)|=0) & (|marking(Ext_Mem_Acc_7_4)|=0) & (|marking(Ext_Mem_Acc_14_20)|=0) & (|marking(Ext_Mem_Acc_13_14)|=0)) & (true & (1>|marking(Ext_Mem_Acc_2_16)|))) & ((false | (1>|marking(Ext_Mem_Acc_2_16)|)) | (false))) & (true & (1=|marking(Ext_Bus)|)))


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