Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

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

export BK_INPUT=SharedMemory-PT-000100
export BK_EXAMINATION=CTLCardinalityComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1651
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/SharedMemory-PT-000100
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is SharedMemory-PT-000100, examination is CTLCardinalityComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

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

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

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

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

START 1369868036

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: 10301 NrTr: 20100)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369868048

--------------------
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: A G E (E F ((|marking(Active_75)|+|marking(Active_60)|+|marking(Active_38)|+|marking(Active_84)|+|marking(Active_81)|+|marking(Active_4)|+|marking(Active_6)|+|marking(Active_68)|+|marking(Active_55)|+|marking(Active_74)|+|marking(Active_99)|+|marking(Active_33)|+|marking(Active_14)|+|marking(Active_26)|+|marking(Active_50)|+|marking(Active_21)|+|marking(Active_82)|+|marking(Active_91)|+|marking(Active_95)|+|marking(Active_28)|+|marking(Active_90)|+|marking(Active_98)|+|marking(Active_77)|+|marking(Active_83)|+|marking(Active_76)|+|marking(Active_29)|+|marking(Active_63)|+|marking(Active_19)|+|marking(Active_30)|+|marking(Active_51)|+|marking(Active_56)|+|marking(Active_17)|+|marking(Active_65)|+|marking(Active_45)|+|marking(Active_11)|+|marking(Active_13)|+|marking(Active_42)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_62)|+|marking(Active_12)|+|marking(Active_49)|+|marking(Active_53)|+|marking(Active_92)|+|marking(Active_79)|+|marking(Active_93)|+|marking(Active_20)|+|marking(Active_87)|+|marking(Active_85)|+|marking(Active_72)|+|marking(Active_67)|+|marking(Active_46)|+|marking(Active_59)|+|marking(Active_70)|+|marking(Active_25)|+|marking(Active_41)|+|marking(Active_97)|+|marking(Active_37)|+|marking(Active_73)|+|marking(Active_9)|+|marking(Active_96)|+|marking(Active_32)|+|marking(Active_52)|+|marking(Active_39)|+|marking(Active_5)|+|marking(Active_36)|+|marking(Active_15)|+|marking(Active_80)|+|marking(Active_23)|+|marking(Active_40)|+|marking(Active_71)|+|marking(Active_1)|+|marking(Active_86)|+|marking(Active_88)|+|marking(Active_18)|+|marking(Active_64)|+|marking(Active_3)|+|marking(Active_22)|+|marking(Active_43)|+|marking(Active_35)|+|marking(Active_44)|+|marking(Active_66)|+|marking(Active_31)|+|marking(Active_61)|+|marking(Active_89)|+|marking(Active_7)|+|marking(Active_16)|+|marking(Active_47)|+|marking(Active_54)|+|marking(Active_27)|+|marking(Active_24)|+|marking(Active_8)|+|marking(Active_100)|+|marking(Active_69)|+|marking(Active_58)|+|marking(Active_94)|+|marking(Active_78)|+|marking(Active_10)|+|marking(Active_48)|+|marking(Active_57)|)!=(|marking(Memory_55)|+|marking(Memory_80)|+|marking(Memory_89)|+|marking(Memory_22)|+|marking(Memory_77)|+|marking(Memory_62)|+|marking(Memory_68)|+|marking(Memory_2)|+|marking(Memory_65)|+|marking(Memory_40)|+|marking(Memory_91)|+|marking(Memory_83)|+|marking(Memory_47)|+|marking(Memory_29)|+|marking(Memory_99)|+|marking(Memory_48)|+|marking(Memory_42)|+|marking(Memory_49)|+|marking(Memory_98)|+|marking(Memory_35)|+|marking(Memory_64)|+|marking(Memory_54)|+|marking(Memory_45)|+|marking(Memory_82)|+|marking(Memory_17)|+|marking(Memory_100)|+|marking(Memory_85)|+|marking(Memory_16)|+|marking(Memory_61)|+|marking(Memory_21)|+|marking(Memory_43)|+|marking(Memory_81)|+|marking(Memory_67)|+|marking(Memory_3)|+|marking(Memory_56)|+|marking(Memory_25)|+|marking(Memory_73)|+|marking(Memory_36)|+|marking(Memory_58)|+|marking(Memory_94)|+|marking(Memory_66)|+|marking(Memory_4)|+|marking(Memory_12)|+|marking(Memory_31)|+|marking(Memory_92)|+|marking(Memory_96)|+|marking(Memory_14)|+|marking(Memory_41)|+|marking(Memory_90)|+|marking(Memory_30)|+|marking(Memory_27)|+|marking(Memory_20)|+|marking(Memory_87)|+|marking(Memory_23)|+|marking(Memory_70)|+|marking(Memory_63)|+|marking(Memory_86)|+|marking(Memory_78)|+|marking(Memory_1)|+|marking(Memory_53)|+|marking(Memory_52)|+|marking(Memory_6)|+|marking(Memory_33)|+|marking(Memory_39)|+|marking(Memory_5)|+|marking(Memory_74)|+|marking(Memory_76)|+|marking(Memory_51)|+|marking(Memory_19)|+|marking(Memory_57)|+|marking(Memory_69)|+|marking(Memory_97)|+|marking(Memory_13)|+|marking(Memory_50)|+|marking(Memory_34)|+|marking(Memory_8)|+|marking(Memory_46)|+|marking(Memory_44)|+|marking(Memory_71)|+|marking(Memory_26)|+|marking(Memory_15)|+|marking(Memory_7)|+|marking(Memory_72)|+|marking(Memory_9)|+|marking(Memory_84)|+|marking(Memory_37)|+|marking(Memory_32)|+|marking(Memory_24)|+|marking(Memory_93)|+|marking(Memory_18)|+|marking(Memory_28)|+|marking(Memory_75)|+|marking(Memory_11)|+|marking(Memory_88)|+|marking(Memory_95)|+|marking(Memory_59)|+|marking(Memory_10)|+|marking(Memory_38)|+|marking(Memory_79)|+|marking(Memory_60)|)) U X ((|marking(Memory_55)|+|marking(Memory_80)|+|marking(Memory_89)|+|marking(Memory_22)|+|marking(Memory_77)|+|marking(Memory_62)|+|marking(Memory_68)|+|marking(Memory_2)|+|marking(Memory_65)|+|marking(Memory_40)|+|marking(Memory_91)|+|marking(Memory_83)|+|marking(Memory_47)|+|marking(Memory_29)|+|marking(Memory_99)|+|marking(Memory_48)|+|marking(Memory_42)|+|marking(Memory_49)|+|marking(Memory_98)|+|marking(Memory_35)|+|marking(Memory_64)|+|marking(Memory_54)|+|marking(Memory_45)|+|marking(Memory_82)|+|marking(Memory_17)|+|marking(Memory_100)|+|marking(Memory_85)|+|marking(Memory_16)|+|marking(Memory_61)|+|marking(Memory_21)|+|marking(Memory_43)|+|marking(Memory_81)|+|marking(Memory_67)|+|marking(Memory_3)|+|marking(Memory_56)|+|marking(Memory_25)|+|marking(Memory_73)|+|marking(Memory_36)|+|marking(Memory_58)|+|marking(Memory_94)|+|marking(Memory_66)|+|marking(Memory_4)|+|marking(Memory_12)|+|marking(Memory_31)|+|marking(Memory_92)|+|marking(Memory_96)|+|marking(Memory_14)|+|marking(Memory_41)|+|marking(Memory_90)|+|marking(Memory_30)|+|marking(Memory_27)|+|marking(Memory_20)|+|marking(Memory_87)|+|marking(Memory_23)|+|marking(Memory_70)|+|marking(Memory_63)|+|marking(Memory_86)|+|marking(Memory_78)|+|marking(Memory_1)|+|marking(Memory_53)|+|marking(Memory_52)|+|marking(Memory_6)|+|marking(Memory_33)|+|marking(Memory_39)|+|marking(Memory_5)|+|marking(Memory_74)|+|marking(Memory_76)|+|marking(Memory_51)|+|marking(Memory_19)|+|marking(Memory_57)|+|marking(Memory_69)|+|marking(Memory_97)|+|marking(Memory_13)|+|marking(Memory_50)|+|marking(Memory_34)|+|marking(Memory_8)|+|marking(Memory_46)|+|marking(Memory_44)|+|marking(Memory_71)|+|marking(Memory_26)|+|marking(Memory_15)|+|marking(Memory_7)|+|marking(Memory_72)|+|marking(Memory_9)|+|marking(Memory_84)|+|marking(Memory_37)|+|marking(Memory_32)|+|marking(Memory_24)|+|marking(Memory_93)|+|marking(Memory_18)|+|marking(Memory_28)|+|marking(Memory_75)|+|marking(Memory_11)|+|marking(Memory_88)|+|marking(Memory_95)|+|marking(Memory_59)|+|marking(Memory_10)|+|marking(Memory_38)|+|marking(Memory_79)|+|marking(Memory_60)|)=(|marking(Active_75)|+|marking(Active_60)|+|marking(Active_38)|+|marking(Active_84)|+|marking(Active_81)|+|marking(Active_4)|+|marking(Active_6)|+|marking(Active_68)|+|marking(Active_55)|+|marking(Active_74)|+|marking(Active_99)|+|marking(Active_33)|+|marking(Active_14)|+|marking(Active_26)|+|marking(Active_50)|+|marking(Active_21)|+|marking(Active_82)|+|marking(Active_91)|+|marking(Active_95)|+|marking(Active_28)|+|marking(Active_90)|+|marking(Active_98)|+|marking(Active_77)|+|marking(Active_83)|+|marking(Active_76)|+|marking(Active_29)|+|marking(Active_63)|+|marking(Active_19)|+|marking(Active_30)|+|marking(Active_51)|+|marking(Active_56)|+|marking(Active_17)|+|marking(Active_65)|+|marking(Active_45)|+|marking(Active_11)|+|marking(Active_13)|+|marking(Active_42)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_62)|+|marking(Active_12)|+|marking(Active_49)|+|marking(Active_53)|+|marking(Active_92)|+|marking(Active_79)|+|marking(Active_93)|+|marking(Active_20)|+|marking(Active_87)|+|marking(Active_85)|+|marking(Active_72)|+|marking(Active_67)|+|marking(Active_46)|+|marking(Active_59)|+|marking(Active_70)|+|marking(Active_25)|+|marking(Active_41)|+|marking(Active_97)|+|marking(Active_37)|+|marking(Active_73)|+|marking(Active_9)|+|marking(Active_96)|+|marking(Active_32)|+|marking(Active_52)|+|marking(Active_39)|+|marking(Active_5)|+|marking(Active_36)|+|marking(Active_15)|+|marking(Active_80)|+|marking(Active_23)|+|marking(Active_40)|+|marking(Active_71)|+|marking(Active_1)|+|marking(Active_86)|+|marking(Active_88)|+|marking(Active_18)|+|marking(Active_64)|+|marking(Active_3)|+|marking(Active_22)|+|marking(Active_43)|+|marking(Active_35)|+|marking(Active_44)|+|marking(Active_66)|+|marking(Active_31)|+|marking(Active_61)|+|marking(Active_89)|+|marking(Active_7)|+|marking(Active_16)|+|marking(Active_47)|+|marking(Active_54)|+|marking(Active_27)|+|marking(Active_24)|+|marking(Active_8)|+|marking(Active_100)|+|marking(Active_69)|+|marking(Active_58)|+|marking(Active_94)|+|marking(Active_78)|+|marking(Active_10)|+|marking(Active_48)|+|marking(Active_57)|)))
ctl p_1861_cardinalitycomparison_full_and: A F (((|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)!=(|marking(Queue_45)|+|marking(Queue_61)|+|marking(Queue_1)|+|marking(Queue_87)|+|marking(Queue_71)|+|marking(Queue_42)|+|marking(Queue_28)|+|marking(Queue_90)|+|marking(Queue_76)|+|marking(Queue_8)|+|marking(Queue_79)|+|marking(Queue_64)|+|marking(Queue_21)|+|marking(Queue_73)|+|marking(Queue_57)|+|marking(Queue_56)|+|marking(Queue_16)|+|marking(Queue_36)|+|marking(Queue_17)|+|marking(Queue_46)|+|marking(Queue_39)|+|marking(Queue_2)|+|marking(Queue_48)|+|marking(Queue_44)|+|marking(Queue_67)|+|marking(Queue_18)|+|marking(Queue_24)|+|marking(Queue_9)|+|marking(Queue_43)|+|marking(Queue_14)|+|marking(Queue_40)|+|marking(Queue_33)|+|marking(Queue_51)|+|marking(Queue_88)|+|marking(Queue_84)|+|marking(Queue_85)|+|marking(Queue_13)|+|marking(Queue_41)|+|marking(Queue_82)|+|marking(Queue_100)|+|marking(Queue_59)|+|marking(Queue_92)|+|marking(Queue_69)|+|marking(Queue_10)|+|marking(Queue_75)|+|marking(Queue_70)|+|marking(Queue_6)|+|marking(Queue_80)|+|marking(Queue_23)|+|marking(Queue_22)|+|marking(Queue_89)|+|marking(Queue_98)|+|marking(Queue_53)|+|marking(Queue_58)|+|marking(Queue_25)|+|marking(Queue_31)|+|marking(Queue_74)|+|marking(Queue_83)|+|marking(Queue_27)|+|marking(Queue_3)|+|marking(Queue_50)|+|marking(Queue_96)|+|marking(Queue_68)|+|marking(Queue_32)|+|marking(Queue_78)|+|marking(Queue_99)|+|marking(Queue_86)|+|marking(Queue_26)|+|marking(Queue_94)|+|marking(Queue_35)|+|marking(Queue_49)|+|marking(Queue_66)|+|marking(Queue_62)|+|marking(Queue_97)|+|marking(Queue_30)|+|marking(Queue_47)|+|marking(Queue_77)|+|marking(Queue_15)|+|marking(Queue_38)|+|marking(Queue_11)|+|marking(Queue_4)|+|marking(Queue_54)|+|marking(Queue_34)|+|marking(Queue_93)|+|marking(Queue_52)|+|marking(Queue_91)|+|marking(Queue_55)|+|marking(Queue_20)|+|marking(Queue_81)|+|marking(Queue_72)|+|marking(Queue_37)|+|marking(Queue_95)|+|marking(Queue_12)|+|marking(Queue_5)|+|marking(Queue_60)|+|marking(Queue_7)|+|marking(Queue_29)|+|marking(Queue_63)|+|marking(Queue_19)|+|marking(Queue_65)|)) & ((|marking(Memory_55)|+|marking(Memory_80)|+|marking(Memory_89)|+|marking(Memory_22)|+|marking(Memory_77)|+|marking(Memory_62)|+|marking(Memory_68)|+|marking(Memory_2)|+|marking(Memory_65)|+|marking(Memory_40)|+|marking(Memory_91)|+|marking(Memory_83)|+|marking(Memory_47)|+|marking(Memory_29)|+|marking(Memory_99)|+|marking(Memory_48)|+|marking(Memory_42)|+|marking(Memory_49)|+|marking(Memory_98)|+|marking(Memory_35)|+|marking(Memory_64)|+|marking(Memory_54)|+|marking(Memory_45)|+|marking(Memory_82)|+|marking(Memory_17)|+|marking(Memory_100)|+|marking(Memory_85)|+|marking(Memory_16)|+|marking(Memory_61)|+|marking(Memory_21)|+|marking(Memory_43)|+|marking(Memory_81)|+|marking(Memory_67)|+|marking(Memory_3)|+|marking(Memory_56)|+|marking(Memory_25)|+|marking(Memory_73)|+|marking(Memory_36)|+|marking(Memory_58)|+|marking(Memory_94)|+|marking(Memory_66)|+|marking(Memory_4)|+|marking(Memory_12)|+|marking(Memory_31)|+|marking(Memory_92)|+|marking(Memory_96)|+|marking(Memory_14)|+|marking(Memory_41)|+|marking(Memory_90)|+|marking(Memory_30)|+|marking(Memory_27)|+|marking(Memory_20)|+|marking(Memory_87)|+|marking(Memory_23)|+|marking(Memory_70)|+|marking(Memory_63)|+|marking(Memory_86)|+|marking(Memory_78)|+|marking(Memory_1)|+|marking(Memory_53)|+|marking(Memory_52)|+|marking(Memory_6)|+|marking(Memory_33)|+|marking(Memory_39)|+|marking(Memory_5)|+|marking(Memory_74)|+|marking(Memory_76)|+|marking(Memory_51)|+|marking(Memory_19)|+|marking(Memory_57)|+|marking(Memory_69)|+|marking(Memory_97)|+|marking(Memory_13)|+|marking(Memory_50)|+|marking(Memory_34)|+|marking(Memory_8)|+|marking(Memory_46)|+|marking(Memory_44)|+|marking(Memory_71)|+|marking(Memory_26)|+|marking(Memory_15)|+|marking(Memory_7)|+|marking(Memory_72)|+|marking(Memory_9)|+|marking(Memory_84)|+|marking(Memory_37)|+|marking(Memory_32)|+|marking(Memory_24)|+|marking(Memory_93)|+|marking(Memory_18)|+|marking(Memory_28)|+|marking(Memory_75)|+|marking(Memory_11)|+|marking(Memory_88)|+|marking(Memory_95)|+|marking(Memory_59)|+|marking(Memory_10)|+|marking(Memory_38)|+|marking(Memory_79)|+|marking(Memory_60)|)>(|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)))
ctl p_1862_cardinalitycomparison_full_or: A G (((|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)!=(|marking(Queue_45)|+|marking(Queue_61)|+|marking(Queue_1)|+|marking(Queue_87)|+|marking(Queue_71)|+|marking(Queue_42)|+|marking(Queue_28)|+|marking(Queue_90)|+|marking(Queue_76)|+|marking(Queue_8)|+|marking(Queue_79)|+|marking(Queue_64)|+|marking(Queue_21)|+|marking(Queue_73)|+|marking(Queue_57)|+|marking(Queue_56)|+|marking(Queue_16)|+|marking(Queue_36)|+|marking(Queue_17)|+|marking(Queue_46)|+|marking(Queue_39)|+|marking(Queue_2)|+|marking(Queue_48)|+|marking(Queue_44)|+|marking(Queue_67)|+|marking(Queue_18)|+|marking(Queue_24)|+|marking(Queue_9)|+|marking(Queue_43)|+|marking(Queue_14)|+|marking(Queue_40)|+|marking(Queue_33)|+|marking(Queue_51)|+|marking(Queue_88)|+|marking(Queue_84)|+|marking(Queue_85)|+|marking(Queue_13)|+|marking(Queue_41)|+|marking(Queue_82)|+|marking(Queue_100)|+|marking(Queue_59)|+|marking(Queue_92)|+|marking(Queue_69)|+|marking(Queue_10)|+|marking(Queue_75)|+|marking(Queue_70)|+|marking(Queue_6)|+|marking(Queue_80)|+|marking(Queue_23)|+|marking(Queue_22)|+|marking(Queue_89)|+|marking(Queue_98)|+|marking(Queue_53)|+|marking(Queue_58)|+|marking(Queue_25)|+|marking(Queue_31)|+|marking(Queue_74)|+|marking(Queue_83)|+|marking(Queue_27)|+|marking(Queue_3)|+|marking(Queue_50)|+|marking(Queue_96)|+|marking(Queue_68)|+|marking(Queue_32)|+|marking(Queue_78)|+|marking(Queue_99)|+|marking(Queue_86)|+|marking(Queue_26)|+|marking(Queue_94)|+|marking(Queue_35)|+|marking(Queue_49)|+|marking(Queue_66)|+|marking(Queue_62)|+|marking(Queue_97)|+|marking(Queue_30)|+|marking(Queue_47)|+|marking(Queue_77)|+|marking(Queue_15)|+|marking(Queue_38)|+|marking(Queue_11)|+|marking(Queue_4)|+|marking(Queue_54)|+|marking(Queue_34)|+|marking(Queue_93)|+|marking(Queue_52)|+|marking(Queue_91)|+|marking(Queue_55)|+|marking(Queue_20)|+|marking(Queue_81)|+|marking(Queue_72)|+|marking(Queue_37)|+|marking(Queue_95)|+|marking(Queue_12)|+|marking(Queue_5)|+|marking(Queue_60)|+|marking(Queue_7)|+|marking(Queue_29)|+|marking(Queue_63)|+|marking(Queue_19)|+|marking(Queue_65)|)) | ((|marking(Memory_55)|+|marking(Memory_80)|+|marking(Memory_89)|+|marking(Memory_22)|+|marking(Memory_77)|+|marking(Memory_62)|+|marking(Memory_68)|+|marking(Memory_2)|+|marking(Memory_65)|+|marking(Memory_40)|+|marking(Memory_91)|+|marking(Memory_83)|+|marking(Memory_47)|+|marking(Memory_29)|+|marking(Memory_99)|+|marking(Memory_48)|+|marking(Memory_42)|+|marking(Memory_49)|+|marking(Memory_98)|+|marking(Memory_35)|+|marking(Memory_64)|+|marking(Memory_54)|+|marking(Memory_45)|+|marking(Memory_82)|+|marking(Memory_17)|+|marking(Memory_100)|+|marking(Memory_85)|+|marking(Memory_16)|+|marking(Memory_61)|+|marking(Memory_21)|+|marking(Memory_43)|+|marking(Memory_81)|+|marking(Memory_67)|+|marking(Memory_3)|+|marking(Memory_56)|+|marking(Memory_25)|+|marking(Memory_73)|+|marking(Memory_36)|+|marking(Memory_58)|+|marking(Memory_94)|+|marking(Memory_66)|+|marking(Memory_4)|+|marking(Memory_12)|+|marking(Memory_31)|+|marking(Memory_92)|+|marking(Memory_96)|+|marking(Memory_14)|+|marking(Memory_41)|+|marking(Memory_90)|+|marking(Memory_30)|+|marking(Memory_27)|+|marking(Memory_20)|+|marking(Memory_87)|+|marking(Memory_23)|+|marking(Memory_70)|+|marking(Memory_63)|+|marking(Memory_86)|+|marking(Memory_78)|+|marking(Memory_1)|+|marking(Memory_53)|+|marking(Memory_52)|+|marking(Memory_6)|+|marking(Memory_33)|+|marking(Memory_39)|+|marking(Memory_5)|+|marking(Memory_74)|+|marking(Memory_76)|+|marking(Memory_51)|+|marking(Memory_19)|+|marking(Memory_57)|+|marking(Memory_69)|+|marking(Memory_97)|+|marking(Memory_13)|+|marking(Memory_50)|+|marking(Memory_34)|+|marking(Memory_8)|+|marking(Memory_46)|+|marking(Memory_44)|+|marking(Memory_71)|+|marking(Memory_26)|+|marking(Memory_15)|+|marking(Memory_7)|+|marking(Memory_72)|+|marking(Memory_9)|+|marking(Memory_84)|+|marking(Memory_37)|+|marking(Memory_32)|+|marking(Memory_24)|+|marking(Memory_93)|+|marking(Memory_18)|+|marking(Memory_28)|+|marking(Memory_75)|+|marking(Memory_11)|+|marking(Memory_88)|+|marking(Memory_95)|+|marking(Memory_59)|+|marking(Memory_10)|+|marking(Memory_38)|+|marking(Memory_79)|+|marking(Memory_60)|)>(|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)))
ctl p_1863_cardinalitycomparison_full_and_notx: A G (((|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)!=(|marking(Queue_45)|+|marking(Queue_61)|+|marking(Queue_1)|+|marking(Queue_87)|+|marking(Queue_71)|+|marking(Queue_42)|+|marking(Queue_28)|+|marking(Queue_90)|+|marking(Queue_76)|+|marking(Queue_8)|+|marking(Queue_79)|+|marking(Queue_64)|+|marking(Queue_21)|+|marking(Queue_73)|+|marking(Queue_57)|+|marking(Queue_56)|+|marking(Queue_16)|+|marking(Queue_36)|+|marking(Queue_17)|+|marking(Queue_46)|+|marking(Queue_39)|+|marking(Queue_2)|+|marking(Queue_48)|+|marking(Queue_44)|+|marking(Queue_67)|+|marking(Queue_18)|+|marking(Queue_24)|+|marking(Queue_9)|+|marking(Queue_43)|+|marking(Queue_14)|+|marking(Queue_40)|+|marking(Queue_33)|+|marking(Queue_51)|+|marking(Queue_88)|+|marking(Queue_84)|+|marking(Queue_85)|+|marking(Queue_13)|+|marking(Queue_41)|+|marking(Queue_82)|+|marking(Queue_100)|+|marking(Queue_59)|+|marking(Queue_92)|+|marking(Queue_69)|+|marking(Queue_10)|+|marking(Queue_75)|+|marking(Queue_70)|+|marking(Queue_6)|+|marking(Queue_80)|+|marking(Queue_23)|+|marking(Queue_22)|+|marking(Queue_89)|+|marking(Queue_98)|+|marking(Queue_53)|+|marking(Queue_58)|+|marking(Queue_25)|+|marking(Queue_31)|+|marking(Queue_74)|+|marking(Queue_83)|+|marking(Queue_27)|+|marking(Queue_3)|+|marking(Queue_50)|+|marking(Queue_96)|+|marking(Queue_68)|+|marking(Queue_32)|+|marking(Queue_78)|+|marking(Queue_99)|+|marking(Queue_86)|+|marking(Queue_26)|+|marking(Queue_94)|+|marking(Queue_35)|+|marking(Queue_49)|+|marking(Queue_66)|+|marking(Queue_62)|+|marking(Queue_97)|+|marking(Queue_30)|+|marking(Queue_47)|+|marking(Queue_77)|+|marking(Queue_15)|+|marking(Queue_38)|+|marking(Queue_11)|+|marking(Queue_4)|+|marking(Queue_54)|+|marking(Queue_34)|+|marking(Queue_93)|+|marking(Queue_52)|+|marking(Queue_91)|+|marking(Queue_55)|+|marking(Queue_20)|+|marking(Queue_81)|+|marking(Queue_72)|+|marking(Queue_37)|+|marking(Queue_95)|+|marking(Queue_12)|+|marking(Queue_5)|+|marking(Queue_60)|+|marking(Queue_7)|+|marking(Queue_29)|+|marking(Queue_63)|+|marking(Queue_19)|+|marking(Queue_65)|)) & ((|marking(Memory_55)|+|marking(Memory_80)|+|marking(Memory_89)|+|marking(Memory_22)|+|marking(Memory_77)|+|marking(Memory_62)|+|marking(Memory_68)|+|marking(Memory_2)|+|marking(Memory_65)|+|marking(Memory_40)|+|marking(Memory_91)|+|marking(Memory_83)|+|marking(Memory_47)|+|marking(Memory_29)|+|marking(Memory_99)|+|marking(Memory_48)|+|marking(Memory_42)|+|marking(Memory_49)|+|marking(Memory_98)|+|marking(Memory_35)|+|marking(Memory_64)|+|marking(Memory_54)|+|marking(Memory_45)|+|marking(Memory_82)|+|marking(Memory_17)|+|marking(Memory_100)|+|marking(Memory_85)|+|marking(Memory_16)|+|marking(Memory_61)|+|marking(Memory_21)|+|marking(Memory_43)|+|marking(Memory_81)|+|marking(Memory_67)|+|marking(Memory_3)|+|marking(Memory_56)|+|marking(Memory_25)|+|marking(Memory_73)|+|marking(Memory_36)|+|marking(Memory_58)|+|marking(Memory_94)|+|marking(Memory_66)|+|marking(Memory_4)|+|marking(Memory_12)|+|marking(Memory_31)|+|marking(Memory_92)|+|marking(Memory_96)|+|marking(Memory_14)|+|marking(Memory_41)|+|marking(Memory_90)|+|marking(Memory_30)|+|marking(Memory_27)|+|marking(Memory_20)|+|marking(Memory_87)|+|marking(Memory_23)|+|marking(Memory_70)|+|marking(Memory_63)|+|marking(Memory_86)|+|marking(Memory_78)|+|marking(Memory_1)|+|marking(Memory_53)|+|marking(Memory_52)|+|marking(Memory_6)|+|marking(Memory_33)|+|marking(Memory_39)|+|marking(Memory_5)|+|marking(Memory_74)|+|marking(Memory_76)|+|marking(Memory_51)|+|marking(Memory_19)|+|marking(Memory_57)|+|marking(Memory_69)|+|marking(Memory_97)|+|marking(Memory_13)|+|marking(Memory_50)|+|marking(Memory_34)|+|marking(Memory_8)|+|marking(Memory_46)|+|marking(Memory_44)|+|marking(Memory_71)|+|marking(Memory_26)|+|marking(Memory_15)|+|marking(Memory_7)|+|marking(Memory_72)|+|marking(Memory_9)|+|marking(Memory_84)|+|marking(Memory_37)|+|marking(Memory_32)|+|marking(Memory_24)|+|marking(Memory_93)|+|marking(Memory_18)|+|marking(Memory_28)|+|marking(Memory_75)|+|marking(Memory_11)|+|marking(Memory_88)|+|marking(Memory_95)|+|marking(Memory_59)|+|marking(Memory_10)|+|marking(Memory_38)|+|marking(Memory_79)|+|marking(Memory_60)|)>(|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)))


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