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

Execution Outputs of marcie for PhilosophersDyn/20 (P/T)

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

execution on node 27: cluster1u29.lip6.fr (runId=136972135800904_n_27)
=====================================================================
runnning marcie on PhilosophersDyn-PT-20 (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 PhilosophersDyn-PT-20, examination is CTLMarkingComparison
=====================================================================

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

START 1369743220

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: 540 NrTr: 17220)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369743225

--------------------
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(Neighbourhood_8_11)|) & (|marking(Neighbourhood_17_5)|=0) & (|marking(Neighbourhood_11_1)|=0) & (|marking(Neighbourhood_16_16)|=0) & (|marking(Neighbourhood_4_14)|=0) & (|marking(Neighbourhood_6_16)|=0) & (|marking(Neighbourhood_8_17)|=0) & (|marking(Neighbourhood_20_2)|=0) & (|marking(Neighbourhood_17_13)|=0) & (|marking(Neighbourhood_18_16)|=0) & (|marking(Neighbourhood_12_8)|=0) & (|marking(Neighbourhood_18_11)|=0) & (|marking(Neighbourhood_5_9)|=0) & (|marking(Neighbourhood_17_7)|=0) & (|marking(Neighbourhood_11_16)|=0) & (|marking(Neighbourhood_14_6)|=0) & (|marking(Neighbourhood_15_20)|=0) & (|marking(Neighbourhood_17_19)|=0) & (|marking(Neighbourhood_16_9)|=0) & (|marking(Neighbourhood_8_18)|=0) & (|marking(Neighbourhood_14_9)|=0) & (|marking(Neighbourhood_18_15)|=0) & (|marking(Neighbourhood_2_12)|=0) & (|marking(Neighbourhood_6_12)|=0) & (|marking(Neighbourhood_18_10)|=0) & (|marking(Neighbourhood_12_14)|=0) & (|marking(Neighbourhood_20_4)|=0) & (|marking(Neighbourhood_1_11)|=0) & (|marking(Neighbourhood_16_1)|=0) & (|marking(Neighbourhood_16_14)|=0) & (|marking(Neighbourhood_5_12)|=0) & (|marking(Neighbourhood_16_6)|=0) & (|marking(Neighbourhood_15_3)|=0) & (|marking(Neighbourhood_10_5)|=0) & (|marking(Neighbourhood_1_4)|=0) & (|marking(Neighbourhood_2_9)|=0) & (|marking(Neighbourhood_2_2)|=0) & (|marking(Neighbourhood_20_16)|=0) & (|marking(Neighbourhood_15_19)|=0) & (|marking(Neighbourhood_20_13)|=0) & (|marking(Neighbourhood_10_10)|=0) & (|marking(Neighbourhood_6_20)|=0) & (|marking(Neighbourhood_6_5)|=0) & (|marking(Neighbourhood_5_14)|=0) & (|marking(Neighbourhood_1_2)|=0) & (|marking(Neighbourhood_7_14)|=0) & (|marking(Neighbourhood_7_12)|=0) & (|marking(Neighbourhood_7_20)|=0) & (|marking(Neighbourhood_19_11)|=0) & (|marking(Neighbourhood_18_18)|=0) & (|marking(Neighbourhood_1_16)|=0) & (|marking(Neighbourhood_19_9)|=0) & (|marking(Neighbourhood_12_12)|=0) & (|marking(Neighbourhood_2_7)|=0) & (|marking(Neighbourhood_11_18)|=0) & (|marking(Neighbourhood_9_14)|=0) & (|marking(Neighbourhood_17_17)|=0) & (|marking(Neighbourhood_11_9)|=0) & (|marking(Neighbourhood_16_20)|=0) & (|marking(Neighbourhood_18_19)|=0) & (|marking(Neighbourhood_2_15)|=0) & (|marking(Neighbourhood_12_9)|=0) & (|marking(Neighbourhood_8_13)|=0) & (|marking(Neighbourhood_16_19)|=0) & (|marking(Neighbourhood_4_11)|=0) & (|marking(Neighbourhood_11_14)|=0) & (|marking(Neighbourhood_3_15)|=0) & (|marking(Neighbourhood_3_5)|=0) & (|marking(Neighbourhood_2_20)|=0) & (|marking(Neighbourhood_1_12)|=0) & (|marking(Neighbourhood_2_17)|=0) & (|marking(Neighbourhood_11_8)|=0) & (|marking(Neighbourhood_19_7)|=0) & (|marking(Neighbourhood_3_1)|=0) & (|marking(Neighbourhood_14_16)|=0) & (|marking(Neighbourhood_4_9)|=0) & (|marking(Neighbourhood_13_11)|=0) & (|marking(Neighbourhood_7_11)|=0) & (|marking(Neighbourhood_15_8)|=0) & (|marking(Neighbourhood_1_10)|=0) & (|marking(Neighbourhood_11_12)|=0) & (|marking(Neighbourhood_11_11)|=0) & (|marking(Neighbourhood_5_4)|=0) & (|marking(Neighbourhood_4_3)|=0) & (|marking(Neighbourhood_4_20)|=0) & (|marking(Neighbourhood_19_19)|=0) & (|marking(Neighbourhood_13_19)|=0) & (|marking(Neighbourhood_4_15)|=0) & (|marking(Neighbourhood_8_2)|=0) & (|marking(Neighbourhood_9_3)|=0) & (|marking(Neighbourhood_4_7)|=0) & (|marking(Neighbourhood_17_18)|=0) & (|marking(Neighbourhood_14_12)|=0) & (|marking(Neighbourhood_16_17)|=0) & (|marking(Neighbourhood_13_5)|=0) & (|marking(Neighbourhood_17_11)|=0) & (|marking(Neighbourhood_12_15)|=0) & (|marking(Neighbourhood_5_20)|=0) & (|marking(Neighbourhood_14_11)|=0) & (|marking(Neighbourhood_9_18)|=0) & (|marking(Neighbourhood_19_18)|=0) & (|marking(Neighbourhood_10_6)|=0) & (|marking(Neighbourhood_2_16)|=0) & (|marking(Neighbourhood_18_8)|=0) & (|marking(Neighbourhood_18_7)|=0) & (|marking(Neighbourhood_15_13)|=0) & (|marking(Neighbourhood_17_1)|=0) & (|marking(Neighbourhood_17_15)|=0) & (|marking(Neighbourhood_6_10)|=0) & (|marking(Neighbourhood_12_18)|=0) & (|marking(Neighbourhood_16_4)|=0) & (|marking(Neighbourhood_14_20)|=0) & (|marking(Neighbourhood_12_13)|=0) & (|marking(Neighbourhood_1_5)|=0) & (|marking(Neighbourhood_13_12)|=0) & (|marking(Neighbourhood_20_20)|=0) & (|marking(Neighbourhood_6_2)|=0) & (|marking(Neighbourhood_20_11)|=0) & (|marking(Neighbourhood_16_12)|=0) & (|marking(Neighbourhood_1_1)|=0) & (|marking(Neighbourhood_11_6)|=0) & (|marking(Neighbourhood_2_13)|=0) & (|marking(Neighbourhood_6_8)|=0) & (|marking(Neighbourhood_10_17)|=0) & (|marking(Neighbourhood_7_6)|=0) & (|marking(Neighbourhood_19_12)|=0) & (|marking(Neighbourhood_8_1)|=0) & (|marking(Neighbourhood_5_1)|=0) & (|marking(Neighbourhood_19_8)|=0) & (|marking(Neighbourhood_14_10)|=0) & (|marking(Neighbourhood_9_13)|=0) & (|marking(Neighbourhood_5_6)|=0) & (|marking(Neighbourhood_17_12)|=0) & (|marking(Neighbourhood_17_10)|=0) & (|marking(Neighbourhood_7_10)|=0) & (|marking(Neighbourhood_14_8)|=0) & (|marking(Neighbourhood_10_1)|=0) & (|marking(Neighbourhood_1_14)|=0) & (|marking(Neighbourhood_13_17)|=0) & (|marking(Neighbourhood_18_2)|=0) & (|marking(Neighbourhood_9_9)|=0) & (|marking(Neighbourhood_6_6)|=0) & (|marking(Neighbourhood_8_12)|=0) & (|marking(Neighbourhood_5_10)|=0) & (|marking(Neighbourhood_6_17)|=0) & (|marking(Neighbourhood_3_20)|=0) & (|marking(Neighbourhood_13_8)|=0) & (|marking(Neighbourhood_6_13)|=0) & (|marking(Neighbourhood_16_15)|=0) & (|marking(Neighbourhood_10_20)|=0) & (|marking(Neighbourhood_19_6)|=0) & (|marking(Neighbourhood_8_10)|=0) & (|marking(Neighbourhood_11_10)|=0) & (|marking(Neighbourhood_17_2)|=0) & (|marking(Neighbourhood_14_15)|=0) & (|marking(Neighbourhood_4_6)|=0) & (|marking(Neighbourhood_9_1)|=0) & (|marking(Neighbourhood_5_18)|=0) & (|marking(Neighbourhood_5_19)|=0) & (|marking(Neighbourhood_18_12)|=0) & (|marking(Neighbourhood_2_1)|=0) & (|marking(Neighbourhood_9_4)|=0) & (|marking(Neighbourhood_3_10)|=0) & (|marking(Neighbourhood_11_20)|=0) & (|marking(Neighbourhood_15_7)|=0) & (|marking(Neighbourhood_5_8)|=0) & (|marking(Neighbourhood_14_14)|=0) & (|marking(Neighbourhood_5_7)|=0) & (|marking(Neighbourhood_1_19)|=0) & (|marking(Neighbourhood_19_14)|=0) & (|marking(Neighbourhood_18_17)|=0) & (|marking(Neighbourhood_4_13)|=0) & (|marking(Neighbourhood_13_10)|=0) & (|marking(Neighbourhood_20_17)|=0) & (|marking(Neighbourhood_7_4)|=0) & (|marking(Neighbourhood_6_11)|=0) & (|marking(Neighbourhood_5_2)|=0) & (|marking(Neighbourhood_10_18)|=0) & (|marking(Neighbourhood_7_16)|=0) & (|marking(Neighbourhood_13_9)|=0) & (|marking(Neighbourhood_19_10)|=0) & (|marking(Neighbourhood_13_14)|=0) & (|marking(Neighbourhood_11_4)|=0) & (|marking(Neighbourhood_5_15)|=0) & (|marking(Neighbourhood_8_15)|=0) & (|marking(Neighbourhood_9_17)|=0) & (|marking(Neighbourhood_13_6)|=0) & (|marking(Neighbourhood_15_15)|=0) & (|marking(Neighbourhood_9_2)|=0) & (|marking(Neighbourhood_12_3)|=0) & (|marking(Neighbourhood_8_3)|=0) & (|marking(Neighbourhood_2_6)|=0) & (|marking(Neighbourhood_2_18)|=0) & (|marking(Neighbourhood_9_19)|=0) & (|marking(Neighbourhood_10_7)|=0) & (|marking(Neighbourhood_4_5)|=0) & (|marking(Neighbourhood_5_13)|=0) & (|marking(Neighbourhood_13_7)|=0) & (|marking(Neighbourhood_3_19)|=0) & (|marking(Neighbourhood_1_8)|=0) & (|marking(Neighbourhood_1_20)|=0) & (|marking(Neighbourhood_8_9)|=0) & (|marking(Neighbourhood_20_8)|=0) & (|marking(Neighbourhood_15_16)|=0) & (|marking(Neighbourhood_4_18)|=0) & (|marking(Neighbourhood_12_5)|=0) & (|marking(Neighbourhood_15_11)|=0) & (|marking(Neighbourhood_11_19)|=0) & (|marking(Neighbourhood_20_10)|=0) & (|marking(Neighbourhood_15_9)|=0) & (|marking(Neighbourhood_19_5)|=0) & (|marking(Neighbourhood_8_7)|=0) & (|marking(Neighbourhood_15_18)|=0) & (|marking(Neighbourhood_6_4)|=0) & (|marking(Neighbourhood_1_17)|=0) & (|marking(Neighbourhood_7_13)|=0) & (|marking(Neighbourhood_15_14)|=0) & (|marking(Neighbourhood_14_3)|=0) & (|marking(Neighbourhood_16_7)|=0) & (|marking(Neighbourhood_5_17)|=0) & (|marking(Neighbourhood_12_19)|=0) & (|marking(Neighbourhood_14_19)|=0) & (|marking(Neighbourhood_20_6)|=0) & (|marking(Neighbourhood_8_4)|=0) & (|marking(Neighbourhood_17_14)|=0) & (|marking(Neighbourhood_20_7)|=0) & (|marking(Neighbourhood_5_5)|=0) & (|marking(Neighbourhood_5_11)|=0) & (|marking(Neighbourhood_9_5)|=0) & (|marking(Neighbourhood_10_15)|=0) & (|marking(Neighbourhood_7_19)|=0) & (|marking(Neighbourhood_20_5)|=0) & (|marking(Neighbourhood_7_3)|=0) & (|marking(Neighbourhood_20_15)|=0) & (|marking(Neighbourhood_12_6)|=0) & (|marking(Neighbourhood_9_7)|=0) & (|marking(Neighbourhood_11_2)|=0) & (|marking(Neighbourhood_4_19)|=0) & (|marking(Neighbourhood_10_2)|=0) & (|marking(Neighbourhood_3_7)|=0) & (|marking(Neighbourhood_12_10)|=0) & (|marking(Neighbourhood_7_18)|=0) & (|marking(Neighbourhood_3_17)|=0) & (|marking(Neighbourhood_4_2)|=0) & (|marking(Neighbourhood_7_9)|=0) & (|marking(Neighbourhood_12_4)|=0) & (|marking(Neighbourhood_19_13)|=0) & (|marking(Neighbourhood_6_19)|=0) & (|marking(Neighbourhood_1_18)|=0) & (|marking(Neighbourhood_1_7)|=0) & (|marking(Neighbourhood_17_20)|=0) & (|marking(Neighbourhood_19_15)|=0) & (|marking(Neighbourhood_10_14)|=0) & (|marking(Neighbourhood_6_3)|=0) & (|marking(Neighbourhood_12_7)|=0) & (|marking(Neighbourhood_2_14)|=0) & (|marking(Neighbourhood_2_10)|=0) & (|marking(Neighbourhood_14_5)|=0) & (|marking(Neighbourhood_3_8)|=0) & (|marking(Neighbourhood_1_15)|=0) & (|marking(Neighbourhood_19_4)|=0) & (|marking(Neighbourhood_11_3)|=0) & (|marking(Neighbourhood_20_18)|=0) & (|marking(Neighbourhood_13_15)|=0) & (|marking(Neighbourhood_14_17)|=0) & (|marking(Neighbourhood_6_9)|=0) & (|marking(Neighbourhood_18_5)|=0) & (|marking(Neighbourhood_8_19)|=0) & (|marking(Neighbourhood_10_9)|=0) & (|marking(Neighbourhood_3_16)|=0) & (|marking(Neighbourhood_15_2)|=0) & (|marking(Neighbourhood_17_16)|=0) & (|marking(Neighbourhood_17_8)|=0) & (|marking(Neighbourhood_7_17)|=0) & (|marking(Neighbourhood_15_10)|=0) & (|marking(Neighbourhood_10_19)|=0) & (|marking(Neighbourhood_10_16)|=0) & (|marking(Neighbourhood_20_1)|=0) & (|marking(Neighbourhood_10_4)|=0) & (|marking(Neighbourhood_19_17)|=0) & (|marking(Neighbourhood_15_4)|=0) & (|marking(Neighbourhood_8_5)|=0) & (|marking(Neighbourhood_5_16)|=0) & (|marking(Neighbourhood_18_6)|=0) & (|marking(Neighbourhood_18_3)|=0) & (|marking(Neighbourhood_20_3)|=0) & (|marking(Neighbourhood_1_6)|=0) & (|marking(Neighbourhood_6_15)|=0) & (|marking(Neighbourhood_18_20)|=0) & (|marking(Neighbourhood_16_18)|=0) & (|marking(Neighbourhood_13_20)|=0) & (|marking(Neighbourhood_14_1)|=0) & (|marking(Neighbourhood_6_14)|=0) & (|marking(Neighbourhood_12_11)|=0) & (|marking(Neighbourhood_14_13)|=0) & (|marking(Neighbourhood_13_4)|=0) & (|marking(Neighbourhood_2_5)|=0) & (|marking(Neighbourhood_7_8)|=0) & (|marking(Neighbourhood_8_8)|=0) & (|marking(Neighbourhood_3_14)|=0) & (|marking(Neighbourhood_10_3)|=0) & (|marking(Neighbourhood_18_1)|=0) & (|marking(Neighbourhood_8_20)|=0) & (|marking(Neighbourhood_4_12)|=0) & (|marking(Neighbourhood_3_2)|=0) & (|marking(Neighbourhood_3_18)|=0) & (|marking(Neighbourhood_12_2)|=0) & (|marking(Neighbourhood_9_16)|=0) & (|marking(Neighbourhood_4_8)|=0) & (|marking(Neighbourhood_9_15)|=0) & (|marking(Neighbourhood_3_9)|=0) & (|marking(Neighbourhood_17_3)|=0) & (|marking(Neighbourhood_9_11)|=0) & (|marking(Neighbourhood_9_10)|=0) & (|marking(Neighbourhood_2_11)|=0) & (|marking(Neighbourhood_4_17)|=0) & (|marking(Neighbourhood_8_14)|=0) & (|marking(Neighbourhood_20_9)|=0) & (|marking(Neighbourhood_10_13)|=0) & (|marking(Neighbourhood_2_19)|=0) & (|marking(Neighbourhood_2_4)|=0) & (|marking(Neighbourhood_7_7)|=0) & (|marking(Neighbourhood_15_17)|=0) & (|marking(Neighbourhood_9_12)|=0) & (|marking(Neighbourhood_3_3)|=0) & (|marking(Neighbourhood_8_16)|=0) & (|marking(Neighbourhood_13_3)|=0) & (|marking(Neighbourhood_4_1)|=0) & (|marking(Neighbourhood_13_2)|=0) & (|marking(Neighbourhood_2_3)|=0) & (|marking(Neighbourhood_12_17)|=0) & (|marking(Neighbourhood_6_18)|=0) & (|marking(Neighbourhood_15_12)|=0) & (|marking(Neighbourhood_9_8)|=0) & (|marking(Neighbourhood_18_9)|=0) & (|marking(Neighbourhood_19_1)|=0) & (|marking(Neighbourhood_17_6)|=0) & (|marking(Neighbourhood_13_1)|=0) & (|marking(Neighbourhood_16_8)|=0) & (|marking(Neighbourhood_20_12)|=0) & (|marking(Neighbourhood_16_2)|=0) & (|marking(Neighbourhood_18_4)|=0) & (|marking(Neighbourhood_19_16)|=0) & (|marking(Neighbourhood_6_1)|=0) & (|marking(Neighbourhood_4_16)|=0) & (|marking(Neighbourhood_18_13)|=0) & (|marking(Neighbourhood_10_8)|=0) & (|marking(Neighbourhood_3_6)|=0) & (|marking(Neighbourhood_15_1)|=0) & (|marking(Neighbourhood_3_4)|=0) & (|marking(Neighbourhood_7_15)|=0) & (|marking(Neighbourhood_12_20)|=0) & (|marking(Neighbourhood_14_4)|=0) & (|marking(Neighbourhood_17_4)|=0) & (|marking(Neighbourhood_16_13)|=0) & (|marking(Neighbourhood_1_13)|=0) & (|marking(Neighbourhood_9_6)|=0) & (|marking(Neighbourhood_2_8)|=0) & (|marking(Neighbourhood_7_1)|=0) & (|marking(Neighbourhood_19_20)|=0) & (|marking(Neighbourhood_11_5)|=0) & (|marking(Neighbourhood_16_10)|=0) & (|marking(Neighbourhood_19_3)|=0) & (|marking(Neighbourhood_5_3)|=0) & (|marking(Neighbourhood_12_1)|=0) & (|marking(Neighbourhood_11_17)|=0) & (|marking(Neighbourhood_19_2)|=0) & (|marking(Neighbourhood_16_11)|=0) & (|marking(Neighbourhood_1_3)|=0) & (|marking(Neighbourhood_20_14)|=0) & (|marking(Neighbourhood_14_7)|=0) & (|marking(Neighbourhood_7_5)|=0) & (|marking(Neighbourhood_16_5)|=0) & (|marking(Neighbourhood_18_14)|=0) & (|marking(Neighbourhood_9_20)|=0) & (|marking(Neighbourhood_14_2)|=0) & (|marking(Neighbourhood_1_9)|=0) & (|marking(Neighbourhood_7_2)|=0) & (|marking(Neighbourhood_4_4)|=0) & (|marking(Neighbourhood_6_7)|=0) & (|marking(Neighbourhood_3_12)|=0) & (|marking(Neighbourhood_11_15)|=0) & (|marking(Neighbourhood_4_10)|=0) & (|marking(Neighbourhood_13_13)|=0) & (|marking(Neighbourhood_11_7)|=0) & (|marking(Neighbourhood_15_6)|=0) & (|marking(Neighbourhood_10_12)|=0) & (|marking(Neighbourhood_20_19)|=0) & (|marking(Neighbourhood_17_9)|=0) & (|marking(Neighbourhood_16_3)|=0) & (|marking(Neighbourhood_10_11)|=0) & (|marking(Neighbourhood_12_16)|=0) & (|marking(Neighbourhood_11_13)|=0) & (|marking(Neighbourhood_13_18)|=0) & (|marking(Neighbourhood_15_5)|=0) & (|marking(Neighbourhood_3_11)|=0) & (|marking(Neighbourhood_13_16)|=0) & (|marking(Neighbourhood_14_18)|=0) & (|marking(Neighbourhood_3_13)|=0) & (|marking(Neighbourhood_8_6)|=0)) => X (true & (1=|marking(HasRight_14)|) & (|marking(HasRight_20)|=0) & (|marking(HasRight_13)|=0) & (|marking(HasRight_12)|=0) & (|marking(HasRight_11)|=0) & (|marking(HasRight_17)|=0) & (|marking(HasRight_15)|=0) & (|marking(HasRight_8)|=0) & (|marking(HasRight_7)|=0) & (|marking(HasRight_2)|=0) & (|marking(HasRight_18)|=0) & (|marking(HasRight_1)|=0) & (|marking(HasRight_3)|=0) & (|marking(HasRight_9)|=0) & (|marking(HasRight_10)|=0) & (|marking(HasRight_6)|=0) & (|marking(HasRight_19)|=0) & (|marking(HasRight_5)|=0) & (|marking(HasRight_4)|=0) & (|marking(HasRight_16)|=0)))
ctl p_1871_markingcomparison_full_and: E G ((true & (1=|marking(WaitRight_1)|) & (|marking(WaitRight_2)|=0) & (|marking(WaitRight_6)|=0) & (|marking(WaitRight_13)|=0) & (|marking(WaitRight_10)|=0) & (|marking(WaitRight_8)|=0) & (|marking(WaitRight_4)|=0) & (|marking(WaitRight_16)|=0) & (|marking(WaitRight_9)|=0) & (|marking(WaitRight_17)|=0) & (|marking(WaitRight_18)|=0) & (|marking(WaitRight_20)|=0) & (|marking(WaitRight_14)|=0) & (|marking(WaitRight_7)|=0) & (|marking(WaitRight_5)|=0) & (|marking(WaitRight_11)|=0) & (|marking(WaitRight_12)|=0) & (|marking(WaitRight_19)|=0) & (|marking(WaitRight_15)|=0) & (|marking(WaitRight_3)|=0)) & (true & (1=|marking(Neighbourhood_3_14)|) & (|marking(Neighbourhood_17_5)|=0) & (|marking(Neighbourhood_11_1)|=0) & (|marking(Neighbourhood_16_16)|=0) & (|marking(Neighbourhood_4_14)|=0) & (|marking(Neighbourhood_6_16)|=0) & (|marking(Neighbourhood_8_17)|=0) & (|marking(Neighbourhood_20_2)|=0) & (|marking(Neighbourhood_17_13)|=0) & (|marking(Neighbourhood_18_16)|=0) & (|marking(Neighbourhood_12_8)|=0) & (|marking(Neighbourhood_18_11)|=0) & (|marking(Neighbourhood_5_9)|=0) & (|marking(Neighbourhood_17_7)|=0) & (|marking(Neighbourhood_11_16)|=0) & (|marking(Neighbourhood_14_6)|=0) & (|marking(Neighbourhood_15_20)|=0) & (|marking(Neighbourhood_17_19)|=0) & (|marking(Neighbourhood_16_9)|=0) & (|marking(Neighbourhood_8_18)|=0) & (|marking(Neighbourhood_14_9)|=0) & (|marking(Neighbourhood_18_15)|=0) & (|marking(Neighbourhood_2_12)|=0) & (|marking(Neighbourhood_6_12)|=0) & (|marking(Neighbourhood_18_10)|=0) & (|marking(Neighbourhood_12_14)|=0) & (|marking(Neighbourhood_20_4)|=0) & (|marking(Neighbourhood_1_11)|=0) & (|marking(Neighbourhood_16_1)|=0) & (|marking(Neighbourhood_16_14)|=0) & (|marking(Neighbourhood_5_12)|=0) & (|marking(Neighbourhood_16_6)|=0) & (|marking(Neighbourhood_15_3)|=0) & (|marking(Neighbourhood_10_5)|=0) & (|marking(Neighbourhood_1_4)|=0) & (|marking(Neighbourhood_2_9)|=0) & (|marking(Neighbourhood_2_2)|=0) & (|marking(Neighbourhood_20_16)|=0) & (|marking(Neighbourhood_15_19)|=0) & (|marking(Neighbourhood_20_13)|=0) & (|marking(Neighbourhood_10_10)|=0) & (|marking(Neighbourhood_6_20)|=0) & (|marking(Neighbourhood_6_5)|=0) & (|marking(Neighbourhood_5_14)|=0) & (|marking(Neighbourhood_1_2)|=0) & (|marking(Neighbourhood_7_14)|=0) & (|marking(Neighbourhood_7_12)|=0) & (|marking(Neighbourhood_7_20)|=0) & (|marking(Neighbourhood_19_11)|=0) & (|marking(Neighbourhood_18_18)|=0) & (|marking(Neighbourhood_1_16)|=0) & (|marking(Neighbourhood_19_9)|=0) & (|marking(Neighbourhood_12_12)|=0) & (|marking(Neighbourhood_2_7)|=0) & (|marking(Neighbourhood_11_18)|=0) & (|marking(Neighbourhood_9_14)|=0) & (|marking(Neighbourhood_17_17)|=0) & (|marking(Neighbourhood_11_9)|=0) & (|marking(Neighbourhood_16_20)|=0) & (|marking(Neighbourhood_18_19)|=0) & (|marking(Neighbourhood_2_15)|=0) & (|marking(Neighbourhood_12_9)|=0) & (|marking(Neighbourhood_8_13)|=0) & (|marking(Neighbourhood_16_19)|=0) & (|marking(Neighbourhood_4_11)|=0) & (|marking(Neighbourhood_11_14)|=0) & (|marking(Neighbourhood_3_15)|=0) & (|marking(Neighbourhood_3_5)|=0) & (|marking(Neighbourhood_2_20)|=0) & (|marking(Neighbourhood_1_12)|=0) & (|marking(Neighbourhood_2_17)|=0) & (|marking(Neighbourhood_11_8)|=0) & (|marking(Neighbourhood_19_7)|=0) & (|marking(Neighbourhood_3_1)|=0) & (|marking(Neighbourhood_14_16)|=0) & (|marking(Neighbourhood_4_9)|=0) & (|marking(Neighbourhood_13_11)|=0) & (|marking(Neighbourhood_7_11)|=0) & (|marking(Neighbourhood_15_8)|=0) & (|marking(Neighbourhood_1_10)|=0) & (|marking(Neighbourhood_11_12)|=0) & (|marking(Neighbourhood_11_11)|=0) & (|marking(Neighbourhood_5_4)|=0) & (|marking(Neighbourhood_4_3)|=0) & (|marking(Neighbourhood_4_20)|=0) & (|marking(Neighbourhood_19_19)|=0) & (|marking(Neighbourhood_13_19)|=0) & (|marking(Neighbourhood_4_15)|=0) & (|marking(Neighbourhood_8_2)|=0) & (|marking(Neighbourhood_9_3)|=0) & (|marking(Neighbourhood_4_7)|=0) & (|marking(Neighbourhood_17_18)|=0) & (|marking(Neighbourhood_14_12)|=0) & (|marking(Neighbourhood_16_17)|=0) & (|marking(Neighbourhood_13_5)|=0) & (|marking(Neighbourhood_17_11)|=0) & (|marking(Neighbourhood_12_15)|=0) & (|marking(Neighbourhood_5_20)|=0) & (|marking(Neighbourhood_14_11)|=0) & (|marking(Neighbourhood_9_18)|=0) & (|marking(Neighbourhood_19_18)|=0) & (|marking(Neighbourhood_10_6)|=0) & (|marking(Neighbourhood_2_16)|=0) & (|marking(Neighbourhood_18_8)|=0) & (|marking(Neighbourhood_18_7)|=0) & (|marking(Neighbourhood_15_13)|=0) & (|marking(Neighbourhood_17_1)|=0) & (|marking(Neighbourhood_17_15)|=0) & (|marking(Neighbourhood_6_10)|=0) & (|marking(Neighbourhood_12_18)|=0) & (|marking(Neighbourhood_16_4)|=0) & (|marking(Neighbourhood_14_20)|=0) & (|marking(Neighbourhood_12_13)|=0) & (|marking(Neighbourhood_1_5)|=0) & (|marking(Neighbourhood_13_12)|=0) & (|marking(Neighbourhood_20_20)|=0) & (|marking(Neighbourhood_6_2)|=0) & (|marking(Neighbourhood_20_11)|=0) & (|marking(Neighbourhood_16_12)|=0) & (|marking(Neighbourhood_1_1)|=0) & (|marking(Neighbourhood_11_6)|=0) & (|marking(Neighbourhood_2_13)|=0) & (|marking(Neighbourhood_6_8)|=0) & (|marking(Neighbourhood_10_17)|=0) & (|marking(Neighbourhood_7_6)|=0) & (|marking(Neighbourhood_19_12)|=0) & (|marking(Neighbourhood_8_1)|=0) & (|marking(Neighbourhood_5_1)|=0) & (|marking(Neighbourhood_19_8)|=0) & (|marking(Neighbourhood_14_10)|=0) & (|marking(Neighbourhood_9_13)|=0) & (|marking(Neighbourhood_5_6)|=0) & (|marking(Neighbourhood_17_12)|=0) & (|marking(Neighbourhood_17_10)|=0) & (|marking(Neighbourhood_7_10)|=0) & (|marking(Neighbourhood_14_8)|=0) & (|marking(Neighbourhood_10_1)|=0) & (|marking(Neighbourhood_1_14)|=0) & (|marking(Neighbourhood_13_17)|=0) & (|marking(Neighbourhood_18_2)|=0) & (|marking(Neighbourhood_9_9)|=0) & (|marking(Neighbourhood_6_6)|=0) & (|marking(Neighbourhood_8_12)|=0) & (|marking(Neighbourhood_5_10)|=0) & (|marking(Neighbourhood_6_17)|=0) & (|marking(Neighbourhood_3_20)|=0) & (|marking(Neighbourhood_13_8)|=0) & (|marking(Neighbourhood_6_13)|=0) & (|marking(Neighbourhood_16_15)|=0) & (|marking(Neighbourhood_10_20)|=0) & (|marking(Neighbourhood_19_6)|=0) & (|marking(Neighbourhood_8_10)|=0) & (|marking(Neighbourhood_11_10)|=0) & (|marking(Neighbourhood_17_2)|=0) & (|marking(Neighbourhood_14_15)|=0) & (|marking(Neighbourhood_4_6)|=0) & (|marking(Neighbourhood_9_1)|=0) & (|marking(Neighbourhood_5_18)|=0) & (|marking(Neighbourhood_5_19)|=0) & (|marking(Neighbourhood_18_12)|=0) & (|marking(Neighbourhood_2_1)|=0) & (|marking(Neighbourhood_9_4)|=0) & (|marking(Neighbourhood_3_10)|=0) & (|marking(Neighbourhood_11_20)|=0) & (|marking(Neighbourhood_15_7)|=0) & (|marking(Neighbourhood_5_8)|=0) & (|marking(Neighbourhood_14_14)|=0) & (|marking(Neighbourhood_5_7)|=0) & (|marking(Neighbourhood_1_19)|=0) & (|marking(Neighbourhood_19_14)|=0) & (|marking(Neighbourhood_18_17)|=0) & (|marking(Neighbourhood_4_13)|=0) & (|marking(Neighbourhood_13_10)|=0) & (|marking(Neighbourhood_20_17)|=0) & (|marking(Neighbourhood_7_4)|=0) & (|marking(Neighbourhood_6_11)|=0) & (|marking(Neighbourhood_5_2)|=0) & (|marking(Neighbourhood_10_18)|=0) & (|marking(Neighbourhood_7_16)|=0) & (|marking(Neighbourhood_13_9)|=0) & (|marking(Neighbourhood_19_10)|=0) & (|marking(Neighbourhood_13_14)|=0) & (|marking(Neighbourhood_11_4)|=0) & (|marking(Neighbourhood_5_15)|=0) & (|marking(Neighbourhood_8_15)|=0) & (|marking(Neighbourhood_9_17)|=0) & (|marking(Neighbourhood_13_6)|=0) & (|marking(Neighbourhood_15_15)|=0) & (|marking(Neighbourhood_9_2)|=0) & (|marking(Neighbourhood_12_3)|=0) & (|marking(Neighbourhood_8_3)|=0) & (|marking(Neighbourhood_2_6)|=0) & (|marking(Neighbourhood_2_18)|=0) & (|marking(Neighbourhood_9_19)|=0) & (|marking(Neighbourhood_10_7)|=0) & (|marking(Neighbourhood_4_5)|=0) & (|marking(Neighbourhood_5_13)|=0) & (|marking(Neighbourhood_13_7)|=0) & (|marking(Neighbourhood_3_19)|=0) & (|marking(Neighbourhood_1_8)|=0) & (|marking(Neighbourhood_1_20)|=0) & (|marking(Neighbourhood_8_9)|=0) & (|marking(Neighbourhood_20_8)|=0) & (|marking(Neighbourhood_15_16)|=0) & (|marking(Neighbourhood_4_18)|=0) & (|marking(Neighbourhood_12_5)|=0) & (|marking(Neighbourhood_15_11)|=0) & (|marking(Neighbourhood_11_19)|=0) & (|marking(Neighbourhood_20_10)|=0) & (|marking(Neighbourhood_15_9)|=0) & (|marking(Neighbourhood_19_5)|=0) & (|marking(Neighbourhood_8_7)|=0) & (|marking(Neighbourhood_15_18)|=0) & (|marking(Neighbourhood_6_4)|=0) & (|marking(Neighbourhood_1_17)|=0) & (|marking(Neighbourhood_7_13)|=0) & (|marking(Neighbourhood_15_14)|=0) & (|marking(Neighbourhood_14_3)|=0) & (|marking(Neighbourhood_16_7)|=0) & (|marking(Neighbourhood_5_17)|=0) & (|marking(Neighbourhood_12_19)|=0) & (|marking(Neighbourhood_14_19)|=0) & (|marking(Neighbourhood_20_6)|=0) & (|marking(Neighbourhood_8_4)|=0) & (|marking(Neighbourhood_17_14)|=0) & (|marking(Neighbourhood_20_7)|=0) & (|marking(Neighbourhood_5_5)|=0) & (|marking(Neighbourhood_5_11)|=0) & (|marking(Neighbourhood_9_5)|=0) & (|marking(Neighbourhood_10_15)|=0) & (|marking(Neighbourhood_7_19)|=0) & (|marking(Neighbourhood_20_5)|=0) & (|marking(Neighbourhood_7_3)|=0) & (|marking(Neighbourhood_20_15)|=0) & (|marking(Neighbourhood_12_6)|=0) & (|marking(Neighbourhood_9_7)|=0) & (|marking(Neighbourhood_11_2)|=0) & (|marking(Neighbourhood_4_19)|=0) & (|marking(Neighbourhood_10_2)|=0) & (|marking(Neighbourhood_3_7)|=0) & (|marking(Neighbourhood_12_10)|=0) & (|marking(Neighbourhood_7_18)|=0) & (|marking(Neighbourhood_3_17)|=0) & (|marking(Neighbourhood_4_2)|=0) & (|marking(Neighbourhood_7_9)|=0) & (|marking(Neighbourhood_12_4)|=0) & (|marking(Neighbourhood_19_13)|=0) & (|marking(Neighbourhood_6_19)|=0) & (|marking(Neighbourhood_1_18)|=0) & (|marking(Neighbourhood_1_7)|=0) & (|marking(Neighbourhood_17_20)|=0) & (|marking(Neighbourhood_19_15)|=0) & (|marking(Neighbourhood_10_14)|=0) & (|marking(Neighbourhood_6_3)|=0) & (|marking(Neighbourhood_12_7)|=0) & (|marking(Neighbourhood_2_14)|=0) & (|marking(Neighbourhood_2_10)|=0) & (|marking(Neighbourhood_14_5)|=0) & (|marking(Neighbourhood_3_8)|=0) & (|marking(Neighbourhood_1_15)|=0) & (|marking(Neighbourhood_19_4)|=0) & (|marking(Neighbourhood_11_3)|=0) & (|marking(Neighbourhood_20_18)|=0) & (|marking(Neighbourhood_13_15)|=0) & (|marking(Neighbourhood_14_17)|=0) & (|marking(Neighbourhood_6_9)|=0) & (|marking(Neighbourhood_18_5)|=0) & (|marking(Neighbourhood_8_19)|=0) & (|marking(Neighbourhood_10_9)|=0) & (|marking(Neighbourhood_3_16)|=0) & (|marking(Neighbourhood_15_2)|=0) & (|marking(Neighbourhood_17_16)|=0) & (|marking(Neighbourhood_17_8)|=0) & (|marking(Neighbourhood_7_17)|=0) & (|marking(Neighbourhood_15_10)|=0) & (|marking(Neighbourhood_10_19)|=0) & (|marking(Neighbourhood_10_16)|=0) & (|marking(Neighbourhood_20_1)|=0) & (|marking(Neighbourhood_10_4)|=0) & (|marking(Neighbourhood_19_17)|=0) & (|marking(Neighbourhood_15_4)|=0) & (|marking(Neighbourhood_8_5)|=0) & (|marking(Neighbourhood_5_16)|=0) & (|marking(Neighbourhood_18_6)|=0) & (|marking(Neighbourhood_18_3)|=0) & (|marking(Neighbourhood_20_3)|=0) & (|marking(Neighbourhood_1_6)|=0) & (|marking(Neighbourhood_6_15)|=0) & (|marking(Neighbourhood_18_20)|=0) & (|marking(Neighbourhood_16_18)|=0) & (|marking(Neighbourhood_13_20)|=0) & (|marking(Neighbourhood_14_1)|=0) & (|marking(Neighbourhood_6_14)|=0) & (|marking(Neighbourhood_12_11)|=0) & (|marking(Neighbourhood_14_13)|=0) & (|marking(Neighbourhood_13_4)|=0) & (|marking(Neighbourhood_2_5)|=0) & (|marking(Neighbourhood_7_8)|=0) & (|marking(Neighbourhood_8_8)|=0) & (|marking(Neighbourhood_10_3)|=0) & (|marking(Neighbourhood_18_1)|=0) & (|marking(Neighbourhood_8_20)|=0) & (|marking(Neighbourhood_4_12)|=0) & (|marking(Neighbourhood_3_2)|=0) & (|marking(Neighbourhood_3_18)|=0) & (|marking(Neighbourhood_12_2)|=0) & (|marking(Neighbourhood_9_16)|=0) & (|marking(Neighbourhood_4_8)|=0) & (|marking(Neighbourhood_9_15)|=0) & (|marking(Neighbourhood_3_9)|=0) & (|marking(Neighbourhood_17_3)|=0) & (|marking(Neighbourhood_9_11)|=0) & (|marking(Neighbourhood_9_10)|=0) & (|marking(Neighbourhood_2_11)|=0) & (|marking(Neighbourhood_4_17)|=0) & (|marking(Neighbourhood_8_14)|=0) & (|marking(Neighbourhood_20_9)|=0) & (|marking(Neighbourhood_10_13)|=0) & (|marking(Neighbourhood_2_19)|=0) & (|marking(Neighbourhood_2_4)|=0) & (|marking(Neighbourhood_7_7)|=0) & (|marking(Neighbourhood_15_17)|=0) & (|marking(Neighbourhood_9_12)|=0) & (|marking(Neighbourhood_3_3)|=0) & (|marking(Neighbourhood_8_16)|=0) & (|marking(Neighbourhood_13_3)|=0) & (|marking(Neighbourhood_4_1)|=0) & (|marking(Neighbourhood_13_2)|=0) & (|marking(Neighbourhood_2_3)|=0) & (|marking(Neighbourhood_12_17)|=0) & (|marking(Neighbourhood_6_18)|=0) & (|marking(Neighbourhood_15_12)|=0) & (|marking(Neighbourhood_9_8)|=0) & (|marking(Neighbourhood_18_9)|=0) & (|marking(Neighbourhood_19_1)|=0) & (|marking(Neighbourhood_17_6)|=0) & (|marking(Neighbourhood_13_1)|=0) & (|marking(Neighbourhood_16_8)|=0) & (|marking(Neighbourhood_20_12)|=0) & (|marking(Neighbourhood_16_2)|=0) & (|marking(Neighbourhood_18_4)|=0) & (|marking(Neighbourhood_19_16)|=0) & (|marking(Neighbourhood_6_1)|=0) & (|marking(Neighbourhood_4_16)|=0) & (|marking(Neighbourhood_18_13)|=0) & (|marking(Neighbourhood_10_8)|=0) & (|marking(Neighbourhood_3_6)|=0) & (|marking(Neighbourhood_15_1)|=0) & (|marking(Neighbourhood_3_4)|=0) & (|marking(Neighbourhood_7_15)|=0) & (|marking(Neighbourhood_12_20)|=0) & (|marking(Neighbourhood_14_4)|=0) & (|marking(Neighbourhood_17_4)|=0) & (|marking(Neighbourhood_16_13)|=0) & (|marking(Neighbourhood_1_13)|=0) & (|marking(Neighbourhood_9_6)|=0) & (|marking(Neighbourhood_2_8)|=0) & (|marking(Neighbourhood_7_1)|=0) & (|marking(Neighbourhood_19_20)|=0) & (|marking(Neighbourhood_11_5)|=0) & (|marking(Neighbourhood_16_10)|=0) & (|marking(Neighbourhood_19_3)|=0) & (|marking(Neighbourhood_5_3)|=0) & (|marking(Neighbourhood_12_1)|=0) & (|marking(Neighbourhood_11_17)|=0) & (|marking(Neighbourhood_19_2)|=0) & (|marking(Neighbourhood_16_11)|=0) & (|marking(Neighbourhood_1_3)|=0) & (|marking(Neighbourhood_20_14)|=0) & (|marking(Neighbourhood_14_7)|=0) & (|marking(Neighbourhood_7_5)|=0) & (|marking(Neighbourhood_16_5)|=0) & (|marking(Neighbourhood_18_14)|=0) & (|marking(Neighbourhood_9_20)|=0) & (|marking(Neighbourhood_14_2)|=0) & (|marking(Neighbourhood_1_9)|=0) & (|marking(Neighbourhood_7_2)|=0) & (|marking(Neighbourhood_4_4)|=0) & (|marking(Neighbourhood_6_7)|=0) & (|marking(Neighbourhood_3_12)|=0) & (|marking(Neighbourhood_11_15)|=0) & (|marking(Neighbourhood_4_10)|=0) & (|marking(Neighbourhood_13_13)|=0) & (|marking(Neighbourhood_11_7)|=0) & (|marking(Neighbourhood_15_6)|=0) & (|marking(Neighbourhood_10_12)|=0) & (|marking(Neighbourhood_20_19)|=0) & (|marking(Neighbourhood_17_9)|=0) & (|marking(Neighbourhood_16_3)|=0) & (|marking(Neighbourhood_10_11)|=0) & (|marking(Neighbourhood_12_16)|=0) & (|marking(Neighbourhood_11_13)|=0) & (|marking(Neighbourhood_13_18)|=0) & (|marking(Neighbourhood_15_5)|=0) & (|marking(Neighbourhood_3_11)|=0) & (|marking(Neighbourhood_13_16)|=0) & (|marking(Neighbourhood_14_18)|=0) & (|marking(Neighbourhood_3_13)|=0) & (|marking(Neighbourhood_8_11)|=0) & (|marking(Neighbourhood_8_6)|=0)))
ctl p_1872_markingcomparison_full_or: A G ((true & (1=|marking(WaitRight_1)|) & (|marking(WaitRight_2)|=0) & (|marking(WaitRight_6)|=0) & (|marking(WaitRight_13)|=0) & (|marking(WaitRight_10)|=0) & (|marking(WaitRight_8)|=0) & (|marking(WaitRight_4)|=0) & (|marking(WaitRight_16)|=0) & (|marking(WaitRight_9)|=0) & (|marking(WaitRight_17)|=0) & (|marking(WaitRight_18)|=0) & (|marking(WaitRight_20)|=0) & (|marking(WaitRight_14)|=0) & (|marking(WaitRight_7)|=0) & (|marking(WaitRight_5)|=0) & (|marking(WaitRight_11)|=0) & (|marking(WaitRight_12)|=0) & (|marking(WaitRight_19)|=0) & (|marking(WaitRight_15)|=0) & (|marking(WaitRight_3)|=0)) | (true & (1=|marking(Neighbourhood_3_14)|) & (|marking(Neighbourhood_17_5)|=0) & (|marking(Neighbourhood_11_1)|=0) & (|marking(Neighbourhood_16_16)|=0) & (|marking(Neighbourhood_4_14)|=0) & (|marking(Neighbourhood_6_16)|=0) & (|marking(Neighbourhood_8_17)|=0) & (|marking(Neighbourhood_20_2)|=0) & (|marking(Neighbourhood_17_13)|=0) & (|marking(Neighbourhood_18_16)|=0) & (|marking(Neighbourhood_12_8)|=0) & (|marking(Neighbourhood_18_11)|=0) & (|marking(Neighbourhood_5_9)|=0) & (|marking(Neighbourhood_17_7)|=0) & (|marking(Neighbourhood_11_16)|=0) & (|marking(Neighbourhood_14_6)|=0) & (|marking(Neighbourhood_15_20)|=0) & (|marking(Neighbourhood_17_19)|=0) & (|marking(Neighbourhood_16_9)|=0) & (|marking(Neighbourhood_8_18)|=0) & (|marking(Neighbourhood_14_9)|=0) & (|marking(Neighbourhood_18_15)|=0) & (|marking(Neighbourhood_2_12)|=0) & (|marking(Neighbourhood_6_12)|=0) & (|marking(Neighbourhood_18_10)|=0) & (|marking(Neighbourhood_12_14)|=0) & (|marking(Neighbourhood_20_4)|=0) & (|marking(Neighbourhood_1_11)|=0) & (|marking(Neighbourhood_16_1)|=0) & (|marking(Neighbourhood_16_14)|=0) & (|marking(Neighbourhood_5_12)|=0) & (|marking(Neighbourhood_16_6)|=0) & (|marking(Neighbourhood_15_3)|=0) & (|marking(Neighbourhood_10_5)|=0) & (|marking(Neighbourhood_1_4)|=0) & (|marking(Neighbourhood_2_9)|=0) & (|marking(Neighbourhood_2_2)|=0) & (|marking(Neighbourhood_20_16)|=0) & (|marking(Neighbourhood_15_19)|=0) & (|marking(Neighbourhood_20_13)|=0) & (|marking(Neighbourhood_10_10)|=0) & (|marking(Neighbourhood_6_20)|=0) & (|marking(Neighbourhood_6_5)|=0) & (|marking(Neighbourhood_5_14)|=0) & (|marking(Neighbourhood_1_2)|=0) & (|marking(Neighbourhood_7_14)|=0) & (|marking(Neighbourhood_7_12)|=0) & (|marking(Neighbourhood_7_20)|=0) & (|marking(Neighbourhood_19_11)|=0) & (|marking(Neighbourhood_18_18)|=0) & (|marking(Neighbourhood_1_16)|=0) & (|marking(Neighbourhood_19_9)|=0) & (|marking(Neighbourhood_12_12)|=0) & (|marking(Neighbourhood_2_7)|=0) & (|marking(Neighbourhood_11_18)|=0) & (|marking(Neighbourhood_9_14)|=0) & (|marking(Neighbourhood_17_17)|=0) & (|marking(Neighbourhood_11_9)|=0) & (|marking(Neighbourhood_16_20)|=0) & (|marking(Neighbourhood_18_19)|=0) & (|marking(Neighbourhood_2_15)|=0) & (|marking(Neighbourhood_12_9)|=0) & (|marking(Neighbourhood_8_13)|=0) & (|marking(Neighbourhood_16_19)|=0) & (|marking(Neighbourhood_4_11)|=0) & (|marking(Neighbourhood_11_14)|=0) & (|marking(Neighbourhood_3_15)|=0) & (|marking(Neighbourhood_3_5)|=0) & (|marking(Neighbourhood_2_20)|=0) & (|marking(Neighbourhood_1_12)|=0) & (|marking(Neighbourhood_2_17)|=0) & (|marking(Neighbourhood_11_8)|=0) & (|marking(Neighbourhood_19_7)|=0) & (|marking(Neighbourhood_3_1)|=0) & (|marking(Neighbourhood_14_16)|=0) & (|marking(Neighbourhood_4_9)|=0) & (|marking(Neighbourhood_13_11)|=0) & (|marking(Neighbourhood_7_11)|=0) & (|marking(Neighbourhood_15_8)|=0) & (|marking(Neighbourhood_1_10)|=0) & (|marking(Neighbourhood_11_12)|=0) & (|marking(Neighbourhood_11_11)|=0) & (|marking(Neighbourhood_5_4)|=0) & (|marking(Neighbourhood_4_3)|=0) & (|marking(Neighbourhood_4_20)|=0) & (|marking(Neighbourhood_19_19)|=0) & (|marking(Neighbourhood_13_19)|=0) & (|marking(Neighbourhood_4_15)|=0) & (|marking(Neighbourhood_8_2)|=0) & (|marking(Neighbourhood_9_3)|=0) & (|marking(Neighbourhood_4_7)|=0) & (|marking(Neighbourhood_17_18)|=0) & (|marking(Neighbourhood_14_12)|=0) & (|marking(Neighbourhood_16_17)|=0) & (|marking(Neighbourhood_13_5)|=0) & (|marking(Neighbourhood_17_11)|=0) & (|marking(Neighbourhood_12_15)|=0) & (|marking(Neighbourhood_5_20)|=0) & (|marking(Neighbourhood_14_11)|=0) & (|marking(Neighbourhood_9_18)|=0) & (|marking(Neighbourhood_19_18)|=0) & (|marking(Neighbourhood_10_6)|=0) & (|marking(Neighbourhood_2_16)|=0) & (|marking(Neighbourhood_18_8)|=0) & (|marking(Neighbourhood_18_7)|=0) & (|marking(Neighbourhood_15_13)|=0) & (|marking(Neighbourhood_17_1)|=0) & (|marking(Neighbourhood_17_15)|=0) & (|marking(Neighbourhood_6_10)|=0) & (|marking(Neighbourhood_12_18)|=0) & (|marking(Neighbourhood_16_4)|=0) & (|marking(Neighbourhood_14_20)|=0) & (|marking(Neighbourhood_12_13)|=0) & (|marking(Neighbourhood_1_5)|=0) & (|marking(Neighbourhood_13_12)|=0) & (|marking(Neighbourhood_20_20)|=0) & (|marking(Neighbourhood_6_2)|=0) & (|marking(Neighbourhood_20_11)|=0) & (|marking(Neighbourhood_16_12)|=0) & (|marking(Neighbourhood_1_1)|=0) & (|marking(Neighbourhood_11_6)|=0) & (|marking(Neighbourhood_2_13)|=0) & (|marking(Neighbourhood_6_8)|=0) & (|marking(Neighbourhood_10_17)|=0) & (|marking(Neighbourhood_7_6)|=0) & (|marking(Neighbourhood_19_12)|=0) & (|marking(Neighbourhood_8_1)|=0) & (|marking(Neighbourhood_5_1)|=0) & (|marking(Neighbourhood_19_8)|=0) & (|marking(Neighbourhood_14_10)|=0) & (|marking(Neighbourhood_9_13)|=0) & (|marking(Neighbourhood_5_6)|=0) & (|marking(Neighbourhood_17_12)|=0) & (|marking(Neighbourhood_17_10)|=0) & (|marking(Neighbourhood_7_10)|=0) & (|marking(Neighbourhood_14_8)|=0) & (|marking(Neighbourhood_10_1)|=0) & (|marking(Neighbourhood_1_14)|=0) & (|marking(Neighbourhood_13_17)|=0) & (|marking(Neighbourhood_18_2)|=0) & (|marking(Neighbourhood_9_9)|=0) & (|marking(Neighbourhood_6_6)|=0) & (|marking(Neighbourhood_8_12)|=0) & (|marking(Neighbourhood_5_10)|=0) & (|marking(Neighbourhood_6_17)|=0) & (|marking(Neighbourhood_3_20)|=0) & (|marking(Neighbourhood_13_8)|=0) & (|marking(Neighbourhood_6_13)|=0) & (|marking(Neighbourhood_16_15)|=0) & (|marking(Neighbourhood_10_20)|=0) & (|marking(Neighbourhood_19_6)|=0) & (|marking(Neighbourhood_8_10)|=0) & (|marking(Neighbourhood_11_10)|=0) & (|marking(Neighbourhood_17_2)|=0) & (|marking(Neighbourhood_14_15)|=0) & (|marking(Neighbourhood_4_6)|=0) & (|marking(Neighbourhood_9_1)|=0) & (|marking(Neighbourhood_5_18)|=0) & (|marking(Neighbourhood_5_19)|=0) & (|marking(Neighbourhood_18_12)|=0) & (|marking(Neighbourhood_2_1)|=0) & (|marking(Neighbourhood_9_4)|=0) & (|marking(Neighbourhood_3_10)|=0) & (|marking(Neighbourhood_11_20)|=0) & (|marking(Neighbourhood_15_7)|=0) & (|marking(Neighbourhood_5_8)|=0) & (|marking(Neighbourhood_14_14)|=0) & (|marking(Neighbourhood_5_7)|=0) & (|marking(Neighbourhood_1_19)|=0) & (|marking(Neighbourhood_19_14)|=0) & (|marking(Neighbourhood_18_17)|=0) & (|marking(Neighbourhood_4_13)|=0) & (|marking(Neighbourhood_13_10)|=0) & (|marking(Neighbourhood_20_17)|=0) & (|marking(Neighbourhood_7_4)|=0) & (|marking(Neighbourhood_6_11)|=0) & (|marking(Neighbourhood_5_2)|=0) & (|marking(Neighbourhood_10_18)|=0) & (|marking(Neighbourhood_7_16)|=0) & (|marking(Neighbourhood_13_9)|=0) & (|marking(Neighbourhood_19_10)|=0) & (|marking(Neighbourhood_13_14)|=0) & (|marking(Neighbourhood_11_4)|=0) & (|marking(Neighbourhood_5_15)|=0) & (|marking(Neighbourhood_8_15)|=0) & (|marking(Neighbourhood_9_17)|=0) & (|marking(Neighbourhood_13_6)|=0) & (|marking(Neighbourhood_15_15)|=0) & (|marking(Neighbourhood_9_2)|=0) & (|marking(Neighbourhood_12_3)|=0) & (|marking(Neighbourhood_8_3)|=0) & (|marking(Neighbourhood_2_6)|=0) & (|marking(Neighbourhood_2_18)|=0) & (|marking(Neighbourhood_9_19)|=0) & (|marking(Neighbourhood_10_7)|=0) & (|marking(Neighbourhood_4_5)|=0) & (|marking(Neighbourhood_5_13)|=0) & (|marking(Neighbourhood_13_7)|=0) & (|marking(Neighbourhood_3_19)|=0) & (|marking(Neighbourhood_1_8)|=0) & (|marking(Neighbourhood_1_20)|=0) & (|marking(Neighbourhood_8_9)|=0) & (|marking(Neighbourhood_20_8)|=0) & (|marking(Neighbourhood_15_16)|=0) & (|marking(Neighbourhood_4_18)|=0) & (|marking(Neighbourhood_12_5)|=0) & (|marking(Neighbourhood_15_11)|=0) & (|marking(Neighbourhood_11_19)|=0) & (|marking(Neighbourhood_20_10)|=0) & (|marking(Neighbourhood_15_9)|=0) & (|marking(Neighbourhood_19_5)|=0) & (|marking(Neighbourhood_8_7)|=0) & (|marking(Neighbourhood_15_18)|=0) & (|marking(Neighbourhood_6_4)|=0) & (|marking(Neighbourhood_1_17)|=0) & (|marking(Neighbourhood_7_13)|=0) & (|marking(Neighbourhood_15_14)|=0) & (|marking(Neighbourhood_14_3)|=0) & (|marking(Neighbourhood_16_7)|=0) & (|marking(Neighbourhood_5_17)|=0) & (|marking(Neighbourhood_12_19)|=0) & (|marking(Neighbourhood_14_19)|=0) & (|marking(Neighbourhood_20_6)|=0) & (|marking(Neighbourhood_8_4)|=0) & (|marking(Neighbourhood_17_14)|=0) & (|marking(Neighbourhood_20_7)|=0) & (|marking(Neighbourhood_5_5)|=0) & (|marking(Neighbourhood_5_11)|=0) & (|marking(Neighbourhood_9_5)|=0) & (|marking(Neighbourhood_10_15)|=0) & (|marking(Neighbourhood_7_19)|=0) & (|marking(Neighbourhood_20_5)|=0) & (|marking(Neighbourhood_7_3)|=0) & (|marking(Neighbourhood_20_15)|=0) & (|marking(Neighbourhood_12_6)|=0) & (|marking(Neighbourhood_9_7)|=0) & (|marking(Neighbourhood_11_2)|=0) & (|marking(Neighbourhood_4_19)|=0) & (|marking(Neighbourhood_10_2)|=0) & (|marking(Neighbourhood_3_7)|=0) & (|marking(Neighbourhood_12_10)|=0) & (|marking(Neighbourhood_7_18)|=0) & (|marking(Neighbourhood_3_17)|=0) & (|marking(Neighbourhood_4_2)|=0) & (|marking(Neighbourhood_7_9)|=0) & (|marking(Neighbourhood_12_4)|=0) & (|marking(Neighbourhood_19_13)|=0) & (|marking(Neighbourhood_6_19)|=0) & (|marking(Neighbourhood_1_18)|=0) & (|marking(Neighbourhood_1_7)|=0) & (|marking(Neighbourhood_17_20)|=0) & (|marking(Neighbourhood_19_15)|=0) & (|marking(Neighbourhood_10_14)|=0) & (|marking(Neighbourhood_6_3)|=0) & (|marking(Neighbourhood_12_7)|=0) & (|marking(Neighbourhood_2_14)|=0) & (|marking(Neighbourhood_2_10)|=0) & (|marking(Neighbourhood_14_5)|=0) & (|marking(Neighbourhood_3_8)|=0) & (|marking(Neighbourhood_1_15)|=0) & (|marking(Neighbourhood_19_4)|=0) & (|marking(Neighbourhood_11_3)|=0) & (|marking(Neighbourhood_20_18)|=0) & (|marking(Neighbourhood_13_15)|=0) & (|marking(Neighbourhood_14_17)|=0) & (|marking(Neighbourhood_6_9)|=0) & (|marking(Neighbourhood_18_5)|=0) & (|marking(Neighbourhood_8_19)|=0) & (|marking(Neighbourhood_10_9)|=0) & (|marking(Neighbourhood_3_16)|=0) & (|marking(Neighbourhood_15_2)|=0) & (|marking(Neighbourhood_17_16)|=0) & (|marking(Neighbourhood_17_8)|=0) & (|marking(Neighbourhood_7_17)|=0) & (|marking(Neighbourhood_15_10)|=0) & (|marking(Neighbourhood_10_19)|=0) & (|marking(Neighbourhood_10_16)|=0) & (|marking(Neighbourhood_20_1)|=0) & (|marking(Neighbourhood_10_4)|=0) & (|marking(Neighbourhood_19_17)|=0) & (|marking(Neighbourhood_15_4)|=0) & (|marking(Neighbourhood_8_5)|=0) & (|marking(Neighbourhood_5_16)|=0) & (|marking(Neighbourhood_18_6)|=0) & (|marking(Neighbourhood_18_3)|=0) & (|marking(Neighbourhood_20_3)|=0) & (|marking(Neighbourhood_1_6)|=0) & (|marking(Neighbourhood_6_15)|=0) & (|marking(Neighbourhood_18_20)|=0) & (|marking(Neighbourhood_16_18)|=0) & (|marking(Neighbourhood_13_20)|=0) & (|marking(Neighbourhood_14_1)|=0) & (|marking(Neighbourhood_6_14)|=0) & (|marking(Neighbourhood_12_11)|=0) & (|marking(Neighbourhood_14_13)|=0) & (|marking(Neighbourhood_13_4)|=0) & (|marking(Neighbourhood_2_5)|=0) & (|marking(Neighbourhood_7_8)|=0) & (|marking(Neighbourhood_8_8)|=0) & (|marking(Neighbourhood_10_3)|=0) & (|marking(Neighbourhood_18_1)|=0) & (|marking(Neighbourhood_8_20)|=0) & (|marking(Neighbourhood_4_12)|=0) & (|marking(Neighbourhood_3_2)|=0) & (|marking(Neighbourhood_3_18)|=0) & (|marking(Neighbourhood_12_2)|=0) & (|marking(Neighbourhood_9_16)|=0) & (|marking(Neighbourhood_4_8)|=0) & (|marking(Neighbourhood_9_15)|=0) & (|marking(Neighbourhood_3_9)|=0) & (|marking(Neighbourhood_17_3)|=0) & (|marking(Neighbourhood_9_11)|=0) & (|marking(Neighbourhood_9_10)|=0) & (|marking(Neighbourhood_2_11)|=0) & (|marking(Neighbourhood_4_17)|=0) & (|marking(Neighbourhood_8_14)|=0) & (|marking(Neighbourhood_20_9)|=0) & (|marking(Neighbourhood_10_13)|=0) & (|marking(Neighbourhood_2_19)|=0) & (|marking(Neighbourhood_2_4)|=0) & (|marking(Neighbourhood_7_7)|=0) & (|marking(Neighbourhood_15_17)|=0) & (|marking(Neighbourhood_9_12)|=0) & (|marking(Neighbourhood_3_3)|=0) & (|marking(Neighbourhood_8_16)|=0) & (|marking(Neighbourhood_13_3)|=0) & (|marking(Neighbourhood_4_1)|=0) & (|marking(Neighbourhood_13_2)|=0) & (|marking(Neighbourhood_2_3)|=0) & (|marking(Neighbourhood_12_17)|=0) & (|marking(Neighbourhood_6_18)|=0) & (|marking(Neighbourhood_15_12)|=0) & (|marking(Neighbourhood_9_8)|=0) & (|marking(Neighbourhood_18_9)|=0) & (|marking(Neighbourhood_19_1)|=0) & (|marking(Neighbourhood_17_6)|=0) & (|marking(Neighbourhood_13_1)|=0) & (|marking(Neighbourhood_16_8)|=0) & (|marking(Neighbourhood_20_12)|=0) & (|marking(Neighbourhood_16_2)|=0) & (|marking(Neighbourhood_18_4)|=0) & (|marking(Neighbourhood_19_16)|=0) & (|marking(Neighbourhood_6_1)|=0) & (|marking(Neighbourhood_4_16)|=0) & (|marking(Neighbourhood_18_13)|=0) & (|marking(Neighbourhood_10_8)|=0) & (|marking(Neighbourhood_3_6)|=0) & (|marking(Neighbourhood_15_1)|=0) & (|marking(Neighbourhood_3_4)|=0) & (|marking(Neighbourhood_7_15)|=0) & (|marking(Neighbourhood_12_20)|=0) & (|marking(Neighbourhood_14_4)|=0) & (|marking(Neighbourhood_17_4)|=0) & (|marking(Neighbourhood_16_13)|=0) & (|marking(Neighbourhood_1_13)|=0) & (|marking(Neighbourhood_9_6)|=0) & (|marking(Neighbourhood_2_8)|=0) & (|marking(Neighbourhood_7_1)|=0) & (|marking(Neighbourhood_19_20)|=0) & (|marking(Neighbourhood_11_5)|=0) & (|marking(Neighbourhood_16_10)|=0) & (|marking(Neighbourhood_19_3)|=0) & (|marking(Neighbourhood_5_3)|=0) & (|marking(Neighbourhood_12_1)|=0) & (|marking(Neighbourhood_11_17)|=0) & (|marking(Neighbourhood_19_2)|=0) & (|marking(Neighbourhood_16_11)|=0) & (|marking(Neighbourhood_1_3)|=0) & (|marking(Neighbourhood_20_14)|=0) & (|marking(Neighbourhood_14_7)|=0) & (|marking(Neighbourhood_7_5)|=0) & (|marking(Neighbourhood_16_5)|=0) & (|marking(Neighbourhood_18_14)|=0) & (|marking(Neighbourhood_9_20)|=0) & (|marking(Neighbourhood_14_2)|=0) & (|marking(Neighbourhood_1_9)|=0) & (|marking(Neighbourhood_7_2)|=0) & (|marking(Neighbourhood_4_4)|=0) & (|marking(Neighbourhood_6_7)|=0) & (|marking(Neighbourhood_3_12)|=0) & (|marking(Neighbourhood_11_15)|=0) & (|marking(Neighbourhood_4_10)|=0) & (|marking(Neighbourhood_13_13)|=0) & (|marking(Neighbourhood_11_7)|=0) & (|marking(Neighbourhood_15_6)|=0) & (|marking(Neighbourhood_10_12)|=0) & (|marking(Neighbourhood_20_19)|=0) & (|marking(Neighbourhood_17_9)|=0) & (|marking(Neighbourhood_16_3)|=0) & (|marking(Neighbourhood_10_11)|=0) & (|marking(Neighbourhood_12_16)|=0) & (|marking(Neighbourhood_11_13)|=0) & (|marking(Neighbourhood_13_18)|=0) & (|marking(Neighbourhood_15_5)|=0) & (|marking(Neighbourhood_3_11)|=0) & (|marking(Neighbourhood_13_16)|=0) & (|marking(Neighbourhood_14_18)|=0) & (|marking(Neighbourhood_3_13)|=0) & (|marking(Neighbourhood_8_11)|=0) & (|marking(Neighbourhood_8_6)|=0)))
ctl p_1873_markingcomparison_full_and_notx: A G ((true & (1=|marking(WaitRight_1)|) & (|marking(WaitRight_2)|=0) & (|marking(WaitRight_6)|=0) & (|marking(WaitRight_13)|=0) & (|marking(WaitRight_10)|=0) & (|marking(WaitRight_8)|=0) & (|marking(WaitRight_4)|=0) & (|marking(WaitRight_16)|=0) & (|marking(WaitRight_9)|=0) & (|marking(WaitRight_17)|=0) & (|marking(WaitRight_18)|=0) & (|marking(WaitRight_20)|=0) & (|marking(WaitRight_14)|=0) & (|marking(WaitRight_7)|=0) & (|marking(WaitRight_5)|=0) & (|marking(WaitRight_11)|=0) & (|marking(WaitRight_12)|=0) & (|marking(WaitRight_19)|=0) & (|marking(WaitRight_15)|=0) & (|marking(WaitRight_3)|=0)) & !(true & (1=|marking(Neighbourhood_3_14)|) & (|marking(Neighbourhood_17_5)|=0) & (|marking(Neighbourhood_11_1)|=0) & (|marking(Neighbourhood_16_16)|=0) & (|marking(Neighbourhood_4_14)|=0) & (|marking(Neighbourhood_6_16)|=0) & (|marking(Neighbourhood_8_17)|=0) & (|marking(Neighbourhood_20_2)|=0) & (|marking(Neighbourhood_17_13)|=0) & (|marking(Neighbourhood_18_16)|=0) & (|marking(Neighbourhood_12_8)|=0) & (|marking(Neighbourhood_18_11)|=0) & (|marking(Neighbourhood_5_9)|=0) & (|marking(Neighbourhood_17_7)|=0) & (|marking(Neighbourhood_11_16)|=0) & (|marking(Neighbourhood_14_6)|=0) & (|marking(Neighbourhood_15_20)|=0) & (|marking(Neighbourhood_17_19)|=0) & (|marking(Neighbourhood_16_9)|=0) & (|marking(Neighbourhood_8_18)|=0) & (|marking(Neighbourhood_14_9)|=0) & (|marking(Neighbourhood_18_15)|=0) & (|marking(Neighbourhood_2_12)|=0) & (|marking(Neighbourhood_6_12)|=0) & (|marking(Neighbourhood_18_10)|=0) & (|marking(Neighbourhood_12_14)|=0) & (|marking(Neighbourhood_20_4)|=0) & (|marking(Neighbourhood_1_11)|=0) & (|marking(Neighbourhood_16_1)|=0) & (|marking(Neighbourhood_16_14)|=0) & (|marking(Neighbourhood_5_12)|=0) & (|marking(Neighbourhood_16_6)|=0) & (|marking(Neighbourhood_15_3)|=0) & (|marking(Neighbourhood_10_5)|=0) & (|marking(Neighbourhood_1_4)|=0) & (|marking(Neighbourhood_2_9)|=0) & (|marking(Neighbourhood_2_2)|=0) & (|marking(Neighbourhood_20_16)|=0) & (|marking(Neighbourhood_15_19)|=0) & (|marking(Neighbourhood_20_13)|=0) & (|marking(Neighbourhood_10_10)|=0) & (|marking(Neighbourhood_6_20)|=0) & (|marking(Neighbourhood_6_5)|=0) & (|marking(Neighbourhood_5_14)|=0) & (|marking(Neighbourhood_1_2)|=0) & (|marking(Neighbourhood_7_14)|=0) & (|marking(Neighbourhood_7_12)|=0) & (|marking(Neighbourhood_7_20)|=0) & (|marking(Neighbourhood_19_11)|=0) & (|marking(Neighbourhood_18_18)|=0) & (|marking(Neighbourhood_1_16)|=0) & (|marking(Neighbourhood_19_9)|=0) & (|marking(Neighbourhood_12_12)|=0) & (|marking(Neighbourhood_2_7)|=0) & (|marking(Neighbourhood_11_18)|=0) & (|marking(Neighbourhood_9_14)|=0) & (|marking(Neighbourhood_17_17)|=0) & (|marking(Neighbourhood_11_9)|=0) & (|marking(Neighbourhood_16_20)|=0) & (|marking(Neighbourhood_18_19)|=0) & (|marking(Neighbourhood_2_15)|=0) & (|marking(Neighbourhood_12_9)|=0) & (|marking(Neighbourhood_8_13)|=0) & (|marking(Neighbourhood_16_19)|=0) & (|marking(Neighbourhood_4_11)|=0) & (|marking(Neighbourhood_11_14)|=0) & (|marking(Neighbourhood_3_15)|=0) & (|marking(Neighbourhood_3_5)|=0) & (|marking(Neighbourhood_2_20)|=0) & (|marking(Neighbourhood_1_12)|=0) & (|marking(Neighbourhood_2_17)|=0) & (|marking(Neighbourhood_11_8)|=0) & (|marking(Neighbourhood_19_7)|=0) & (|marking(Neighbourhood_3_1)|=0) & (|marking(Neighbourhood_14_16)|=0) & (|marking(Neighbourhood_4_9)|=0) & (|marking(Neighbourhood_13_11)|=0) & (|marking(Neighbourhood_7_11)|=0) & (|marking(Neighbourhood_15_8)|=0) & (|marking(Neighbourhood_1_10)|=0) & (|marking(Neighbourhood_11_12)|=0) & (|marking(Neighbourhood_11_11)|=0) & (|marking(Neighbourhood_5_4)|=0) & (|marking(Neighbourhood_4_3)|=0) & (|marking(Neighbourhood_4_20)|=0) & (|marking(Neighbourhood_19_19)|=0) & (|marking(Neighbourhood_13_19)|=0) & (|marking(Neighbourhood_4_15)|=0) & (|marking(Neighbourhood_8_2)|=0) & (|marking(Neighbourhood_9_3)|=0) & (|marking(Neighbourhood_4_7)|=0) & (|marking(Neighbourhood_17_18)|=0) & (|marking(Neighbourhood_14_12)|=0) & (|marking(Neighbourhood_16_17)|=0) & (|marking(Neighbourhood_13_5)|=0) & (|marking(Neighbourhood_17_11)|=0) & (|marking(Neighbourhood_12_15)|=0) & (|marking(Neighbourhood_5_20)|=0) & (|marking(Neighbourhood_14_11)|=0) & (|marking(Neighbourhood_9_18)|=0) & (|marking(Neighbourhood_19_18)|=0) & (|marking(Neighbourhood_10_6)|=0) & (|marking(Neighbourhood_2_16)|=0) & (|marking(Neighbourhood_18_8)|=0) & (|marking(Neighbourhood_18_7)|=0) & (|marking(Neighbourhood_15_13)|=0) & (|marking(Neighbourhood_17_1)|=0) & (|marking(Neighbourhood_17_15)|=0) & (|marking(Neighbourhood_6_10)|=0) & (|marking(Neighbourhood_12_18)|=0) & (|marking(Neighbourhood_16_4)|=0) & (|marking(Neighbourhood_14_20)|=0) & (|marking(Neighbourhood_12_13)|=0) & (|marking(Neighbourhood_1_5)|=0) & (|marking(Neighbourhood_13_12)|=0) & (|marking(Neighbourhood_20_20)|=0) & (|marking(Neighbourhood_6_2)|=0) & (|marking(Neighbourhood_20_11)|=0) & (|marking(Neighbourhood_16_12)|=0) & (|marking(Neighbourhood_1_1)|=0) & (|marking(Neighbourhood_11_6)|=0) & (|marking(Neighbourhood_2_13)|=0) & (|marking(Neighbourhood_6_8)|=0) & (|marking(Neighbourhood_10_17)|=0) & (|marking(Neighbourhood_7_6)|=0) & (|marking(Neighbourhood_19_12)|=0) & (|marking(Neighbourhood_8_1)|=0) & (|marking(Neighbourhood_5_1)|=0) & (|marking(Neighbourhood_19_8)|=0) & (|marking(Neighbourhood_14_10)|=0) & (|marking(Neighbourhood_9_13)|=0) & (|marking(Neighbourhood_5_6)|=0) & (|marking(Neighbourhood_17_12)|=0) & (|marking(Neighbourhood_17_10)|=0) & (|marking(Neighbourhood_7_10)|=0) & (|marking(Neighbourhood_14_8)|=0) & (|marking(Neighbourhood_10_1)|=0) & (|marking(Neighbourhood_1_14)|=0) & (|marking(Neighbourhood_13_17)|=0) & (|marking(Neighbourhood_18_2)|=0) & (|marking(Neighbourhood_9_9)|=0) & (|marking(Neighbourhood_6_6)|=0) & (|marking(Neighbourhood_8_12)|=0) & (|marking(Neighbourhood_5_10)|=0) & (|marking(Neighbourhood_6_17)|=0) & (|marking(Neighbourhood_3_20)|=0) & (|marking(Neighbourhood_13_8)|=0) & (|marking(Neighbourhood_6_13)|=0) & (|marking(Neighbourhood_16_15)|=0) & (|marking(Neighbourhood_10_20)|=0) & (|marking(Neighbourhood_19_6)|=0) & (|marking(Neighbourhood_8_10)|=0) & (|marking(Neighbourhood_11_10)|=0) & (|marking(Neighbourhood_17_2)|=0) & (|marking(Neighbourhood_14_15)|=0) & (|marking(Neighbourhood_4_6)|=0) & (|marking(Neighbourhood_9_1)|=0) & (|marking(Neighbourhood_5_18)|=0) & (|marking(Neighbourhood_5_19)|=0) & (|marking(Neighbourhood_18_12)|=0) & (|marking(Neighbourhood_2_1)|=0) & (|marking(Neighbourhood_9_4)|=0) & (|marking(Neighbourhood_3_10)|=0) & (|marking(Neighbourhood_11_20)|=0) & (|marking(Neighbourhood_15_7)|=0) & (|marking(Neighbourhood_5_8)|=0) & (|marking(Neighbourhood_14_14)|=0) & (|marking(Neighbourhood_5_7)|=0) & (|marking(Neighbourhood_1_19)|=0) & (|marking(Neighbourhood_19_14)|=0) & (|marking(Neighbourhood_18_17)|=0) & (|marking(Neighbourhood_4_13)|=0) & (|marking(Neighbourhood_13_10)|=0) & (|marking(Neighbourhood_20_17)|=0) & (|marking(Neighbourhood_7_4)|=0) & (|marking(Neighbourhood_6_11)|=0) & (|marking(Neighbourhood_5_2)|=0) & (|marking(Neighbourhood_10_18)|=0) & (|marking(Neighbourhood_7_16)|=0) & (|marking(Neighbourhood_13_9)|=0) & (|marking(Neighbourhood_19_10)|=0) & (|marking(Neighbourhood_13_14)|=0) & (|marking(Neighbourhood_11_4)|=0) & (|marking(Neighbourhood_5_15)|=0) & (|marking(Neighbourhood_8_15)|=0) & (|marking(Neighbourhood_9_17)|=0) & (|marking(Neighbourhood_13_6)|=0) & (|marking(Neighbourhood_15_15)|=0) & (|marking(Neighbourhood_9_2)|=0) & (|marking(Neighbourhood_12_3)|=0) & (|marking(Neighbourhood_8_3)|=0) & (|marking(Neighbourhood_2_6)|=0) & (|marking(Neighbourhood_2_18)|=0) & (|marking(Neighbourhood_9_19)|=0) & (|marking(Neighbourhood_10_7)|=0) & (|marking(Neighbourhood_4_5)|=0) & (|marking(Neighbourhood_5_13)|=0) & (|marking(Neighbourhood_13_7)|=0) & (|marking(Neighbourhood_3_19)|=0) & (|marking(Neighbourhood_1_8)|=0) & (|marking(Neighbourhood_1_20)|=0) & (|marking(Neighbourhood_8_9)|=0) & (|marking(Neighbourhood_20_8)|=0) & (|marking(Neighbourhood_15_16)|=0) & (|marking(Neighbourhood_4_18)|=0) & (|marking(Neighbourhood_12_5)|=0) & (|marking(Neighbourhood_15_11)|=0) & (|marking(Neighbourhood_11_19)|=0) & (|marking(Neighbourhood_20_10)|=0) & (|marking(Neighbourhood_15_9)|=0) & (|marking(Neighbourhood_19_5)|=0) & (|marking(Neighbourhood_8_7)|=0) & (|marking(Neighbourhood_15_18)|=0) & (|marking(Neighbourhood_6_4)|=0) & (|marking(Neighbourhood_1_17)|=0) & (|marking(Neighbourhood_7_13)|=0) & (|marking(Neighbourhood_15_14)|=0) & (|marking(Neighbourhood_14_3)|=0) & (|marking(Neighbourhood_16_7)|=0) & (|marking(Neighbourhood_5_17)|=0) & (|marking(Neighbourhood_12_19)|=0) & (|marking(Neighbourhood_14_19)|=0) & (|marking(Neighbourhood_20_6)|=0) & (|marking(Neighbourhood_8_4)|=0) & (|marking(Neighbourhood_17_14)|=0) & (|marking(Neighbourhood_20_7)|=0) & (|marking(Neighbourhood_5_5)|=0) & (|marking(Neighbourhood_5_11)|=0) & (|marking(Neighbourhood_9_5)|=0) & (|marking(Neighbourhood_10_15)|=0) & (|marking(Neighbourhood_7_19)|=0) & (|marking(Neighbourhood_20_5)|=0) & (|marking(Neighbourhood_7_3)|=0) & (|marking(Neighbourhood_20_15)|=0) & (|marking(Neighbourhood_12_6)|=0) & (|marking(Neighbourhood_9_7)|=0) & (|marking(Neighbourhood_11_2)|=0) & (|marking(Neighbourhood_4_19)|=0) & (|marking(Neighbourhood_10_2)|=0) & (|marking(Neighbourhood_3_7)|=0) & (|marking(Neighbourhood_12_10)|=0) & (|marking(Neighbourhood_7_18)|=0) & (|marking(Neighbourhood_3_17)|=0) & (|marking(Neighbourhood_4_2)|=0) & (|marking(Neighbourhood_7_9)|=0) & (|marking(Neighbourhood_12_4)|=0) & (|marking(Neighbourhood_19_13)|=0) & (|marking(Neighbourhood_6_19)|=0) & (|marking(Neighbourhood_1_18)|=0) & (|marking(Neighbourhood_1_7)|=0) & (|marking(Neighbourhood_17_20)|=0) & (|marking(Neighbourhood_19_15)|=0) & (|marking(Neighbourhood_10_14)|=0) & (|marking(Neighbourhood_6_3)|=0) & (|marking(Neighbourhood_12_7)|=0) & (|marking(Neighbourhood_2_14)|=0) & (|marking(Neighbourhood_2_10)|=0) & (|marking(Neighbourhood_14_5)|=0) & (|marking(Neighbourhood_3_8)|=0) & (|marking(Neighbourhood_1_15)|=0) & (|marking(Neighbourhood_19_4)|=0) & (|marking(Neighbourhood_11_3)|=0) & (|marking(Neighbourhood_20_18)|=0) & (|marking(Neighbourhood_13_15)|=0) & (|marking(Neighbourhood_14_17)|=0) & (|marking(Neighbourhood_6_9)|=0) & (|marking(Neighbourhood_18_5)|=0) & (|marking(Neighbourhood_8_19)|=0) & (|marking(Neighbourhood_10_9)|=0) & (|marking(Neighbourhood_3_16)|=0) & (|marking(Neighbourhood_15_2)|=0) & (|marking(Neighbourhood_17_16)|=0) & (|marking(Neighbourhood_17_8)|=0) & (|marking(Neighbourhood_7_17)|=0) & (|marking(Neighbourhood_15_10)|=0) & (|marking(Neighbourhood_10_19)|=0) & (|marking(Neighbourhood_10_16)|=0) & (|marking(Neighbourhood_20_1)|=0) & (|marking(Neighbourhood_10_4)|=0) & (|marking(Neighbourhood_19_17)|=0) & (|marking(Neighbourhood_15_4)|=0) & (|marking(Neighbourhood_8_5)|=0) & (|marking(Neighbourhood_5_16)|=0) & (|marking(Neighbourhood_18_6)|=0) & (|marking(Neighbourhood_18_3)|=0) & (|marking(Neighbourhood_20_3)|=0) & (|marking(Neighbourhood_1_6)|=0) & (|marking(Neighbourhood_6_15)|=0) & (|marking(Neighbourhood_18_20)|=0) & (|marking(Neighbourhood_16_18)|=0) & (|marking(Neighbourhood_13_20)|=0) & (|marking(Neighbourhood_14_1)|=0) & (|marking(Neighbourhood_6_14)|=0) & (|marking(Neighbourhood_12_11)|=0) & (|marking(Neighbourhood_14_13)|=0) & (|marking(Neighbourhood_13_4)|=0) & (|marking(Neighbourhood_2_5)|=0) & (|marking(Neighbourhood_7_8)|=0) & (|marking(Neighbourhood_8_8)|=0) & (|marking(Neighbourhood_10_3)|=0) & (|marking(Neighbourhood_18_1)|=0) & (|marking(Neighbourhood_8_20)|=0) & (|marking(Neighbourhood_4_12)|=0) & (|marking(Neighbourhood_3_2)|=0) & (|marking(Neighbourhood_3_18)|=0) & (|marking(Neighbourhood_12_2)|=0) & (|marking(Neighbourhood_9_16)|=0) & (|marking(Neighbourhood_4_8)|=0) & (|marking(Neighbourhood_9_15)|=0) & (|marking(Neighbourhood_3_9)|=0) & (|marking(Neighbourhood_17_3)|=0) & (|marking(Neighbourhood_9_11)|=0) & (|marking(Neighbourhood_9_10)|=0) & (|marking(Neighbourhood_2_11)|=0) & (|marking(Neighbourhood_4_17)|=0) & (|marking(Neighbourhood_8_14)|=0) & (|marking(Neighbourhood_20_9)|=0) & (|marking(Neighbourhood_10_13)|=0) & (|marking(Neighbourhood_2_19)|=0) & (|marking(Neighbourhood_2_4)|=0) & (|marking(Neighbourhood_7_7)|=0) & (|marking(Neighbourhood_15_17)|=0) & (|marking(Neighbourhood_9_12)|=0) & (|marking(Neighbourhood_3_3)|=0) & (|marking(Neighbourhood_8_16)|=0) & (|marking(Neighbourhood_13_3)|=0) & (|marking(Neighbourhood_4_1)|=0) & (|marking(Neighbourhood_13_2)|=0) & (|marking(Neighbourhood_2_3)|=0) & (|marking(Neighbourhood_12_17)|=0) & (|marking(Neighbourhood_6_18)|=0) & (|marking(Neighbourhood_15_12)|=0) & (|marking(Neighbourhood_9_8)|=0) & (|marking(Neighbourhood_18_9)|=0) & (|marking(Neighbourhood_19_1)|=0) & (|marking(Neighbourhood_17_6)|=0) & (|marking(Neighbourhood_13_1)|=0) & (|marking(Neighbourhood_16_8)|=0) & (|marking(Neighbourhood_20_12)|=0) & (|marking(Neighbourhood_16_2)|=0) & (|marking(Neighbourhood_18_4)|=0) & (|marking(Neighbourhood_19_16)|=0) & (|marking(Neighbourhood_6_1)|=0) & (|marking(Neighbourhood_4_16)|=0) & (|marking(Neighbourhood_18_13)|=0) & (|marking(Neighbourhood_10_8)|=0) & (|marking(Neighbourhood_3_6)|=0) & (|marking(Neighbourhood_15_1)|=0) & (|marking(Neighbourhood_3_4)|=0) & (|marking(Neighbourhood_7_15)|=0) & (|marking(Neighbourhood_12_20)|=0) & (|marking(Neighbourhood_14_4)|=0) & (|marking(Neighbourhood_17_4)|=0) & (|marking(Neighbourhood_16_13)|=0) & (|marking(Neighbourhood_1_13)|=0) & (|marking(Neighbourhood_9_6)|=0) & (|marking(Neighbourhood_2_8)|=0) & (|marking(Neighbourhood_7_1)|=0) & (|marking(Neighbourhood_19_20)|=0) & (|marking(Neighbourhood_11_5)|=0) & (|marking(Neighbourhood_16_10)|=0) & (|marking(Neighbourhood_19_3)|=0) & (|marking(Neighbourhood_5_3)|=0) & (|marking(Neighbourhood_12_1)|=0) & (|marking(Neighbourhood_11_17)|=0) & (|marking(Neighbourhood_19_2)|=0) & (|marking(Neighbourhood_16_11)|=0) & (|marking(Neighbourhood_1_3)|=0) & (|marking(Neighbourhood_20_14)|=0) & (|marking(Neighbourhood_14_7)|=0) & (|marking(Neighbourhood_7_5)|=0) & (|marking(Neighbourhood_16_5)|=0) & (|marking(Neighbourhood_18_14)|=0) & (|marking(Neighbourhood_9_20)|=0) & (|marking(Neighbourhood_14_2)|=0) & (|marking(Neighbourhood_1_9)|=0) & (|marking(Neighbourhood_7_2)|=0) & (|marking(Neighbourhood_4_4)|=0) & (|marking(Neighbourhood_6_7)|=0) & (|marking(Neighbourhood_3_12)|=0) & (|marking(Neighbourhood_11_15)|=0) & (|marking(Neighbourhood_4_10)|=0) & (|marking(Neighbourhood_13_13)|=0) & (|marking(Neighbourhood_11_7)|=0) & (|marking(Neighbourhood_15_6)|=0) & (|marking(Neighbourhood_10_12)|=0) & (|marking(Neighbourhood_20_19)|=0) & (|marking(Neighbourhood_17_9)|=0) & (|marking(Neighbourhood_16_3)|=0) & (|marking(Neighbourhood_10_11)|=0) & (|marking(Neighbourhood_12_16)|=0) & (|marking(Neighbourhood_11_13)|=0) & (|marking(Neighbourhood_13_18)|=0) & (|marking(Neighbourhood_15_5)|=0) & (|marking(Neighbourhood_3_11)|=0) & (|marking(Neighbourhood_13_16)|=0) & (|marking(Neighbourhood_14_18)|=0) & (|marking(Neighbourhood_3_13)|=0) & (|marking(Neighbourhood_8_11)|=0) & (|marking(Neighbourhood_8_6)|=0)))


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