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

Execution Outputs of marcie for Peterson/6 (P/T)

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

execution on node 34: cluster1u36.lip6.fr (runId=136966892701343_n_34)
=====================================================================
runnning marcie on Peterson-PT-6 (CTLCardinalityComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Peterson-PT-6, examination is CTLCardinalityComparison
=====================================================================

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

START 1369711065

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 1330 NrTr: 2030)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369711066

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

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

mcc/mcc_parse.cc:759: Exception: parse error ctl p_1860_cardinalitycomparison_eq_x: E F (A F ((|marking(Idle_6)|+|marking(Idle_1)|+|marking(Idle_0)|+|marking(Idle_3)|+|marking(Idle_5)|+|marking(Idle_2)|+|marking(Idle_4)|)!=(|marking(CS_1)|+|marking(CS_2)|+|marking(CS_3)|+|marking(CS_0)|+|marking(CS_6)|+|marking(CS_5)|+|marking(CS_4)|)) & X ((|marking(AskForSection_1_4)|+|marking(AskForSection_1_5)|+|marking(AskForSection_6_0)|+|marking(AskForSection_3_2)|+|marking(AskForSection_2_1)|+|marking(AskForSection_6_4)|+|marking(AskForSection_0_2)|+|marking(AskForSection_3_0)|+|marking(AskForSection_2_5)|+|marking(AskForSection_6_1)|+|marking(AskForSection_2_0)|+|marking(AskForSection_4_1)|+|marking(AskForSection_0_0)|+|marking(AskForSection_2_3)|+|marking(AskForSection_6_2)|+|marking(AskForSection_4_4)|+|marking(AskForSection_6_3)|+|marking(AskForSection_4_3)|+|marking(AskForSection_0_5)|+|marking(AskForSection_3_5)|+|marking(AskForSection_5_4)|+|marking(AskForSection_5_5)|+|marking(AskForSection_4_2)|+|marking(AskForSection_5_0)|+|marking(AskForSection_5_3)|+|marking(AskForSection_2_4)|+|marking(AskForSection_5_1)|+|marking(AskForSection_0_3)|+|marking(AskForSection_5_2)|+|marking(AskForSection_1_2)|+|marking(AskForSection_4_5)|+|marking(AskForSection_3_3)|+|marking(AskForSection_0_1)|+|marking(AskForSection_1_0)|+|marking(AskForSection_1_3)|+|marking(AskForSection_4_0)|+|marking(AskForSection_3_4)|+|marking(AskForSection_3_1)|+|marking(AskForSection_1_1)|+|marking(AskForSection_2_2)|+|marking(AskForSection_6_5)|+|marking(AskForSection_0_4)|)=(|marking(TestTurn_3_3)|+|marking(TestTurn_3_0)|+|marking(TestTurn_6_4)|+|marking(TestTurn_1_4)|+|marking(TestTurn_4_1)|+|marking(TestTurn_4_5)|+|marking(TestTurn_6_3)|+|marking(TestTurn_2_2)|+|marking(TestTurn_3_1)|+|marking(TestTurn_4_0)|+|marking(TestTurn_0_4)|+|marking(TestTurn_2_3)|+|marking(TestTurn_0_0)|+|marking(TestTurn_3_4)|+|marking(TestTurn_4_3)|+|marking(TestTurn_1_2)|+|marking(TestTurn_2_5)|+|marking(TestTurn_6_2)|+|marking(TestTurn_0_3)|+|marking(TestTurn_5_0)|+|marking(TestTurn_1_5)|+|marking(TestTurn_0_5)|+|marking(TestTurn_2_4)|+|marking(TestTurn_5_4)|+|marking(TestTurn_5_3)|+|marking(TestTurn_2_0)|+|marking(TestTurn_0_2)|+|marking(TestTurn_1_1)|+|marking(TestTurn_5_1)|+|marking(TestTurn_5_5)|+|marking(TestTurn_2_1)|+|marking(TestTurn_6_0)|+|marking(TestTurn_1_3)|+|marking(TestTurn_5_2)|+|marking(TestTurn_1_0)|+|marking(TestTurn_3_5)|+|marking(TestTurn_4_2)|+|marking(TestTurn_3_2)|+|marking(TestTurn_4_4)|+|marking(TestTurn_0_1)|+|marking(TestTurn_6_5)|+|marking(TestTurn_6_1)|)))
ctl p_1861_cardinalitycomparison_full_and: E G (((|marking(AskForSection_1_4)|+|marking(AskForSection_1_5)|+|marking(AskForSection_6_0)|+|marking(AskForSection_3_2)|+|marking(AskForSection_2_1)|+|marking(AskForSection_6_4)|+|marking(AskForSection_0_2)|+|marking(AskForSection_3_0)|+|marking(AskForSection_2_5)|+|marking(AskForSection_6_1)|+|marking(AskForSection_2_0)|+|marking(AskForSection_4_1)|+|marking(AskForSection_0_0)|+|marking(AskForSection_2_3)|+|marking(AskForSection_6_2)|+|marking(AskForSection_4_4)|+|marking(AskForSection_6_3)|+|marking(AskForSection_4_3)|+|marking(AskForSection_0_5)|+|marking(AskForSection_3_5)|+|marking(AskForSection_5_4)|+|marking(AskForSection_5_5)|+|marking(AskForSection_4_2)|+|marking(AskForSection_5_0)|+|marking(AskForSection_5_3)|+|marking(AskForSection_2_4)|+|marking(AskForSection_5_1)|+|marking(AskForSection_0_3)|+|marking(AskForSection_5_2)|+|marking(AskForSection_1_2)|+|marking(AskForSection_4_5)|+|marking(AskForSection_3_3)|+|marking(AskForSection_0_1)|+|marking(AskForSection_1_0)|+|marking(AskForSection_1_3)|+|marking(AskForSection_4_0)|+|marking(AskForSection_3_4)|+|marking(AskForSection_3_1)|+|marking(AskForSection_1_1)|+|marking(AskForSection_2_2)|+|marking(AskForSection_6_5)|+|marking(AskForSection_0_4)|)!=(|marking(TestTurn_3_3)|+|marking(TestTurn_3_0)|+|marking(TestTurn_6_4)|+|marking(TestTurn_1_4)|+|marking(TestTurn_4_1)|+|marking(TestTurn_4_5)|+|marking(TestTurn_6_3)|+|marking(TestTurn_2_2)|+|marking(TestTurn_3_1)|+|marking(TestTurn_4_0)|+|marking(TestTurn_0_4)|+|marking(TestTurn_2_3)|+|marking(TestTurn_0_0)|+|marking(TestTurn_3_4)|+|marking(TestTurn_4_3)|+|marking(TestTurn_1_2)|+|marking(TestTurn_2_5)|+|marking(TestTurn_6_2)|+|marking(TestTurn_0_3)|+|marking(TestTurn_5_0)|+|marking(TestTurn_1_5)|+|marking(TestTurn_0_5)|+|marking(TestTurn_2_4)|+|marking(TestTurn_5_4)|+|marking(TestTurn_5_3)|+|marking(TestTurn_2_0)|+|marking(TestTurn_0_2)|+|marking(TestTurn_1_1)|+|marking(TestTurn_5_1)|+|marking(TestTurn_5_5)|+|marking(TestTurn_2_1)|+|marking(TestTurn_6_0)|+|marking(TestTurn_1_3)|+|marking(TestTurn_5_2)|+|marking(TestTurn_1_0)|+|marking(TestTurn_3_5)|+|marking(TestTurn_4_2)|+|marking(TestTurn_3_2)|+|marking(TestTurn_4_4)|+|marking(TestTurn_0_1)|+|marking(TestTurn_6_5)|+|marking(TestTurn_6_1)|)) & ((|marking(TestIdentity_2_2_0)|+|marking(TestIdentity_6_0_4)|+|marking(TestIdentity_3_4_3)|+|marking(TestIdentity_0_4_3)|+|marking(TestIdentity_1_2_0)|+|marking(TestIdentity_6_4_1)|+|marking(TestIdentity_2_3_6)|+|marking(TestIdentity_5_4_1)|+|marking(TestIdentity_2_5_4)|+|marking(TestIdentity_3_4_2)|+|marking(TestIdentity_5_3_6)|+|marking(TestIdentity_2_2_5)|+|marking(TestIdentity_1_0_6)|+|marking(TestIdentity_5_4_5)|+|marking(TestIdentity_4_0_5)|+|marking(TestIdentity_1_2_2)|+|marking(TestIdentity_5_5_5)|+|marking(TestIdentity_2_4_6)|+|marking(TestIdentity_6_1_5)|+|marking(TestIdentity_1_4_1)|+|marking(TestIdentity_0_1_5)|+|marking(TestIdentity_6_3_5)|+|marking(TestIdentity_3_0_3)|+|marking(TestIdentity_0_3_2)|+|marking(TestIdentity_6_1_1)|+|marking(TestIdentity_2_3_2)|+|marking(TestIdentity_1_5_1)|+|marking(TestIdentity_0_4_5)|+|marking(TestIdentity_4_3_5)|+|marking(TestIdentity_4_3_6)|+|marking(TestIdentity_6_2_6)|+|marking(TestIdentity_1_4_5)|+|marking(TestIdentity_6_4_3)|+|marking(TestIdentity_5_1_3)|+|marking(TestIdentity_6_0_5)|+|marking(TestIdentity_4_0_0)|+|marking(TestIdentity_3_3_6)|+|marking(TestIdentity_2_2_2)|+|marking(TestIdentity_2_0_3)|+|marking(TestIdentity_0_3_3)|+|marking(TestIdentity_1_2_3)|+|marking(TestIdentity_3_2_3)|+|marking(TestIdentity_1_1_1)|+|marking(TestIdentity_3_2_1)|+|marking(TestIdentity_5_3_1)|+|marking(TestIdentity_2_4_3)|+|marking(TestIdentity_2_5_3)|+|marking(TestIdentity_2_0_4)|+|marking(TestIdentity_2_4_5)|+|marking(TestIdentity_6_2_3)|+|marking(TestIdentity_6_0_3)|+|marking(TestIdentity_6_5_0)|+|marking(TestIdentity_6_2_2)|+|marking(TestIdentity_6_3_6)|+|marking(TestIdentity_5_1_1)|+|marking(TestIdentity_4_0_3)|+|marking(TestIdentity_6_5_5)|+|marking(TestIdentity_5_0_5)|+|marking(TestIdentity_4_3_0)|+|marking(TestIdentity_0_3_5)|+|marking(TestIdentity_5_0_1)|+|marking(TestIdentity_3_3_0)|+|marking(TestIdentity_3_3_2)|+|marking(TestIdentity_4_1_1)|+|marking(TestIdentity_6_5_2)|+|marking(TestIdentity_1_3_4)|+|marking(TestIdentity_2_0_1)|+|marking(TestIdentity_5_5_6)|+|marking(TestIdentity_6_1_6)|+|marking(TestIdentity_4_5_2)|+|marking(TestIdentity_2_0_5)|+|marking(TestIdentity_1_2_5)|+|marking(TestIdentity_1_4_3)|+|marking(TestIdentity_4_0_1)|+|marking(TestIdentity_6_1_2)|+|marking(TestIdentity_3_5_1)|+|marking(TestIdentity_1_5_6)|+|marking(TestIdentity_0_0_1)|+|marking(TestIdentity_4_0_6)|+|marking(TestIdentity_3_5_6)|+|marking(TestIdentity_5_5_2)|+|marking(TestIdentity_2_4_1)|+|marking(TestIdentity_5_2_1)|+|marking(TestIdentity_0_2_6)|+|marking(TestIdentity_2_5_0)|+|marking(TestIdentity_2_4_4)|+|marking(TestIdentity_3_2_4)|+|marking(TestIdentity_1_5_5)|+|marking(TestIdentity_1_0_4)|+|marking(TestIdentity_5_3_4)|+|marking(TestIdentity_0_2_5)|+|marking(TestIdentity_1_2_1)|+|marking(TestIdentity_0_1_2)|+|marking(TestIdentity_0_2_4)|+|marking(TestIdentity_3_5_3)|+|marking(TestIdentity_3_5_4)|+|marking(TestIdentity_4_1_0)|+|marking(TestIdentity_5_4_2)|+|marking(TestIdentity_4_3_1)|+|marking(TestIdentity_1_3_6)|+|marking(TestIdentity_2_3_0)|+|marking(TestIdentity_0_4_4)|+|marking(TestIdentity_0_1_0)|+|marking(TestIdentity_0_5_5)|+|marking(TestIdentity_3_3_5)|+|marking(TestIdentity_0_4_2)|+|marking(TestIdentity_6_3_0)|+|marking(TestIdentity_3_3_1)|+|marking(TestIdentity_5_5_3)|+|marking(TestIdentity_0_4_6)|+|marking(TestIdentity_5_3_3)|+|marking(TestIdentity_0_1_3)|+|marking(TestIdentity_5_2_5)|+|marking(TestIdentity_5_2_4)|+|marking(TestIdentity_3_4_6)|+|marking(TestIdentity_3_4_4)|+|marking(TestIdentity_6_1_4)|+|marking(TestIdentity_3_4_5)|+|marking(TestIdentity_5_1_6)|+|marking(TestIdentity_1_1_0)|+|marking(TestIdentity_4_4_0)|+|marking(TestIdentity_6_0_0)|+|marking(TestIdentity_0_5_0)|+|marking(TestIdentity_3_4_1)|+|marking(TestIdentity_1_5_2)|+|marking(TestIdentity_6_2_4)|+|marking(TestIdentity_4_4_5)|+|marking(TestIdentity_0_1_4)|+|marking(TestIdentity_1_1_5)|+|marking(TestIdentity_1_0_3)|+|marking(TestIdentity_6_4_0)|+|marking(TestIdentity_3_0_1)|+|marking(TestIdentity_5_5_1)|+|marking(TestIdentity_5_1_0)|+|marking(TestIdentity_4_5_5)|+|marking(TestIdentity_4_1_2)|+|marking(TestIdentity_5_3_5)|+|marking(TestIdentity_3_1_3)|+|marking(TestIdentity_3_0_0)|+|marking(TestIdentity_6_0_2)|+|marking(TestIdentity_6_0_6)|+|marking(TestIdentity_3_2_5)|+|marking(TestIdentity_5_1_5)|+|marking(TestIdentity_1_1_4)|+|marking(TestIdentity_3_1_5)|+|marking(TestIdentity_3_0_4)|+|marking(TestIdentity_3_5_0)|+|marking(TestIdentity_3_0_2)|+|marking(TestIdentity_1_4_4)|+|marking(TestIdentity_3_3_3)|+|marking(TestIdentity_0_0_0)|+|marking(TestIdentity_2_1_3)|+|marking(TestIdentity_2_0_6)|+|marking(TestIdentity_0_5_3)|+|marking(TestIdentity_1_3_2)|+|marking(TestIdentity_2_2_6)|+|marking(TestIdentity_5_0_6)|+|marking(TestIdentity_0_4_1)|+|marking(TestIdentity_1_5_0)|+|marking(TestIdentity_4_4_1)|+|marking(TestIdentity_6_2_1)|+|marking(TestIdentity_5_3_2)|+|marking(TestIdentity_1_3_1)|+|marking(TestIdentity_0_5_4)|+|marking(TestIdentity_2_3_3)|+|marking(TestIdentity_5_1_2)|+|marking(TestIdentity_2_1_1)|+|marking(TestIdentity_3_1_6)|+|marking(TestIdentity_2_2_4)|+|marking(TestIdentity_4_1_4)|+|marking(TestIdentity_0_1_6)|+|marking(TestIdentity_1_4_0)|+|marking(TestIdentity_0_3_6)|+|marking(TestIdentity_5_4_3)|+|marking(TestIdentity_1_0_0)|+|marking(TestIdentity_4_5_0)|+|marking(TestIdentity_5_2_0)|+|marking(TestIdentity_0_0_5)|+|marking(TestIdentity_1_5_4)|+|marking(TestIdentity_5_4_6)|+|marking(TestIdentity_5_4_4)|+|marking(TestIdentity_1_1_2)|+|marking(TestIdentity_2_4_0)|+|marking(TestIdentity_0_2_0)|+|marking(TestIdentity_6_3_3)|+|marking(TestIdentity_3_2_6)|+|marking(TestIdentity_5_0_3)|+|marking(TestIdentity_4_4_2)|+|marking(TestIdentity_2_2_3)|+|marking(TestIdentity_1_0_5)|+|marking(TestIdentity_3_1_1)|+|marking(TestIdentity_5_2_6)|+|marking(TestIdentity_1_2_4)|+|marking(TestIdentity_2_5_6)|+|marking(TestIdentity_1_3_5)|+|marking(TestIdentity_1_2_6)|+|marking(TestIdentity_4_2_6)|+|marking(TestIdentity_5_0_2)|+|marking(TestIdentity_6_5_1)|+|marking(TestIdentity_2_3_4)|+|marking(TestIdentity_2_5_5)|+|marking(TestIdentity_2_0_0)|+|marking(TestIdentity_4_3_2)|+|marking(TestIdentity_2_5_1)|+|marking(TestIdentity_2_0_2)|+|marking(TestIdentity_4_2_5)|+|marking(TestIdentity_2_4_2)|+|marking(TestIdentity_0_2_2)|+|marking(TestIdentity_0_1_1)|+|marking(TestIdentity_1_1_3)|+|marking(TestIdentity_0_0_3)|+|marking(TestIdentity_2_3_1)|+|marking(TestIdentity_4_0_2)|+|marking(TestIdentity_6_5_3)|+|marking(TestIdentity_1_1_6)|+|marking(TestIdentity_3_1_0)|+|marking(TestIdentity_5_1_4)|+|marking(TestIdentity_4_2_0)|+|marking(TestIdentity_4_5_6)|+|marking(TestIdentity_5_3_0)|+|marking(TestIdentity_0_4_0)|+|marking(TestIdentity_4_1_3)|+|marking(TestIdentity_6_4_6)|+|marking(TestIdentity_6_4_5)|+|marking(TestIdentity_5_2_2)|+|marking(TestIdentity_6_3_1)|+|marking(TestIdentity_4_2_4)|+|marking(TestIdentity_2_1_0)|+|marking(TestIdentity_3_0_5)|+|marking(TestIdentity_4_4_6)|+|marking(TestIdentity_5_5_0)|+|marking(TestIdentity_6_1_0)|+|marking(TestIdentity_0_5_1)|+|marking(TestIdentity_2_1_5)|+|marking(TestIdentity_0_5_6)|+|marking(TestIdentity_2_5_2)|+|marking(TestIdentity_0_2_3)|+|marking(TestIdentity_2_1_6)|+|marking(TestIdentity_1_0_1)|+|marking(TestIdentity_3_2_2)|+|marking(TestIdentity_3_1_4)|+|marking(TestIdentity_3_1_2)|+|marking(TestIdentity_6_0_1)|+|marking(TestIdentity_6_5_6)|+|marking(TestIdentity_6_2_0)|+|marking(TestIdentity_4_1_5)|+|marking(TestIdentity_0_3_0)|+|marking(TestIdentity_6_1_3)|+|marking(TestIdentity_5_5_4)|+|marking(TestIdentity_0_3_1)|+|marking(TestIdentity_2_2_1)|+|marking(TestIdentity_4_5_4)|+|marking(TestIdentity_0_5_2)|+|marking(TestIdentity_2_3_5)|+|marking(TestIdentity_6_2_5)|+|marking(TestIdentity_4_1_6)|+|marking(TestIdentity_0_2_1)|+|marking(TestIdentity_4_2_3)|+|marking(TestIdentity_6_5_4)|+|marking(TestIdentity_6_4_4)|+|marking(TestIdentity_6_4_2)|+|marking(TestIdentity_2_1_4)|+|marking(TestIdentity_3_3_4)|+|marking(TestIdentity_4_3_3)|+|marking(TestIdentity_0_0_6)|+|marking(TestIdentity_3_5_2)|+|marking(TestIdentity_1_0_2)|+|marking(TestIdentity_4_5_1)|+|marking(TestIdentity_4_2_1)|+|marking(TestIdentity_0_0_4)|+|marking(TestIdentity_4_3_4)|+|marking(TestIdentity_3_4_0)|+|marking(TestIdentity_5_4_0)|+|marking(TestIdentity_1_3_0)|+|marking(TestIdentity_4_2_2)|+|marking(TestIdentity_5_0_0)|+|marking(TestIdentity_3_0_6)|+|marking(TestIdentity_5_0_4)|+|marking(TestIdentity_4_4_3)|+|marking(TestIdentity_0_3_4)|+|marking(TestIdentity_1_5_3)|+|marking(TestIdentity_4_4_4)|+|marking(TestIdentity_6_3_4)|+|marking(TestIdentity_1_4_6)|+|marking(TestIdentity_6_3_2)|+|marking(TestIdentity_5_2_3)|+|marking(TestIdentity_0_0_2)|+|marking(TestIdentity_4_0_4)|+|marking(TestIdentity_3_2_0)|+|marking(TestIdentity_1_4_2)|+|marking(TestIdentity_4_5_3)|+|marking(TestIdentity_2_1_2)|+|marking(TestIdentity_1_3_3)|+|marking(TestIdentity_3_5_5)|)<=(|marking(BeginLoop_6_0_6)|+|marking(BeginLoop_2_2_0)|+|marking(BeginLoop_0_4_6)|+|marking(BeginLoop_6_2_1)|+|marking(BeginLoop_3_1_0)|+|marking(BeginLoop_0_5_4)|+|marking(BeginLoop_0_0_6)|+|marking(BeginLoop_4_2_2)|+|marking(BeginLoop_6_5_6)|+|marking(BeginLoop_6_2_2)|+|marking(BeginLoop_2_2_6)|+|marking(BeginLoop_2_4_1)|+|marking(BeginLoop_4_3_3)|+|marking(BeginLoop_4_4_6)|+|marking(BeginLoop_0_5_2)|+|marking(BeginLoop_4_4_4)|+|marking(BeginLoop_0_0_3)|+|marking(BeginLoop_1_3_3)|+|marking(BeginLoop_6_5_4)|+|marking(BeginLoop_2_3_3)|+|marking(BeginLoop_0_3_6)|+|marking(BeginLoop_1_2_4)|+|marking(BeginLoop_1_0_5)|+|marking(BeginLoop_6_5_2)|+|marking(BeginLoop_5_5_5)|+|marking(BeginLoop_2_0_5)|+|marking(BeginLoop_6_0_1)|+|marking(BeginLoop_3_4_1)|+|marking(BeginLoop_1_0_4)|+|marking(BeginLoop_2_1_5)|+|marking(BeginLoop_5_0_4)|+|marking(BeginLoop_0_5_0)|+|marking(BeginLoop_0_1_0)|+|marking(BeginLoop_3_5_3)|+|marking(BeginLoop_0_4_0)|+|marking(BeginLoop_4_2_3)|+|marking(BeginLoop_4_3_4)|+|marking(BeginLoop_3_4_3)|+|marking(BeginLoop_4_2_6)|+|marking(BeginLoop_4_3_2)|+|marking(BeginLoop_1_2_1)|+|marking(BeginLoop_0_4_2)|+|marking(BeginLoop_0_1_3)|+|marking(BeginLoop_1_4_0)|+|marking(BeginLoop_0_1_6)|+|marking(BeginLoop_6_3_2)|+|marking(BeginLoop_6_4_0)|+|marking(BeginLoop_3_3_6)|+|marking(BeginLoop_6_5_1)|+|marking(BeginLoop_4_1_0)|+|marking(BeginLoop_5_1_0)|+|marking(BeginLoop_2_3_2)|+|marking(BeginLoop_3_4_4)|+|marking(BeginLoop_5_4_6)|+|marking(BeginLoop_0_5_1)|+|marking(BeginLoop_2_2_5)|+|marking(BeginLoop_3_5_2)|+|marking(BeginLoop_3_2_1)|+|marking(BeginLoop_6_4_3)|+|marking(BeginLoop_1_1_1)|+|marking(BeginLoop_1_5_1)|+|marking(BeginLoop_6_0_0)|+|marking(BeginLoop_3_5_1)|+|marking(BeginLoop_2_5_2)|+|marking(BeginLoop_4_1_5)|+|marking(BeginLoop_4_3_1)|+|marking(BeginLoop_5_0_3)|+|marking(BeginLoop_1_3_5)|+|marking(BeginLoop_3_1_1)|+|marking(BeginLoop_5_4_2)|+|marking(BeginLoop_1_1_5)|+|marking(BeginLoop_3_5_5)|+|marking(BeginLoop_1_2_3)|+|marking(BeginLoop_1_0_0)|+|marking(BeginLoop_0_3_0)|+|marking(BeginLoop_0_3_2)|+|marking(BeginLoop_5_3_2)|+|marking(BeginLoop_6_3_3)|+|marking(BeginLoop_3_3_2)|+|marking(BeginLoop_2_3_5)|+|marking(BeginLoop_0_2_5)|+|marking(BeginLoop_2_1_1)|+|marking(BeginLoop_5_3_3)|+|marking(BeginLoop_5_5_6)|+|marking(BeginLoop_3_3_0)|+|marking(BeginLoop_0_2_2)|+|marking(BeginLoop_5_2_2)|+|marking(BeginLoop_0_5_6)|+|marking(BeginLoop_4_2_4)|+|marking(BeginLoop_5_4_4)|+|marking(BeginLoop_1_5_3)|+|marking(BeginLoop_3_1_3)|+|marking(BeginLoop_5_0_5)|+|marking(BeginLoop_4_0_6)|+|marking(BeginLoop_2_2_1)|+|marking(BeginLoop_5_5_0)|+|marking(BeginLoop_4_1_1)|+|marking(BeginLoop_3_0_5)|+|marking(BeginLoop_4_5_1)|+|marking(BeginLoop_0_4_4)|+|marking(BeginLoop_0_2_1)|+|marking(BeginLoop_6_2_3)|+|marking(BeginLoop_3_3_5)|+|marking(BeginLoop_2_5_0)|+|marking(BeginLoop_3_0_1)|+|marking(BeginLoop_2_4_0)|+|marking(BeginLoop_6_2_4)|+|marking(BeginLoop_1_4_1)|+|marking(BeginLoop_6_3_1)|+|marking(BeginLoop_6_2_6)|+|marking(BeginLoop_3_0_6)|+|marking(BeginLoop_5_1_1)|+|marking(BeginLoop_0_3_5)|+|marking(BeginLoop_4_0_3)|+|marking(BeginLoop_2_2_2)|+|marking(BeginLoop_5_3_0)|+|marking(BeginLoop_3_4_0)|+|marking(BeginLoop_4_4_1)|+|marking(BeginLoop_2_1_2)|+|marking(BeginLoop_0_0_1)|+|marking(BeginLoop_3_0_2)|+|marking(BeginLoop_5_2_6)|+|marking(BeginLoop_2_3_0)|+|marking(BeginLoop_4_4_3)|+|marking(BeginLoop_5_1_5)|+|marking(BeginLoop_4_5_3)|+|marking(BeginLoop_4_0_4)|+|marking(BeginLoop_4_0_0)|+|marking(BeginLoop_6_5_0)|+|marking(BeginLoop_4_0_2)|+|marking(BeginLoop_0_2_0)|+|marking(BeginLoop_3_0_3)|+|marking(BeginLoop_4_1_2)|+|marking(BeginLoop_4_1_6)|+|marking(BeginLoop_5_1_2)|+|marking(BeginLoop_3_0_4)|+|marking(BeginLoop_4_3_6)|+|marking(BeginLoop_5_4_3)|+|marking(BeginLoop_1_5_5)|+|marking(BeginLoop_1_3_0)|+|marking(BeginLoop_0_1_4)|+|marking(BeginLoop_1_4_5)|+|marking(BeginLoop_1_4_3)|+|marking(BeginLoop_0_2_3)|+|marking(BeginLoop_0_5_3)|+|marking(BeginLoop_5_3_5)|+|marking(BeginLoop_3_3_1)|+|marking(BeginLoop_1_4_4)|+|marking(BeginLoop_1_5_0)|+|marking(BeginLoop_2_5_6)|+|marking(BeginLoop_6_4_6)|+|marking(BeginLoop_0_4_5)|+|marking(BeginLoop_5_0_2)|+|marking(BeginLoop_0_1_2)|+|marking(BeginLoop_1_3_6)|+|marking(BeginLoop_0_1_1)|+|marking(BeginLoop_5_0_6)|+|marking(BeginLoop_0_0_2)|+|marking(BeginLoop_6_3_4)|+|marking(BeginLoop_0_3_3)|+|marking(BeginLoop_3_2_5)|+|marking(BeginLoop_1_1_6)|+|marking(BeginLoop_2_1_6)|+|marking(BeginLoop_2_5_5)|+|marking(BeginLoop_4_5_2)|+|marking(BeginLoop_1_5_2)|+|marking(BeginLoop_5_5_3)|+|marking(BeginLoop_5_5_2)|+|marking(BeginLoop_0_3_4)|+|marking(BeginLoop_2_4_6)|+|marking(BeginLoop_6_3_0)|+|marking(BeginLoop_1_0_6)|+|marking(BeginLoop_1_5_6)|+|marking(BeginLoop_2_0_4)|+|marking(BeginLoop_6_5_5)|+|marking(BeginLoop_5_2_0)|+|marking(BeginLoop_0_5_5)|+|marking(BeginLoop_6_5_3)|+|marking(BeginLoop_4_3_0)|+|marking(BeginLoop_5_3_4)|+|marking(BeginLoop_3_1_6)|+|marking(BeginLoop_3_1_5)|+|marking(BeginLoop_5_0_0)|+|marking(BeginLoop_6_0_2)|+|marking(BeginLoop_4_4_2)|+|marking(BeginLoop_1_0_3)|+|marking(BeginLoop_5_1_3)|+|marking(BeginLoop_6_3_6)|+|marking(BeginLoop_2_5_4)|+|marking(BeginLoop_4_4_0)|+|marking(BeginLoop_5_2_4)|+|marking(BeginLoop_6_1_0)|+|marking(BeginLoop_4_0_5)|+|marking(BeginLoop_5_2_1)|+|marking(BeginLoop_0_2_6)|+|marking(BeginLoop_4_0_1)|+|marking(BeginLoop_0_0_5)|+|marking(BeginLoop_6_4_4)|+|marking(BeginLoop_5_4_0)|+|marking(BeginLoop_1_5_4)|+|marking(BeginLoop_4_5_5)|+|marking(BeginLoop_1_1_3)|+|marking(BeginLoop_2_0_0)|+|marking(BeginLoop_5_3_6)|+|marking(BeginLoop_6_2_5)|+|marking(BeginLoop_5_5_4)|+|marking(BeginLoop_1_3_2)|+|marking(BeginLoop_3_1_2)|+|marking(BeginLoop_4_5_0)|+|marking(BeginLoop_3_0_0)|+|marking(BeginLoop_2_3_4)|+|marking(BeginLoop_6_4_5)|+|marking(BeginLoop_1_1_2)|+|marking(BeginLoop_1_1_0)|+|marking(BeginLoop_0_1_5)|+|marking(BeginLoop_1_2_6)|+|marking(BeginLoop_0_3_1)|+|marking(BeginLoop_2_5_1)|+|marking(BeginLoop_1_0_2)|+|marking(BeginLoop_2_4_5)|+|marking(BeginLoop_6_1_3)|+|marking(BeginLoop_2_0_3)|+|marking(BeginLoop_5_5_1)|+|marking(BeginLoop_3_3_3)|+|marking(BeginLoop_3_5_4)|+|marking(BeginLoop_2_3_6)|+|marking(BeginLoop_2_4_2)|+|marking(BeginLoop_5_2_3)|+|marking(BeginLoop_6_2_0)|+|marking(BeginLoop_3_3_4)|+|marking(BeginLoop_1_2_2)|+|marking(BeginLoop_5_2_5)|+|marking(BeginLoop_2_4_4)|+|marking(BeginLoop_2_1_4)|+|marking(BeginLoop_2_1_0)|+|marking(BeginLoop_4_1_4)|+|marking(BeginLoop_4_5_6)|+|marking(BeginLoop_5_1_6)|+|marking(BeginLoop_1_4_2)|+|marking(BeginLoop_6_0_5)|+|marking(BeginLoop_3_2_6)|+|marking(BeginLoop_0_0_4)|+|marking(BeginLoop_1_1_4)|+|marking(BeginLoop_3_4_2)|+|marking(BeginLoop_2_5_3)|+|marking(BeginLoop_2_0_1)|+|marking(BeginLoop_6_1_1)|+|marking(BeginLoop_3_5_0)|+|marking(BeginLoop_3_5_6)|+|marking(BeginLoop_3_2_2)|+|marking(BeginLoop_4_5_4)|+|marking(BeginLoop_5_3_1)|+|marking(BeginLoop_2_2_3)|+|marking(BeginLoop_2_3_1)|+|marking(BeginLoop_6_0_3)|+|marking(BeginLoop_1_2_5)|+|marking(BeginLoop_1_4_6)|+|marking(BeginLoop_1_0_1)|+|marking(BeginLoop_4_2_1)|+|marking(BeginLoop_3_2_3)|+|marking(BeginLoop_1_2_0)|+|marking(BeginLoop_6_1_5)|+|marking(BeginLoop_1_3_4)|+|marking(BeginLoop_1_3_1)|+|marking(BeginLoop_5_4_1)|+|marking(BeginLoop_3_1_4)|+|marking(BeginLoop_4_1_3)|+|marking(BeginLoop_5_0_1)|+|marking(BeginLoop_2_0_6)|+|marking(BeginLoop_2_0_2)|+|marking(BeginLoop_0_4_1)|+|marking(BeginLoop_6_4_1)|+|marking(BeginLoop_6_0_4)|+|marking(BeginLoop_0_0_0)|+|marking(BeginLoop_6_4_2)|+|marking(BeginLoop_5_4_5)|+|marking(BeginLoop_4_2_5)|+|marking(BeginLoop_2_1_3)|+|marking(BeginLoop_0_4_3)|+|marking(BeginLoop_2_4_3)|+|marking(BeginLoop_6_1_4)|+|marking(BeginLoop_5_1_4)|+|marking(BeginLoop_4_4_5)|+|marking(BeginLoop_4_3_5)|+|marking(BeginLoop_0_2_4)|+|marking(BeginLoop_6_1_6)|+|marking(BeginLoop_3_2_0)|+|marking(BeginLoop_3_4_5)|+|marking(BeginLoop_6_1_2)|+|marking(BeginLoop_6_3_5)|+|marking(BeginLoop_3_4_6)|+|marking(BeginLoop_2_2_4)|+|marking(BeginLoop_3_2_4)|+|marking(BeginLoop_4_2_0)|)))
ctl p_1862_cardinalitycomparison_full_or: E G (((|marking(AskForSection_1_4)|+|marking(AskForSection_1_5)|+|marking(AskForSection_6_0)|+|marking(AskForSection_3_2)|+|marking(AskForSection_2_1)|+|marking(AskForSection_6_4)|+|marking(AskForSection_0_2)|+|marking(AskForSection_3_0)|+|marking(AskForSection_2_5)|+|marking(AskForSection_6_1)|+|marking(AskForSection_2_0)|+|marking(AskForSection_4_1)|+|marking(AskForSection_0_0)|+|marking(AskForSection_2_3)|+|marking(AskForSection_6_2)|+|marking(AskForSection_4_4)|+|marking(AskForSection_6_3)|+|marking(AskForSection_4_3)|+|marking(AskForSection_0_5)|+|marking(AskForSection_3_5)|+|marking(AskForSection_5_4)|+|marking(AskForSection_5_5)|+|marking(AskForSection_4_2)|+|marking(AskForSection_5_0)|+|marking(AskForSection_5_3)|+|marking(AskForSection_2_4)|+|marking(AskForSection_5_1)|+|marking(AskForSection_0_3)|+|marking(AskForSection_5_2)|+|marking(AskForSection_1_2)|+|marking(AskForSection_4_5)|+|marking(AskForSection_3_3)|+|marking(AskForSection_0_1)|+|marking(AskForSection_1_0)|+|marking(AskForSection_1_3)|+|marking(AskForSection_4_0)|+|marking(AskForSection_3_4)|+|marking(AskForSection_3_1)|+|marking(AskForSection_1_1)|+|marking(AskForSection_2_2)|+|marking(AskForSection_6_5)|+|marking(AskForSection_0_4)|)!=(|marking(TestTurn_3_3)|+|marking(TestTurn_3_0)|+|marking(TestTurn_6_4)|+|marking(TestTurn_1_4)|+|marking(TestTurn_4_1)|+|marking(TestTurn_4_5)|+|marking(TestTurn_6_3)|+|marking(TestTurn_2_2)|+|marking(TestTurn_3_1)|+|marking(TestTurn_4_0)|+|marking(TestTurn_0_4)|+|marking(TestTurn_2_3)|+|marking(TestTurn_0_0)|+|marking(TestTurn_3_4)|+|marking(TestTurn_4_3)|+|marking(TestTurn_1_2)|+|marking(TestTurn_2_5)|+|marking(TestTurn_6_2)|+|marking(TestTurn_0_3)|+|marking(TestTurn_5_0)|+|marking(TestTurn_1_5)|+|marking(TestTurn_0_5)|+|marking(TestTurn_2_4)|+|marking(TestTurn_5_4)|+|marking(TestTurn_5_3)|+|marking(TestTurn_2_0)|+|marking(TestTurn_0_2)|+|marking(TestTurn_1_1)|+|marking(TestTurn_5_1)|+|marking(TestTurn_5_5)|+|marking(TestTurn_2_1)|+|marking(TestTurn_6_0)|+|marking(TestTurn_1_3)|+|marking(TestTurn_5_2)|+|marking(TestTurn_1_0)|+|marking(TestTurn_3_5)|+|marking(TestTurn_4_2)|+|marking(TestTurn_3_2)|+|marking(TestTurn_4_4)|+|marking(TestTurn_0_1)|+|marking(TestTurn_6_5)|+|marking(TestTurn_6_1)|)) | ((|marking(TestIdentity_2_2_0)|+|marking(TestIdentity_6_0_4)|+|marking(TestIdentity_3_4_3)|+|marking(TestIdentity_0_4_3)|+|marking(TestIdentity_1_2_0)|+|marking(TestIdentity_6_4_1)|+|marking(TestIdentity_2_3_6)|+|marking(TestIdentity_5_4_1)|+|marking(TestIdentity_2_5_4)|+|marking(TestIdentity_3_4_2)|+|marking(TestIdentity_5_3_6)|+|marking(TestIdentity_2_2_5)|+|marking(TestIdentity_1_0_6)|+|marking(TestIdentity_5_4_5)|+|marking(TestIdentity_4_0_5)|+|marking(TestIdentity_1_2_2)|+|marking(TestIdentity_5_5_5)|+|marking(TestIdentity_2_4_6)|+|marking(TestIdentity_6_1_5)|+|marking(TestIdentity_1_4_1)|+|marking(TestIdentity_0_1_5)|+|marking(TestIdentity_6_3_5)|+|marking(TestIdentity_3_0_3)|+|marking(TestIdentity_0_3_2)|+|marking(TestIdentity_6_1_1)|+|marking(TestIdentity_2_3_2)|+|marking(TestIdentity_1_5_1)|+|marking(TestIdentity_0_4_5)|+|marking(TestIdentity_4_3_5)|+|marking(TestIdentity_4_3_6)|+|marking(TestIdentity_6_2_6)|+|marking(TestIdentity_1_4_5)|+|marking(TestIdentity_6_4_3)|+|marking(TestIdentity_5_1_3)|+|marking(TestIdentity_6_0_5)|+|marking(TestIdentity_4_0_0)|+|marking(TestIdentity_3_3_6)|+|marking(TestIdentity_2_2_2)|+|marking(TestIdentity_2_0_3)|+|marking(TestIdentity_0_3_3)|+|marking(TestIdentity_1_2_3)|+|marking(TestIdentity_3_2_3)|+|marking(TestIdentity_1_1_1)|+|marking(TestIdentity_3_2_1)|+|marking(TestIdentity_5_3_1)|+|marking(TestIdentity_2_4_3)|+|marking(TestIdentity_2_5_3)|+|marking(TestIdentity_2_0_4)|+|marking(TestIdentity_2_4_5)|+|marking(TestIdentity_6_2_3)|+|marking(TestIdentity_6_0_3)|+|marking(TestIdentity_6_5_0)|+|marking(TestIdentity_6_2_2)|+|marking(TestIdentity_6_3_6)|+|marking(TestIdentity_5_1_1)|+|marking(TestIdentity_4_0_3)|+|marking(TestIdentity_6_5_5)|+|marking(TestIdentity_5_0_5)|+|marking(TestIdentity_4_3_0)|+|marking(TestIdentity_0_3_5)|+|marking(TestIdentity_5_0_1)|+|marking(TestIdentity_3_3_0)|+|marking(TestIdentity_3_3_2)|+|marking(TestIdentity_4_1_1)|+|marking(TestIdentity_6_5_2)|+|marking(TestIdentity_1_3_4)|+|marking(TestIdentity_2_0_1)|+|marking(TestIdentity_5_5_6)|+|marking(TestIdentity_6_1_6)|+|marking(TestIdentity_4_5_2)|+|marking(TestIdentity_2_0_5)|+|marking(TestIdentity_1_2_5)|+|marking(TestIdentity_1_4_3)|+|marking(TestIdentity_4_0_1)|+|marking(TestIdentity_6_1_2)|+|marking(TestIdentity_3_5_1)|+|marking(TestIdentity_1_5_6)|+|marking(TestIdentity_0_0_1)|+|marking(TestIdentity_4_0_6)|+|marking(TestIdentity_3_5_6)|+|marking(TestIdentity_5_5_2)|+|marking(TestIdentity_2_4_1)|+|marking(TestIdentity_5_2_1)|+|marking(TestIdentity_0_2_6)|+|marking(TestIdentity_2_5_0)|+|marking(TestIdentity_2_4_4)|+|marking(TestIdentity_3_2_4)|+|marking(TestIdentity_1_5_5)|+|marking(TestIdentity_1_0_4)|+|marking(TestIdentity_5_3_4)|+|marking(TestIdentity_0_2_5)|+|marking(TestIdentity_1_2_1)|+|marking(TestIdentity_0_1_2)|+|marking(TestIdentity_0_2_4)|+|marking(TestIdentity_3_5_3)|+|marking(TestIdentity_3_5_4)|+|marking(TestIdentity_4_1_0)|+|marking(TestIdentity_5_4_2)|+|marking(TestIdentity_4_3_1)|+|marking(TestIdentity_1_3_6)|+|marking(TestIdentity_2_3_0)|+|marking(TestIdentity_0_4_4)|+|marking(TestIdentity_0_1_0)|+|marking(TestIdentity_0_5_5)|+|marking(TestIdentity_3_3_5)|+|marking(TestIdentity_0_4_2)|+|marking(TestIdentity_6_3_0)|+|marking(TestIdentity_3_3_1)|+|marking(TestIdentity_5_5_3)|+|marking(TestIdentity_0_4_6)|+|marking(TestIdentity_5_3_3)|+|marking(TestIdentity_0_1_3)|+|marking(TestIdentity_5_2_5)|+|marking(TestIdentity_5_2_4)|+|marking(TestIdentity_3_4_6)|+|marking(TestIdentity_3_4_4)|+|marking(TestIdentity_6_1_4)|+|marking(TestIdentity_3_4_5)|+|marking(TestIdentity_5_1_6)|+|marking(TestIdentity_1_1_0)|+|marking(TestIdentity_4_4_0)|+|marking(TestIdentity_6_0_0)|+|marking(TestIdentity_0_5_0)|+|marking(TestIdentity_3_4_1)|+|marking(TestIdentity_1_5_2)|+|marking(TestIdentity_6_2_4)|+|marking(TestIdentity_4_4_5)|+|marking(TestIdentity_0_1_4)|+|marking(TestIdentity_1_1_5)|+|marking(TestIdentity_1_0_3)|+|marking(TestIdentity_6_4_0)|+|marking(TestIdentity_3_0_1)|+|marking(TestIdentity_5_5_1)|+|marking(TestIdentity_5_1_0)|+|marking(TestIdentity_4_5_5)|+|marking(TestIdentity_4_1_2)|+|marking(TestIdentity_5_3_5)|+|marking(TestIdentity_3_1_3)|+|marking(TestIdentity_3_0_0)|+|marking(TestIdentity_6_0_2)|+|marking(TestIdentity_6_0_6)|+|marking(TestIdentity_3_2_5)|+|marking(TestIdentity_5_1_5)|+|marking(TestIdentity_1_1_4)|+|marking(TestIdentity_3_1_5)|+|marking(TestIdentity_3_0_4)|+|marking(TestIdentity_3_5_0)|+|marking(TestIdentity_3_0_2)|+|marking(TestIdentity_1_4_4)|+|marking(TestIdentity_3_3_3)|+|marking(TestIdentity_0_0_0)|+|marking(TestIdentity_2_1_3)|+|marking(TestIdentity_2_0_6)|+|marking(TestIdentity_0_5_3)|+|marking(TestIdentity_1_3_2)|+|marking(TestIdentity_2_2_6)|+|marking(TestIdentity_5_0_6)|+|marking(TestIdentity_0_4_1)|+|marking(TestIdentity_1_5_0)|+|marking(TestIdentity_4_4_1)|+|marking(TestIdentity_6_2_1)|+|marking(TestIdentity_5_3_2)|+|marking(TestIdentity_1_3_1)|+|marking(TestIdentity_0_5_4)|+|marking(TestIdentity_2_3_3)|+|marking(TestIdentity_5_1_2)|+|marking(TestIdentity_2_1_1)|+|marking(TestIdentity_3_1_6)|+|marking(TestIdentity_2_2_4)|+|marking(TestIdentity_4_1_4)|+|marking(TestIdentity_0_1_6)|+|marking(TestIdentity_1_4_0)|+|marking(TestIdentity_0_3_6)|+|marking(TestIdentity_5_4_3)|+|marking(TestIdentity_1_0_0)|+|marking(TestIdentity_4_5_0)|+|marking(TestIdentity_5_2_0)|+|marking(TestIdentity_0_0_5)|+|marking(TestIdentity_1_5_4)|+|marking(TestIdentity_5_4_6)|+|marking(TestIdentity_5_4_4)|+|marking(TestIdentity_1_1_2)|+|marking(TestIdentity_2_4_0)|+|marking(TestIdentity_0_2_0)|+|marking(TestIdentity_6_3_3)|+|marking(TestIdentity_3_2_6)|+|marking(TestIdentity_5_0_3)|+|marking(TestIdentity_4_4_2)|+|marking(TestIdentity_2_2_3)|+|marking(TestIdentity_1_0_5)|+|marking(TestIdentity_3_1_1)|+|marking(TestIdentity_5_2_6)|+|marking(TestIdentity_1_2_4)|+|marking(TestIdentity_2_5_6)|+|marking(TestIdentity_1_3_5)|+|marking(TestIdentity_1_2_6)|+|marking(TestIdentity_4_2_6)|+|marking(TestIdentity_5_0_2)|+|marking(TestIdentity_6_5_1)|+|marking(TestIdentity_2_3_4)|+|marking(TestIdentity_2_5_5)|+|marking(TestIdentity_2_0_0)|+|marking(TestIdentity_4_3_2)|+|marking(TestIdentity_2_5_1)|+|marking(TestIdentity_2_0_2)|+|marking(TestIdentity_4_2_5)|+|marking(TestIdentity_2_4_2)|+|marking(TestIdentity_0_2_2)|+|marking(TestIdentity_0_1_1)|+|marking(TestIdentity_1_1_3)|+|marking(TestIdentity_0_0_3)|+|marking(TestIdentity_2_3_1)|+|marking(TestIdentity_4_0_2)|+|marking(TestIdentity_6_5_3)|+|marking(TestIdentity_1_1_6)|+|marking(TestIdentity_3_1_0)|+|marking(TestIdentity_5_1_4)|+|marking(TestIdentity_4_2_0)|+|marking(TestIdentity_4_5_6)|+|marking(TestIdentity_5_3_0)|+|marking(TestIdentity_0_4_0)|+|marking(TestIdentity_4_1_3)|+|marking(TestIdentity_6_4_6)|+|marking(TestIdentity_6_4_5)|+|marking(TestIdentity_5_2_2)|+|marking(TestIdentity_6_3_1)|+|marking(TestIdentity_4_2_4)|+|marking(TestIdentity_2_1_0)|+|marking(TestIdentity_3_0_5)|+|marking(TestIdentity_4_4_6)|+|marking(TestIdentity_5_5_0)|+|marking(TestIdentity_6_1_0)|+|marking(TestIdentity_0_5_1)|+|marking(TestIdentity_2_1_5)|+|marking(TestIdentity_0_5_6)|+|marking(TestIdentity_2_5_2)|+|marking(TestIdentity_0_2_3)|+|marking(TestIdentity_2_1_6)|+|marking(TestIdentity_1_0_1)|+|marking(TestIdentity_3_2_2)|+|marking(TestIdentity_3_1_4)|+|marking(TestIdentity_3_1_2)|+|marking(TestIdentity_6_0_1)|+|marking(TestIdentity_6_5_6)|+|marking(TestIdentity_6_2_0)|+|marking(TestIdentity_4_1_5)|+|marking(TestIdentity_0_3_0)|+|marking(TestIdentity_6_1_3)|+|marking(TestIdentity_5_5_4)|+|marking(TestIdentity_0_3_1)|+|marking(TestIdentity_2_2_1)|+|marking(TestIdentity_4_5_4)|+|marking(TestIdentity_0_5_2)|+|marking(TestIdentity_2_3_5)|+|marking(TestIdentity_6_2_5)|+|marking(TestIdentity_4_1_6)|+|marking(TestIdentity_0_2_1)|+|marking(TestIdentity_4_2_3)|+|marking(TestIdentity_6_5_4)|+|marking(TestIdentity_6_4_4)|+|marking(TestIdentity_6_4_2)|+|marking(TestIdentity_2_1_4)|+|marking(TestIdentity_3_3_4)|+|marking(TestIdentity_4_3_3)|+|marking(TestIdentity_0_0_6)|+|marking(TestIdentity_3_5_2)|+|marking(TestIdentity_1_0_2)|+|marking(TestIdentity_4_5_1)|+|marking(TestIdentity_4_2_1)|+|marking(TestIdentity_0_0_4)|+|marking(TestIdentity_4_3_4)|+|marking(TestIdentity_3_4_0)|+|marking(TestIdentity_5_4_0)|+|marking(TestIdentity_1_3_0)|+|marking(TestIdentity_4_2_2)|+|marking(TestIdentity_5_0_0)|+|marking(TestIdentity_3_0_6)|+|marking(TestIdentity_5_0_4)|+|marking(TestIdentity_4_4_3)|+|marking(TestIdentity_0_3_4)|+|marking(TestIdentity_1_5_3)|+|marking(TestIdentity_4_4_4)|+|marking(TestIdentity_6_3_4)|+|marking(TestIdentity_1_4_6)|+|marking(TestIdentity_6_3_2)|+|marking(TestIdentity_5_2_3)|+|marking(TestIdentity_0_0_2)|+|marking(TestIdentity_4_0_4)|+|marking(TestIdentity_3_2_0)|+|marking(TestIdentity_1_4_2)|+|marking(TestIdentity_4_5_3)|+|marking(TestIdentity_2_1_2)|+|marking(TestIdentity_1_3_3)|+|marking(TestIdentity_3_5_5)|)<=(|marking(BeginLoop_6_0_6)|+|marking(BeginLoop_2_2_0)|+|marking(BeginLoop_0_4_6)|+|marking(BeginLoop_6_2_1)|+|marking(BeginLoop_3_1_0)|+|marking(BeginLoop_0_5_4)|+|marking(BeginLoop_0_0_6)|+|marking(BeginLoop_4_2_2)|+|marking(BeginLoop_6_5_6)|+|marking(BeginLoop_6_2_2)|+|marking(BeginLoop_2_2_6)|+|marking(BeginLoop_2_4_1)|+|marking(BeginLoop_4_3_3)|+|marking(BeginLoop_4_4_6)|+|marking(BeginLoop_0_5_2)|+|marking(BeginLoop_4_4_4)|+|marking(BeginLoop_0_0_3)|+|marking(BeginLoop_1_3_3)|+|marking(BeginLoop_6_5_4)|+|marking(BeginLoop_2_3_3)|+|marking(BeginLoop_0_3_6)|+|marking(BeginLoop_1_2_4)|+|marking(BeginLoop_1_0_5)|+|marking(BeginLoop_6_5_2)|+|marking(BeginLoop_5_5_5)|+|marking(BeginLoop_2_0_5)|+|marking(BeginLoop_6_0_1)|+|marking(BeginLoop_3_4_1)|+|marking(BeginLoop_1_0_4)|+|marking(BeginLoop_2_1_5)|+|marking(BeginLoop_5_0_4)|+|marking(BeginLoop_0_5_0)|+|marking(BeginLoop_0_1_0)|+|marking(BeginLoop_3_5_3)|+|marking(BeginLoop_0_4_0)|+|marking(BeginLoop_4_2_3)|+|marking(BeginLoop_4_3_4)|+|marking(BeginLoop_3_4_3)|+|marking(BeginLoop_4_2_6)|+|marking(BeginLoop_4_3_2)|+|marking(BeginLoop_1_2_1)|+|marking(BeginLoop_0_4_2)|+|marking(BeginLoop_0_1_3)|+|marking(BeginLoop_1_4_0)|+|marking(BeginLoop_0_1_6)|+|marking(BeginLoop_6_3_2)|+|marking(BeginLoop_6_4_0)|+|marking(BeginLoop_3_3_6)|+|marking(BeginLoop_6_5_1)|+|marking(BeginLoop_4_1_0)|+|marking(BeginLoop_5_1_0)|+|marking(BeginLoop_2_3_2)|+|marking(BeginLoop_3_4_4)|+|marking(BeginLoop_5_4_6)|+|marking(BeginLoop_0_5_1)|+|marking(BeginLoop_2_2_5)|+|marking(BeginLoop_3_5_2)|+|marking(BeginLoop_3_2_1)|+|marking(BeginLoop_6_4_3)|+|marking(BeginLoop_1_1_1)|+|marking(BeginLoop_1_5_1)|+|marking(BeginLoop_6_0_0)|+|marking(BeginLoop_3_5_1)|+|marking(BeginLoop_2_5_2)|+|marking(BeginLoop_4_1_5)|+|marking(BeginLoop_4_3_1)|+|marking(BeginLoop_5_0_3)|+|marking(BeginLoop_1_3_5)|+|marking(BeginLoop_3_1_1)|+|marking(BeginLoop_5_4_2)|+|marking(BeginLoop_1_1_5)|+|marking(BeginLoop_3_5_5)|+|marking(BeginLoop_1_2_3)|+|marking(BeginLoop_1_0_0)|+|marking(BeginLoop_0_3_0)|+|marking(BeginLoop_0_3_2)|+|marking(BeginLoop_5_3_2)|+|marking(BeginLoop_6_3_3)|+|marking(BeginLoop_3_3_2)|+|marking(BeginLoop_2_3_5)|+|marking(BeginLoop_0_2_5)|+|marking(BeginLoop_2_1_1)|+|marking(BeginLoop_5_3_3)|+|marking(BeginLoop_5_5_6)|+|marking(BeginLoop_3_3_0)|+|marking(BeginLoop_0_2_2)|+|marking(BeginLoop_5_2_2)|+|marking(BeginLoop_0_5_6)|+|marking(BeginLoop_4_2_4)|+|marking(BeginLoop_5_4_4)|+|marking(BeginLoop_1_5_3)|+|marking(BeginLoop_3_1_3)|+|marking(BeginLoop_5_0_5)|+|marking(BeginLoop_4_0_6)|+|marking(BeginLoop_2_2_1)|+|marking(BeginLoop_5_5_0)|+|marking(BeginLoop_4_1_1)|+|marking(BeginLoop_3_0_5)|+|marking(BeginLoop_4_5_1)|+|marking(BeginLoop_0_4_4)|+|marking(BeginLoop_0_2_1)|+|marking(BeginLoop_6_2_3)|+|marking(BeginLoop_3_3_5)|+|marking(BeginLoop_2_5_0)|+|marking(BeginLoop_3_0_1)|+|marking(BeginLoop_2_4_0)|+|marking(BeginLoop_6_2_4)|+|marking(BeginLoop_1_4_1)|+|marking(BeginLoop_6_3_1)|+|marking(BeginLoop_6_2_6)|+|marking(BeginLoop_3_0_6)|+|marking(BeginLoop_5_1_1)|+|marking(BeginLoop_0_3_5)|+|marking(BeginLoop_4_0_3)|+|marking(BeginLoop_2_2_2)|+|marking(BeginLoop_5_3_0)|+|marking(BeginLoop_3_4_0)|+|marking(BeginLoop_4_4_1)|+|marking(BeginLoop_2_1_2)|+|marking(BeginLoop_0_0_1)|+|marking(BeginLoop_3_0_2)|+|marking(BeginLoop_5_2_6)|+|marking(BeginLoop_2_3_0)|+|marking(BeginLoop_4_4_3)|+|marking(BeginLoop_5_1_5)|+|marking(BeginLoop_4_5_3)|+|marking(BeginLoop_4_0_4)|+|marking(BeginLoop_4_0_0)|+|marking(BeginLoop_6_5_0)|+|marking(BeginLoop_4_0_2)|+|marking(BeginLoop_0_2_0)|+|marking(BeginLoop_3_0_3)|+|marking(BeginLoop_4_1_2)|+|marking(BeginLoop_4_1_6)|+|marking(BeginLoop_5_1_2)|+|marking(BeginLoop_3_0_4)|+|marking(BeginLoop_4_3_6)|+|marking(BeginLoop_5_4_3)|+|marking(BeginLoop_1_5_5)|+|marking(BeginLoop_1_3_0)|+|marking(BeginLoop_0_1_4)|+|marking(BeginLoop_1_4_5)|+|marking(BeginLoop_1_4_3)|+|marking(BeginLoop_0_2_3)|+|marking(BeginLoop_0_5_3)|+|marking(BeginLoop_5_3_5)|+|marking(BeginLoop_3_3_1)|+|marking(BeginLoop_1_4_4)|+|marking(BeginLoop_1_5_0)|+|marking(BeginLoop_2_5_6)|+|marking(BeginLoop_6_4_6)|+|marking(BeginLoop_0_4_5)|+|marking(BeginLoop_5_0_2)|+|marking(BeginLoop_0_1_2)|+|marking(BeginLoop_1_3_6)|+|marking(BeginLoop_0_1_1)|+|marking(BeginLoop_5_0_6)|+|marking(BeginLoop_0_0_2)|+|marking(BeginLoop_6_3_4)|+|marking(BeginLoop_0_3_3)|+|marking(BeginLoop_3_2_5)|+|marking(BeginLoop_1_1_6)|+|marking(BeginLoop_2_1_6)|+|marking(BeginLoop_2_5_5)|+|marking(BeginLoop_4_5_2)|+|marking(BeginLoop_1_5_2)|+|marking(BeginLoop_5_5_3)|+|marking(BeginLoop_5_5_2)|+|marking(BeginLoop_0_3_4)|+|marking(BeginLoop_2_4_6)|+|marking(BeginLoop_6_3_0)|+|marking(BeginLoop_1_0_6)|+|marking(BeginLoop_1_5_6)|+|marking(BeginLoop_2_0_4)|+|marking(BeginLoop_6_5_5)|+|marking(BeginLoop_5_2_0)|+|marking(BeginLoop_0_5_5)|+|marking(BeginLoop_6_5_3)|+|marking(BeginLoop_4_3_0)|+|marking(BeginLoop_5_3_4)|+|marking(BeginLoop_3_1_6)|+|marking(BeginLoop_3_1_5)|+|marking(BeginLoop_5_0_0)|+|marking(BeginLoop_6_0_2)|+|marking(BeginLoop_4_4_2)|+|marking(BeginLoop_1_0_3)|+|marking(BeginLoop_5_1_3)|+|marking(BeginLoop_6_3_6)|+|marking(BeginLoop_2_5_4)|+|marking(BeginLoop_4_4_0)|+|marking(BeginLoop_5_2_4)|+|marking(BeginLoop_6_1_0)|+|marking(BeginLoop_4_0_5)|+|marking(BeginLoop_5_2_1)|+|marking(BeginLoop_0_2_6)|+|marking(BeginLoop_4_0_1)|+|marking(BeginLoop_0_0_5)|+|marking(BeginLoop_6_4_4)|+|marking(BeginLoop_5_4_0)|+|marking(BeginLoop_1_5_4)|+|marking(BeginLoop_4_5_5)|+|marking(BeginLoop_1_1_3)|+|marking(BeginLoop_2_0_0)|+|marking(BeginLoop_5_3_6)|+|marking(BeginLoop_6_2_5)|+|marking(BeginLoop_5_5_4)|+|marking(BeginLoop_1_3_2)|+|marking(BeginLoop_3_1_2)|+|marking(BeginLoop_4_5_0)|+|marking(BeginLoop_3_0_0)|+|marking(BeginLoop_2_3_4)|+|marking(BeginLoop_6_4_5)|+|marking(BeginLoop_1_1_2)|+|marking(BeginLoop_1_1_0)|+|marking(BeginLoop_0_1_5)|+|marking(BeginLoop_1_2_6)|+|marking(BeginLoop_0_3_1)|+|marking(BeginLoop_2_5_1)|+|marking(BeginLoop_1_0_2)|+|marking(BeginLoop_2_4_5)|+|marking(BeginLoop_6_1_3)|+|marking(BeginLoop_2_0_3)|+|marking(BeginLoop_5_5_1)|+|marking(BeginLoop_3_3_3)|+|marking(BeginLoop_3_5_4)|+|marking(BeginLoop_2_3_6)|+|marking(BeginLoop_2_4_2)|+|marking(BeginLoop_5_2_3)|+|marking(BeginLoop_6_2_0)|+|marking(BeginLoop_3_3_4)|+|marking(BeginLoop_1_2_2)|+|marking(BeginLoop_5_2_5)|+|marking(BeginLoop_2_4_4)|+|marking(BeginLoop_2_1_4)|+|marking(BeginLoop_2_1_0)|+|marking(BeginLoop_4_1_4)|+|marking(BeginLoop_4_5_6)|+|marking(BeginLoop_5_1_6)|+|marking(BeginLoop_1_4_2)|+|marking(BeginLoop_6_0_5)|+|marking(BeginLoop_3_2_6)|+|marking(BeginLoop_0_0_4)|+|marking(BeginLoop_1_1_4)|+|marking(BeginLoop_3_4_2)|+|marking(BeginLoop_2_5_3)|+|marking(BeginLoop_2_0_1)|+|marking(BeginLoop_6_1_1)|+|marking(BeginLoop_3_5_0)|+|marking(BeginLoop_3_5_6)|+|marking(BeginLoop_3_2_2)|+|marking(BeginLoop_4_5_4)|+|marking(BeginLoop_5_3_1)|+|marking(BeginLoop_2_2_3)|+|marking(BeginLoop_2_3_1)|+|marking(BeginLoop_6_0_3)|+|marking(BeginLoop_1_2_5)|+|marking(BeginLoop_1_4_6)|+|marking(BeginLoop_1_0_1)|+|marking(BeginLoop_4_2_1)|+|marking(BeginLoop_3_2_3)|+|marking(BeginLoop_1_2_0)|+|marking(BeginLoop_6_1_5)|+|marking(BeginLoop_1_3_4)|+|marking(BeginLoop_1_3_1)|+|marking(BeginLoop_5_4_1)|+|marking(BeginLoop_3_1_4)|+|marking(BeginLoop_4_1_3)|+|marking(BeginLoop_5_0_1)|+|marking(BeginLoop_2_0_6)|+|marking(BeginLoop_2_0_2)|+|marking(BeginLoop_0_4_1)|+|marking(BeginLoop_6_4_1)|+|marking(BeginLoop_6_0_4)|+|marking(BeginLoop_0_0_0)|+|marking(BeginLoop_6_4_2)|+|marking(BeginLoop_5_4_5)|+|marking(BeginLoop_4_2_5)|+|marking(BeginLoop_2_1_3)|+|marking(BeginLoop_0_4_3)|+|marking(BeginLoop_2_4_3)|+|marking(BeginLoop_6_1_4)|+|marking(BeginLoop_5_1_4)|+|marking(BeginLoop_4_4_5)|+|marking(BeginLoop_4_3_5)|+|marking(BeginLoop_0_2_4)|+|marking(BeginLoop_6_1_6)|+|marking(BeginLoop_3_2_0)|+|marking(BeginLoop_3_4_5)|+|marking(BeginLoop_6_1_2)|+|marking(BeginLoop_6_3_5)|+|marking(BeginLoop_3_4_6)|+|marking(BeginLoop_2_2_4)|+|marking(BeginLoop_3_2_4)|+|marking(BeginLoop_4_2_0)|)))
ctl p_1863_cardinalitycomparison_full_and_notx: E G (!((|marking(AskForSection_1_4)|+|marking(AskForSection_1_5)|+|marking(AskForSection_6_0)|+|marking(AskForSection_3_2)|+|marking(AskForSection_2_1)|+|marking(AskForSection_6_4)|+|marking(AskForSection_0_2)|+|marking(AskForSection_3_0)|+|marking(AskForSection_2_5)|+|marking(AskForSection_6_1)|+|marking(AskForSection_2_0)|+|marking(AskForSection_4_1)|+|marking(AskForSection_0_0)|+|marking(AskForSection_2_3)|+|marking(AskForSection_6_2)|+|marking(AskForSection_4_4)|+|marking(AskForSection_6_3)|+|marking(AskForSection_4_3)|+|marking(AskForSection_0_5)|+|marking(AskForSection_3_5)|+|marking(AskForSection_5_4)|+|marking(AskForSection_5_5)|+|marking(AskForSection_4_2)|+|marking(AskForSection_5_0)|+|marking(AskForSection_5_3)|+|marking(AskForSection_2_4)|+|marking(AskForSection_5_1)|+|marking(AskForSection_0_3)|+|marking(AskForSection_5_2)|+|marking(AskForSection_1_2)|+|marking(AskForSection_4_5)|+|marking(AskForSection_3_3)|+|marking(AskForSection_0_1)|+|marking(AskForSection_1_0)|+|marking(AskForSection_1_3)|+|marking(AskForSection_4_0)|+|marking(AskForSection_3_4)|+|marking(AskForSection_3_1)|+|marking(AskForSection_1_1)|+|marking(AskForSection_2_2)|+|marking(AskForSection_6_5)|+|marking(AskForSection_0_4)|)!=(|marking(TestTurn_3_3)|+|marking(TestTurn_3_0)|+|marking(TestTurn_6_4)|+|marking(TestTurn_1_4)|+|marking(TestTurn_4_1)|+|marking(TestTurn_4_5)|+|marking(TestTurn_6_3)|+|marking(TestTurn_2_2)|+|marking(TestTurn_3_1)|+|marking(TestTurn_4_0)|+|marking(TestTurn_0_4)|+|marking(TestTurn_2_3)|+|marking(TestTurn_0_0)|+|marking(TestTurn_3_4)|+|marking(TestTurn_4_3)|+|marking(TestTurn_1_2)|+|marking(TestTurn_2_5)|+|marking(TestTurn_6_2)|+|marking(TestTurn_0_3)|+|marking(TestTurn_5_0)|+|marking(TestTurn_1_5)|+|marking(TestTurn_0_5)|+|marking(TestTurn_2_4)|+|marking(TestTurn_5_4)|+|marking(TestTurn_5_3)|+|marking(TestTurn_2_0)|+|marking(TestTurn_0_2)|+|marking(TestTurn_1_1)|+|marking(TestTurn_5_1)|+|marking(TestTurn_5_5)|+|marking(TestTurn_2_1)|+|marking(TestTurn_6_0)|+|marking(TestTurn_1_3)|+|marking(TestTurn_5_2)|+|marking(TestTurn_1_0)|+|marking(TestTurn_3_5)|+|marking(TestTurn_4_2)|+|marking(TestTurn_3_2)|+|marking(TestTurn_4_4)|+|marking(TestTurn_0_1)|+|marking(TestTurn_6_5)|+|marking(TestTurn_6_1)|)) & !((|marking(TestIdentity_2_2_0)|+|marking(TestIdentity_6_0_4)|+|marking(TestIdentity_3_4_3)|+|marking(TestIdentity_0_4_3)|+|marking(TestIdentity_1_2_0)|+|marking(TestIdentity_6_4_1)|+|marking(TestIdentity_2_3_6)|+|marking(TestIdentity_5_4_1)|+|marking(TestIdentity_2_5_4)|+|marking(TestIdentity_3_4_2)|+|marking(TestIdentity_5_3_6)|+|marking(TestIdentity_2_2_5)|+|marking(TestIdentity_1_0_6)|+|marking(TestIdentity_5_4_5)|+|marking(TestIdentity_4_0_5)|+|marking(TestIdentity_1_2_2)|+|marking(TestIdentity_5_5_5)|+|marking(TestIdentity_2_4_6)|+|marking(TestIdentity_6_1_5)|+|marking(TestIdentity_1_4_1)|+|marking(TestIdentity_0_1_5)|+|marking(TestIdentity_6_3_5)|+|marking(TestIdentity_3_0_3)|+|marking(TestIdentity_0_3_2)|+|marking(TestIdentity_6_1_1)|+|marking(TestIdentity_2_3_2)|+|marking(TestIdentity_1_5_1)|+|marking(TestIdentity_0_4_5)|+|marking(TestIdentity_4_3_5)|+|marking(TestIdentity_4_3_6)|+|marking(TestIdentity_6_2_6)|+|marking(TestIdentity_1_4_5)|+|marking(TestIdentity_6_4_3)|+|marking(TestIdentity_5_1_3)|+|marking(TestIdentity_6_0_5)|+|marking(TestIdentity_4_0_0)|+|marking(TestIdentity_3_3_6)|+|marking(TestIdentity_2_2_2)|+|marking(TestIdentity_2_0_3)|+|marking(TestIdentity_0_3_3)|+|marking(TestIdentity_1_2_3)|+|marking(TestIdentity_3_2_3)|+|marking(TestIdentity_1_1_1)|+|marking(TestIdentity_3_2_1)|+|marking(TestIdentity_5_3_1)|+|marking(TestIdentity_2_4_3)|+|marking(TestIdentity_2_5_3)|+|marking(TestIdentity_2_0_4)|+|marking(TestIdentity_2_4_5)|+|marking(TestIdentity_6_2_3)|+|marking(TestIdentity_6_0_3)|+|marking(TestIdentity_6_5_0)|+|marking(TestIdentity_6_2_2)|+|marking(TestIdentity_6_3_6)|+|marking(TestIdentity_5_1_1)|+|marking(TestIdentity_4_0_3)|+|marking(TestIdentity_6_5_5)|+|marking(TestIdentity_5_0_5)|+|marking(TestIdentity_4_3_0)|+|marking(TestIdentity_0_3_5)|+|marking(TestIdentity_5_0_1)|+|marking(TestIdentity_3_3_0)|+|marking(TestIdentity_3_3_2)|+|marking(TestIdentity_4_1_1)|+|marking(TestIdentity_6_5_2)|+|marking(TestIdentity_1_3_4)|+|marking(TestIdentity_2_0_1)|+|marking(TestIdentity_5_5_6)|+|marking(TestIdentity_6_1_6)|+|marking(TestIdentity_4_5_2)|+|marking(TestIdentity_2_0_5)|+|marking(TestIdentity_1_2_5)|+|marking(TestIdentity_1_4_3)|+|marking(TestIdentity_4_0_1)|+|marking(TestIdentity_6_1_2)|+|marking(TestIdentity_3_5_1)|+|marking(TestIdentity_1_5_6)|+|marking(TestIdentity_0_0_1)|+|marking(TestIdentity_4_0_6)|+|marking(TestIdentity_3_5_6)|+|marking(TestIdentity_5_5_2)|+|marking(TestIdentity_2_4_1)|+|marking(TestIdentity_5_2_1)|+|marking(TestIdentity_0_2_6)|+|marking(TestIdentity_2_5_0)|+|marking(TestIdentity_2_4_4)|+|marking(TestIdentity_3_2_4)|+|marking(TestIdentity_1_5_5)|+|marking(TestIdentity_1_0_4)|+|marking(TestIdentity_5_3_4)|+|marking(TestIdentity_0_2_5)|+|marking(TestIdentity_1_2_1)|+|marking(TestIdentity_0_1_2)|+|marking(TestIdentity_0_2_4)|+|marking(TestIdentity_3_5_3)|+|marking(TestIdentity_3_5_4)|+|marking(TestIdentity_4_1_0)|+|marking(TestIdentity_5_4_2)|+|marking(TestIdentity_4_3_1)|+|marking(TestIdentity_1_3_6)|+|marking(TestIdentity_2_3_0)|+|marking(TestIdentity_0_4_4)|+|marking(TestIdentity_0_1_0)|+|marking(TestIdentity_0_5_5)|+|marking(TestIdentity_3_3_5)|+|marking(TestIdentity_0_4_2)|+|marking(TestIdentity_6_3_0)|+|marking(TestIdentity_3_3_1)|+|marking(TestIdentity_5_5_3)|+|marking(TestIdentity_0_4_6)|+|marking(TestIdentity_5_3_3)|+|marking(TestIdentity_0_1_3)|+|marking(TestIdentity_5_2_5)|+|marking(TestIdentity_5_2_4)|+|marking(TestIdentity_3_4_6)|+|marking(TestIdentity_3_4_4)|+|marking(TestIdentity_6_1_4)|+|marking(TestIdentity_3_4_5)|+|marking(TestIdentity_5_1_6)|+|marking(TestIdentity_1_1_0)|+|marking(TestIdentity_4_4_0)|+|marking(TestIdentity_6_0_0)|+|marking(TestIdentity_0_5_0)|+|marking(TestIdentity_3_4_1)|+|marking(TestIdentity_1_5_2)|+|marking(TestIdentity_6_2_4)|+|marking(TestIdentity_4_4_5)|+|marking(TestIdentity_0_1_4)|+|marking(TestIdentity_1_1_5)|+|marking(TestIdentity_1_0_3)|+|marking(TestIdentity_6_4_0)|+|marking(TestIdentity_3_0_1)|+|marking(TestIdentity_5_5_1)|+|marking(TestIdentity_5_1_0)|+|marking(TestIdentity_4_5_5)|+|marking(TestIdentity_4_1_2)|+|marking(TestIdentity_5_3_5)|+|marking(TestIdentity_3_1_3)|+|marking(TestIdentity_3_0_0)|+|marking(TestIdentity_6_0_2)|+|marking(TestIdentity_6_0_6)|+|marking(TestIdentity_3_2_5)|+|marking(TestIdentity_5_1_5)|+|marking(TestIdentity_1_1_4)|+|marking(TestIdentity_3_1_5)|+|marking(TestIdentity_3_0_4)|+|marking(TestIdentity_3_5_0)|+|marking(TestIdentity_3_0_2)|+|marking(TestIdentity_1_4_4)|+|marking(TestIdentity_3_3_3)|+|marking(TestIdentity_0_0_0)|+|marking(TestIdentity_2_1_3)|+|marking(TestIdentity_2_0_6)|+|marking(TestIdentity_0_5_3)|+|marking(TestIdentity_1_3_2)|+|marking(TestIdentity_2_2_6)|+|marking(TestIdentity_5_0_6)|+|marking(TestIdentity_0_4_1)|+|marking(TestIdentity_1_5_0)|+|marking(TestIdentity_4_4_1)|+|marking(TestIdentity_6_2_1)|+|marking(TestIdentity_5_3_2)|+|marking(TestIdentity_1_3_1)|+|marking(TestIdentity_0_5_4)|+|marking(TestIdentity_2_3_3)|+|marking(TestIdentity_5_1_2)|+|marking(TestIdentity_2_1_1)|+|marking(TestIdentity_3_1_6)|+|marking(TestIdentity_2_2_4)|+|marking(TestIdentity_4_1_4)|+|marking(TestIdentity_0_1_6)|+|marking(TestIdentity_1_4_0)|+|marking(TestIdentity_0_3_6)|+|marking(TestIdentity_5_4_3)|+|marking(TestIdentity_1_0_0)|+|marking(TestIdentity_4_5_0)|+|marking(TestIdentity_5_2_0)|+|marking(TestIdentity_0_0_5)|+|marking(TestIdentity_1_5_4)|+|marking(TestIdentity_5_4_6)|+|marking(TestIdentity_5_4_4)|+|marking(TestIdentity_1_1_2)|+|marking(TestIdentity_2_4_0)|+|marking(TestIdentity_0_2_0)|+|marking(TestIdentity_6_3_3)|+|marking(TestIdentity_3_2_6)|+|marking(TestIdentity_5_0_3)|+|marking(TestIdentity_4_4_2)|+|marking(TestIdentity_2_2_3)|+|marking(TestIdentity_1_0_5)|+|marking(TestIdentity_3_1_1)|+|marking(TestIdentity_5_2_6)|+|marking(TestIdentity_1_2_4)|+|marking(TestIdentity_2_5_6)|+|marking(TestIdentity_1_3_5)|+|marking(TestIdentity_1_2_6)|+|marking(TestIdentity_4_2_6)|+|marking(TestIdentity_5_0_2)|+|marking(TestIdentity_6_5_1)|+|marking(TestIdentity_2_3_4)|+|marking(TestIdentity_2_5_5)|+|marking(TestIdentity_2_0_0)|+|marking(TestIdentity_4_3_2)|+|marking(TestIdentity_2_5_1)|+|marking(TestIdentity_2_0_2)|+|marking(TestIdentity_4_2_5)|+|marking(TestIdentity_2_4_2)|+|marking(TestIdentity_0_2_2)|+|marking(TestIdentity_0_1_1)|+|marking(TestIdentity_1_1_3)|+|marking(TestIdentity_0_0_3)|+|marking(TestIdentity_2_3_1)|+|marking(TestIdentity_4_0_2)|+|marking(TestIdentity_6_5_3)|+|marking(TestIdentity_1_1_6)|+|marking(TestIdentity_3_1_0)|+|marking(TestIdentity_5_1_4)|+|marking(TestIdentity_4_2_0)|+|marking(TestIdentity_4_5_6)|+|marking(TestIdentity_5_3_0)|+|marking(TestIdentity_0_4_0)|+|marking(TestIdentity_4_1_3)|+|marking(TestIdentity_6_4_6)|+|marking(TestIdentity_6_4_5)|+|marking(TestIdentity_5_2_2)|+|marking(TestIdentity_6_3_1)|+|marking(TestIdentity_4_2_4)|+|marking(TestIdentity_2_1_0)|+|marking(TestIdentity_3_0_5)|+|marking(TestIdentity_4_4_6)|+|marking(TestIdentity_5_5_0)|+|marking(TestIdentity_6_1_0)|+|marking(TestIdentity_0_5_1)|+|marking(TestIdentity_2_1_5)|+|marking(TestIdentity_0_5_6)|+|marking(TestIdentity_2_5_2)|+|marking(TestIdentity_0_2_3)|+|marking(TestIdentity_2_1_6)|+|marking(TestIdentity_1_0_1)|+|marking(TestIdentity_3_2_2)|+|marking(TestIdentity_3_1_4)|+|marking(TestIdentity_3_1_2)|+|marking(TestIdentity_6_0_1)|+|marking(TestIdentity_6_5_6)|+|marking(TestIdentity_6_2_0)|+|marking(TestIdentity_4_1_5)|+|marking(TestIdentity_0_3_0)|+|marking(TestIdentity_6_1_3)|+|marking(TestIdentity_5_5_4)|+|marking(TestIdentity_0_3_1)|+|marking(TestIdentity_2_2_1)|+|marking(TestIdentity_4_5_4)|+|marking(TestIdentity_0_5_2)|+|marking(TestIdentity_2_3_5)|+|marking(TestIdentity_6_2_5)|+|marking(TestIdentity_4_1_6)|+|marking(TestIdentity_0_2_1)|+|marking(TestIdentity_4_2_3)|+|marking(TestIdentity_6_5_4)|+|marking(TestIdentity_6_4_4)|+|marking(TestIdentity_6_4_2)|+|marking(TestIdentity_2_1_4)|+|marking(TestIdentity_3_3_4)|+|marking(TestIdentity_4_3_3)|+|marking(TestIdentity_0_0_6)|+|marking(TestIdentity_3_5_2)|+|marking(TestIdentity_1_0_2)|+|marking(TestIdentity_4_5_1)|+|marking(TestIdentity_4_2_1)|+|marking(TestIdentity_0_0_4)|+|marking(TestIdentity_4_3_4)|+|marking(TestIdentity_3_4_0)|+|marking(TestIdentity_5_4_0)|+|marking(TestIdentity_1_3_0)|+|marking(TestIdentity_4_2_2)|+|marking(TestIdentity_5_0_0)|+|marking(TestIdentity_3_0_6)|+|marking(TestIdentity_5_0_4)|+|marking(TestIdentity_4_4_3)|+|marking(TestIdentity_0_3_4)|+|marking(TestIdentity_1_5_3)|+|marking(TestIdentity_4_4_4)|+|marking(TestIdentity_6_3_4)|+|marking(TestIdentity_1_4_6)|+|marking(TestIdentity_6_3_2)|+|marking(TestIdentity_5_2_3)|+|marking(TestIdentity_0_0_2)|+|marking(TestIdentity_4_0_4)|+|marking(TestIdentity_3_2_0)|+|marking(TestIdentity_1_4_2)|+|marking(TestIdentity_4_5_3)|+|marking(TestIdentity_2_1_2)|+|marking(TestIdentity_1_3_3)|+|marking(TestIdentity_3_5_5)|)<=(|marking(BeginLoop_6_0_6)|+|marking(BeginLoop_2_2_0)|+|marking(BeginLoop_0_4_6)|+|marking(BeginLoop_6_2_1)|+|marking(BeginLoop_3_1_0)|+|marking(BeginLoop_0_5_4)|+|marking(BeginLoop_0_0_6)|+|marking(BeginLoop_4_2_2)|+|marking(BeginLoop_6_5_6)|+|marking(BeginLoop_6_2_2)|+|marking(BeginLoop_2_2_6)|+|marking(BeginLoop_2_4_1)|+|marking(BeginLoop_4_3_3)|+|marking(BeginLoop_4_4_6)|+|marking(BeginLoop_0_5_2)|+|marking(BeginLoop_4_4_4)|+|marking(BeginLoop_0_0_3)|+|marking(BeginLoop_1_3_3)|+|marking(BeginLoop_6_5_4)|+|marking(BeginLoop_2_3_3)|+|marking(BeginLoop_0_3_6)|+|marking(BeginLoop_1_2_4)|+|marking(BeginLoop_1_0_5)|+|marking(BeginLoop_6_5_2)|+|marking(BeginLoop_5_5_5)|+|marking(BeginLoop_2_0_5)|+|marking(BeginLoop_6_0_1)|+|marking(BeginLoop_3_4_1)|+|marking(BeginLoop_1_0_4)|+|marking(BeginLoop_2_1_5)|+|marking(BeginLoop_5_0_4)|+|marking(BeginLoop_0_5_0)|+|marking(BeginLoop_0_1_0)|+|marking(BeginLoop_3_5_3)|+|marking(BeginLoop_0_4_0)|+|marking(BeginLoop_4_2_3)|+|marking(BeginLoop_4_3_4)|+|marking(BeginLoop_3_4_3)|+|marking(BeginLoop_4_2_6)|+|marking(BeginLoop_4_3_2)|+|marking(BeginLoop_1_2_1)|+|marking(BeginLoop_0_4_2)|+|marking(BeginLoop_0_1_3)|+|marking(BeginLoop_1_4_0)|+|marking(BeginLoop_0_1_6)|+|marking(BeginLoop_6_3_2)|+|marking(BeginLoop_6_4_0)|+|marking(BeginLoop_3_3_6)|+|marking(BeginLoop_6_5_1)|+|marking(BeginLoop_4_1_0)|+|marking(BeginLoop_5_1_0)|+|marking(BeginLoop_2_3_2)|+|marking(BeginLoop_3_4_4)|+|marking(BeginLoop_5_4_6)|+|marking(BeginLoop_0_5_1)|+|marking(BeginLoop_2_2_5)|+|marking(BeginLoop_3_5_2)|+|marking(BeginLoop_3_2_1)|+|marking(BeginLoop_6_4_3)|+|marking(BeginLoop_1_1_1)|+|marking(BeginLoop_1_5_1)|+|marking(BeginLoop_6_0_0)|+|marking(BeginLoop_3_5_1)|+|marking(BeginLoop_2_5_2)|+|marking(BeginLoop_4_1_5)|+|marking(BeginLoop_4_3_1)|+|marking(BeginLoop_5_0_3)|+|marking(BeginLoop_1_3_5)|+|marking(BeginLoop_3_1_1)|+|marking(BeginLoop_5_4_2)|+|marking(BeginLoop_1_1_5)|+|marking(BeginLoop_3_5_5)|+|marking(BeginLoop_1_2_3)|+|marking(BeginLoop_1_0_0)|+|marking(BeginLoop_0_3_0)|+|marking(BeginLoop_0_3_2)|+|marking(BeginLoop_5_3_2)|+|marking(BeginLoop_6_3_3)|+|marking(BeginLoop_3_3_2)|+|marking(BeginLoop_2_3_5)|+|marking(BeginLoop_0_2_5)|+|marking(BeginLoop_2_1_1)|+|marking(BeginLoop_5_3_3)|+|marking(BeginLoop_5_5_6)|+|marking(BeginLoop_3_3_0)|+|marking(BeginLoop_0_2_2)|+|marking(BeginLoop_5_2_2)|+|marking(BeginLoop_0_5_6)|+|marking(BeginLoop_4_2_4)|+|marking(BeginLoop_5_4_4)|+|marking(BeginLoop_1_5_3)|+|marking(BeginLoop_3_1_3)|+|marking(BeginLoop_5_0_5)|+|marking(BeginLoop_4_0_6)|+|marking(BeginLoop_2_2_1)|+|marking(BeginLoop_5_5_0)|+|marking(BeginLoop_4_1_1)|+|marking(BeginLoop_3_0_5)|+|marking(BeginLoop_4_5_1)|+|marking(BeginLoop_0_4_4)|+|marking(BeginLoop_0_2_1)|+|marking(BeginLoop_6_2_3)|+|marking(BeginLoop_3_3_5)|+|marking(BeginLoop_2_5_0)|+|marking(BeginLoop_3_0_1)|+|marking(BeginLoop_2_4_0)|+|marking(BeginLoop_6_2_4)|+|marking(BeginLoop_1_4_1)|+|marking(BeginLoop_6_3_1)|+|marking(BeginLoop_6_2_6)|+|marking(BeginLoop_3_0_6)|+|marking(BeginLoop_5_1_1)|+|marking(BeginLoop_0_3_5)|+|marking(BeginLoop_4_0_3)|+|marking(BeginLoop_2_2_2)|+|marking(BeginLoop_5_3_0)|+|marking(BeginLoop_3_4_0)|+|marking(BeginLoop_4_4_1)|+|marking(BeginLoop_2_1_2)|+|marking(BeginLoop_0_0_1)|+|marking(BeginLoop_3_0_2)|+|marking(BeginLoop_5_2_6)|+|marking(BeginLoop_2_3_0)|+|marking(BeginLoop_4_4_3)|+|marking(BeginLoop_5_1_5)|+|marking(BeginLoop_4_5_3)|+|marking(BeginLoop_4_0_4)|+|marking(BeginLoop_4_0_0)|+|marking(BeginLoop_6_5_0)|+|marking(BeginLoop_4_0_2)|+|marking(BeginLoop_0_2_0)|+|marking(BeginLoop_3_0_3)|+|marking(BeginLoop_4_1_2)|+|marking(BeginLoop_4_1_6)|+|marking(BeginLoop_5_1_2)|+|marking(BeginLoop_3_0_4)|+|marking(BeginLoop_4_3_6)|+|marking(BeginLoop_5_4_3)|+|marking(BeginLoop_1_5_5)|+|marking(BeginLoop_1_3_0)|+|marking(BeginLoop_0_1_4)|+|marking(BeginLoop_1_4_5)|+|marking(BeginLoop_1_4_3)|+|marking(BeginLoop_0_2_3)|+|marking(BeginLoop_0_5_3)|+|marking(BeginLoop_5_3_5)|+|marking(BeginLoop_3_3_1)|+|marking(BeginLoop_1_4_4)|+|marking(BeginLoop_1_5_0)|+|marking(BeginLoop_2_5_6)|+|marking(BeginLoop_6_4_6)|+|marking(BeginLoop_0_4_5)|+|marking(BeginLoop_5_0_2)|+|marking(BeginLoop_0_1_2)|+|marking(BeginLoop_1_3_6)|+|marking(BeginLoop_0_1_1)|+|marking(BeginLoop_5_0_6)|+|marking(BeginLoop_0_0_2)|+|marking(BeginLoop_6_3_4)|+|marking(BeginLoop_0_3_3)|+|marking(BeginLoop_3_2_5)|+|marking(BeginLoop_1_1_6)|+|marking(BeginLoop_2_1_6)|+|marking(BeginLoop_2_5_5)|+|marking(BeginLoop_4_5_2)|+|marking(BeginLoop_1_5_2)|+|marking(BeginLoop_5_5_3)|+|marking(BeginLoop_5_5_2)|+|marking(BeginLoop_0_3_4)|+|marking(BeginLoop_2_4_6)|+|marking(BeginLoop_6_3_0)|+|marking(BeginLoop_1_0_6)|+|marking(BeginLoop_1_5_6)|+|marking(BeginLoop_2_0_4)|+|marking(BeginLoop_6_5_5)|+|marking(BeginLoop_5_2_0)|+|marking(BeginLoop_0_5_5)|+|marking(BeginLoop_6_5_3)|+|marking(BeginLoop_4_3_0)|+|marking(BeginLoop_5_3_4)|+|marking(BeginLoop_3_1_6)|+|marking(BeginLoop_3_1_5)|+|marking(BeginLoop_5_0_0)|+|marking(BeginLoop_6_0_2)|+|marking(BeginLoop_4_4_2)|+|marking(BeginLoop_1_0_3)|+|marking(BeginLoop_5_1_3)|+|marking(BeginLoop_6_3_6)|+|marking(BeginLoop_2_5_4)|+|marking(BeginLoop_4_4_0)|+|marking(BeginLoop_5_2_4)|+|marking(BeginLoop_6_1_0)|+|marking(BeginLoop_4_0_5)|+|marking(BeginLoop_5_2_1)|+|marking(BeginLoop_0_2_6)|+|marking(BeginLoop_4_0_1)|+|marking(BeginLoop_0_0_5)|+|marking(BeginLoop_6_4_4)|+|marking(BeginLoop_5_4_0)|+|marking(BeginLoop_1_5_4)|+|marking(BeginLoop_4_5_5)|+|marking(BeginLoop_1_1_3)|+|marking(BeginLoop_2_0_0)|+|marking(BeginLoop_5_3_6)|+|marking(BeginLoop_6_2_5)|+|marking(BeginLoop_5_5_4)|+|marking(BeginLoop_1_3_2)|+|marking(BeginLoop_3_1_2)|+|marking(BeginLoop_4_5_0)|+|marking(BeginLoop_3_0_0)|+|marking(BeginLoop_2_3_4)|+|marking(BeginLoop_6_4_5)|+|marking(BeginLoop_1_1_2)|+|marking(BeginLoop_1_1_0)|+|marking(BeginLoop_0_1_5)|+|marking(BeginLoop_1_2_6)|+|marking(BeginLoop_0_3_1)|+|marking(BeginLoop_2_5_1)|+|marking(BeginLoop_1_0_2)|+|marking(BeginLoop_2_4_5)|+|marking(BeginLoop_6_1_3)|+|marking(BeginLoop_2_0_3)|+|marking(BeginLoop_5_5_1)|+|marking(BeginLoop_3_3_3)|+|marking(BeginLoop_3_5_4)|+|marking(BeginLoop_2_3_6)|+|marking(BeginLoop_2_4_2)|+|marking(BeginLoop_5_2_3)|+|marking(BeginLoop_6_2_0)|+|marking(BeginLoop_3_3_4)|+|marking(BeginLoop_1_2_2)|+|marking(BeginLoop_5_2_5)|+|marking(BeginLoop_2_4_4)|+|marking(BeginLoop_2_1_4)|+|marking(BeginLoop_2_1_0)|+|marking(BeginLoop_4_1_4)|+|marking(BeginLoop_4_5_6)|+|marking(BeginLoop_5_1_6)|+|marking(BeginLoop_1_4_2)|+|marking(BeginLoop_6_0_5)|+|marking(BeginLoop_3_2_6)|+|marking(BeginLoop_0_0_4)|+|marking(BeginLoop_1_1_4)|+|marking(BeginLoop_3_4_2)|+|marking(BeginLoop_2_5_3)|+|marking(BeginLoop_2_0_1)|+|marking(BeginLoop_6_1_1)|+|marking(BeginLoop_3_5_0)|+|marking(BeginLoop_3_5_6)|+|marking(BeginLoop_3_2_2)|+|marking(BeginLoop_4_5_4)|+|marking(BeginLoop_5_3_1)|+|marking(BeginLoop_2_2_3)|+|marking(BeginLoop_2_3_1)|+|marking(BeginLoop_6_0_3)|+|marking(BeginLoop_1_2_5)|+|marking(BeginLoop_1_4_6)|+|marking(BeginLoop_1_0_1)|+|marking(BeginLoop_4_2_1)|+|marking(BeginLoop_3_2_3)|+|marking(BeginLoop_1_2_0)|+|marking(BeginLoop_6_1_5)|+|marking(BeginLoop_1_3_4)|+|marking(BeginLoop_1_3_1)|+|marking(BeginLoop_5_4_1)|+|marking(BeginLoop_3_1_4)|+|marking(BeginLoop_4_1_3)|+|marking(BeginLoop_5_0_1)|+|marking(BeginLoop_2_0_6)|+|marking(BeginLoop_2_0_2)|+|marking(BeginLoop_0_4_1)|+|marking(BeginLoop_6_4_1)|+|marking(BeginLoop_6_0_4)|+|marking(BeginLoop_0_0_0)|+|marking(BeginLoop_6_4_2)|+|marking(BeginLoop_5_4_5)|+|marking(BeginLoop_4_2_5)|+|marking(BeginLoop_2_1_3)|+|marking(BeginLoop_0_4_3)|+|marking(BeginLoop_2_4_3)|+|marking(BeginLoop_6_1_4)|+|marking(BeginLoop_5_1_4)|+|marking(BeginLoop_4_4_5)|+|marking(BeginLoop_4_3_5)|+|marking(BeginLoop_0_2_4)|+|marking(BeginLoop_6_1_6)|+|marking(BeginLoop_3_2_0)|+|marking(BeginLoop_3_4_5)|+|marking(BeginLoop_6_1_2)|+|marking(BeginLoop_6_3_5)|+|marking(BeginLoop_3_4_6)|+|marking(BeginLoop_2_2_4)|+|marking(BeginLoop_3_2_4)|+|marking(BeginLoop_4_2_0)|)))


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