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

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

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

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

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

START 1369719386

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 500 NrTr: 500)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369719387

--------------------
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_1880_mix_eq_x: E F (X (true & (|marking(Catch2_40)|=|marking(Think_40)|) & (|marking(Catch2_88)|=|marking(Think_88)|) & (|marking(Catch2_36)|=|marking(Think_36)|) & (|marking(Catch2_15)|=|marking(Think_15)|) & (|marking(Catch2_16)|=|marking(Think_16)|) & (|marking(Catch2_24)|=|marking(Think_24)|) & (|marking(Catch2_9)|=|marking(Think_9)|) & (|marking(Catch2_92)|=|marking(Think_92)|) & (|marking(Catch2_61)|=|marking(Think_61)|) & (|marking(Catch2_99)|=|marking(Think_99)|) & (|marking(Catch2_57)|=|marking(Think_57)|) & (|marking(Catch2_28)|=|marking(Think_28)|) & (|marking(Catch2_68)|=|marking(Think_68)|) & (|marking(Catch2_4)|=|marking(Think_4)|) & (|marking(Catch2_82)|=|marking(Think_82)|) & (|marking(Catch2_56)|=|marking(Think_56)|) & (|marking(Catch2_42)|=|marking(Think_42)|) & (|marking(Catch2_52)|=|marking(Think_52)|) & (|marking(Catch2_59)|=|marking(Think_59)|) & (|marking(Catch2_98)|=|marking(Think_98)|) & (|marking(Catch2_58)|=|marking(Think_58)|) & (|marking(Catch2_35)|=|marking(Think_35)|) & (|marking(Catch2_30)|=|marking(Think_30)|) & (|marking(Catch2_45)|=|marking(Think_45)|) & (|marking(Catch2_20)|=|marking(Think_20)|) & (|marking(Catch2_79)|=|marking(Think_79)|) & (|marking(Catch2_13)|=|marking(Think_13)|) & (|marking(Catch2_18)|=|marking(Think_18)|) & (|marking(Catch2_83)|=|marking(Think_83)|) & (|marking(Catch2_46)|=|marking(Think_46)|) & (|marking(Catch2_97)|=|marking(Think_97)|) & (|marking(Catch2_51)|=|marking(Think_51)|) & (|marking(Catch2_23)|=|marking(Think_23)|) & (|marking(Catch2_75)|=|marking(Think_75)|) & (|marking(Catch2_81)|=|marking(Think_81)|) & (|marking(Catch2_37)|=|marking(Think_37)|) & (|marking(Catch2_67)|=|marking(Think_67)|) & (|marking(Catch2_69)|=|marking(Think_69)|) & (|marking(Catch2_38)|=|marking(Think_38)|) & (|marking(Catch2_66)|=|marking(Think_66)|) & (|marking(Catch2_100)|=|marking(Think_100)|) & (|marking(Catch2_12)|=|marking(Think_12)|) & (|marking(Catch2_71)|=|marking(Think_71)|) & (|marking(Catch2_96)|=|marking(Think_96)|) & (|marking(Catch2_95)|=|marking(Think_95)|) & (|marking(Catch2_41)|=|marking(Think_41)|) & (|marking(Catch2_21)|=|marking(Think_21)|) & (|marking(Catch2_19)|=|marking(Think_19)|) & (|marking(Catch2_70)|=|marking(Think_70)|) & (|marking(Catch2_32)|=|marking(Think_32)|) & (|marking(Catch2_2)|=|marking(Think_2)|) & (|marking(Catch2_87)|=|marking(Think_87)|) & (|marking(Catch2_31)|=|marking(Think_31)|) & (|marking(Catch2_34)|=|marking(Think_34)|) & (|marking(Catch2_47)|=|marking(Think_47)|) & (|marking(Catch2_29)|=|marking(Think_29)|) & (|marking(Catch2_27)|=|marking(Think_27)|) & (|marking(Catch2_64)|=|marking(Think_64)|) & (|marking(Catch2_26)|=|marking(Think_26)|) & (|marking(Catch2_93)|=|marking(Think_93)|) & (|marking(Catch2_50)|=|marking(Think_50)|) & (|marking(Catch2_94)|=|marking(Think_94)|) & (|marking(Catch2_78)|=|marking(Think_78)|) & (|marking(Catch2_22)|=|marking(Think_22)|) & (|marking(Catch2_76)|=|marking(Think_76)|) & (|marking(Catch2_1)|=|marking(Think_1)|) & (|marking(Catch2_73)|=|marking(Think_73)|) & (|marking(Catch2_85)|=|marking(Think_85)|) & (|marking(Catch2_44)|=|marking(Think_44)|) & (|marking(Catch2_62)|=|marking(Think_62)|) & (|marking(Catch2_54)|=|marking(Think_54)|) & (|marking(Catch2_84)|=|marking(Think_84)|) & (|marking(Catch2_65)|=|marking(Think_65)|) & (|marking(Catch2_7)|=|marking(Think_7)|) & (|marking(Catch2_74)|=|marking(Think_74)|) & (|marking(Catch2_11)|=|marking(Think_11)|) & (|marking(Catch2_14)|=|marking(Think_14)|) & (|marking(Catch2_63)|=|marking(Think_63)|) & (|marking(Catch2_17)|=|marking(Think_17)|) & (|marking(Catch2_25)|=|marking(Think_25)|) & (|marking(Catch2_8)|=|marking(Think_8)|) & (|marking(Catch2_53)|=|marking(Think_53)|) & (|marking(Catch2_86)|=|marking(Think_86)|) & (|marking(Catch2_39)|=|marking(Think_39)|) & (|marking(Catch2_6)|=|marking(Think_6)|) & (|marking(Catch2_55)|=|marking(Think_55)|) & (|marking(Catch2_91)|=|marking(Think_91)|) & (|marking(Catch2_80)|=|marking(Think_80)|) & (|marking(Catch2_10)|=|marking(Think_10)|) & (|marking(Catch2_3)|=|marking(Think_3)|) & (|marking(Catch2_49)|=|marking(Think_49)|) & (|marking(Catch2_33)|=|marking(Think_33)|) & (|marking(Catch2_90)|=|marking(Think_90)|) & (|marking(Catch2_77)|=|marking(Think_77)|) & (|marking(Catch2_89)|=|marking(Think_89)|) & (|marking(Catch2_5)|=|marking(Think_5)|) & (|marking(Catch2_72)|=|marking(Think_72)|) & (|marking(Catch2_43)|=|marking(Think_43)|) & (|marking(Catch2_60)|=|marking(Think_60)|) & (|marking(Catch2_48)|=|marking(Think_48)|)) xor !(FF2a_73? | FF2a_25? | FF2a_52? | FF2a_90? | FF2a_70? | FF2a_97? | FF2a_47? | FF2a_88? | FF2a_76? | FF2a_83? | FF2a_15? | FF2a_5? | FF2a_51? | FF2a_41? | FF2a_55? | FF2a_30? | FF2a_66? | FF2a_23? | FF2a_37? | FF2a_61? | FF2a_17? | FF2a_99? | FF2a_20? | FF2a_8? | FF2a_33? | FF2a_49? | FF2a_3? | FF2a_10? | FF2a_53? | FF2a_71? | FF2a_6? | FF2a_16? | FF2a_36? | FF2a_57? | FF2a_38? | FF2a_44? | FF2a_87? | FF2a_42? | FF2a_7? | FF2a_13? | FF2a_2? | FF2a_45? | FF2a_58? | FF2a_14? | FF2a_34? | FF2a_65? | FF2a_11? | FF2a_9? | FF2a_81? | FF2a_93? | FF2a_79? | FF2a_96? | FF2a_89? | FF2a_95? | FF2a_100? | FF2a_94? | FF2a_69? | FF2a_46? | FF2a_27? | FF2a_12? | FF2a_59? | FF2a_92? | FF2a_18? | FF2a_28? | FF2a_40? | FF2a_60? | FF2a_91? | FF2a_48? | FF2a_85? | FF2a_4? | FF2a_24? | FF2a_29? | FF2a_67? | FF2a_19? | FF2a_64? | FF2a_63? | FF2a_54? | FF2a_75? | FF2a_74? | FF2a_31? | FF2a_22? | FF2a_82? | FF2a_84? | FF2a_72? | FF2a_86? | FF2a_1? | FF2a_35? | FF2a_98? | FF2a_21? | FF2a_39? | FF2a_80? | FF2a_32? | FF2a_56? | FF2a_50? | FF2a_26? | FF2a_62? | FF2a_43? | FF2a_77? | FF2a_68? | FF2a_78?))
ctl p_1881_mix_full_and: A G ((FF1a_40? | FF1a_34? | FF1a_69? | FF1a_73? | FF1a_85? | FF1a_80? | FF1a_33? | FF1a_79? | FF1a_20? | FF1a_14? | FF1a_55? | FF1a_44? | FF1a_36? | FF1a_32? | FF1a_67? | FF1a_65? | FF1a_88? | FF1a_30? | FF1a_9? | FF1a_66? | FF1a_86? | FF1a_77? | FF1a_87? | FF1a_13? | FF1a_45? | FF1a_21? | FF1a_78? | FF1a_3? | FF1a_54? | FF1a_47? | FF1a_37? | FF1a_95? | FF1a_64? | FF1a_60? | FF1a_56? | FF1a_5? | FF1a_12? | FF1a_74? | FF1a_97? | FF1a_23? | FF1a_84? | FF1a_68? | FF1a_39? | FF1a_43? | FF1a_46? | FF1a_38? | FF1a_10? | FF1a_59? | FF1a_16? | FF1a_89? | FF1a_7? | FF1a_57? | FF1a_26? | FF1a_99? | FF1a_81? | FF1a_4? | FF1a_8? | FF1a_82? | FF1a_75? | FF1a_71? | FF1a_58? | FF1a_51? | FF1a_25? | FF1a_93? | FF1a_48? | FF1a_50? | FF1a_29? | FF1a_94? | FF1a_53? | FF1a_100? | FF1a_90? | FF1a_35? | FF1a_24? | FF1a_92? | FF1a_63? | FF1a_70? | FF1a_72? | FF1a_62? | FF1a_18? | FF1a_49? | FF1a_96? | FF1a_15? | FF1a_41? | FF1a_17? | FF1a_31? | FF1a_91? | FF1a_27? | FF1a_6? | FF1a_11? | FF1a_19? | FF1a_76? | FF1a_28? | FF1a_98? | FF1a_1? | FF1a_61? | FF1a_42? | FF1a_2? | FF1a_22? | FF1a_52? | FF1a_83?) & ((|marking(Catch2_79)|+|marking(Catch2_52)|+|marking(Catch2_96)|+|marking(Catch2_53)|+|marking(Catch2_69)|+|marking(Catch2_43)|+|marking(Catch2_98)|+|marking(Catch2_44)|+|marking(Catch2_85)|+|marking(Catch2_29)|+|marking(Catch2_76)|+|marking(Catch2_22)|+|marking(Catch2_62)|+|marking(Catch2_19)|+|marking(Catch2_48)|+|marking(Catch2_95)|+|marking(Catch2_78)|+|marking(Catch2_91)|+|marking(Catch2_37)|+|marking(Catch2_12)|+|marking(Catch2_92)|+|marking(Catch2_45)|+|marking(Catch2_47)|+|marking(Catch2_46)|+|marking(Catch2_83)|+|marking(Catch2_15)|+|marking(Catch2_67)|+|marking(Catch2_42)|+|marking(Catch2_68)|+|marking(Catch2_66)|+|marking(Catch2_5)|+|marking(Catch2_14)|+|marking(Catch2_73)|+|marking(Catch2_61)|+|marking(Catch2_50)|+|marking(Catch2_36)|+|marking(Catch2_75)|+|marking(Catch2_35)|+|marking(Catch2_93)|+|marking(Catch2_54)|+|marking(Catch2_32)|+|marking(Catch2_94)|+|marking(Catch2_51)|+|marking(Catch2_24)|+|marking(Catch2_6)|+|marking(Catch2_56)|+|marking(Catch2_60)|+|marking(Catch2_9)|+|marking(Catch2_72)|+|marking(Catch2_97)|+|marking(Catch2_17)|+|marking(Catch2_65)|+|marking(Catch2_33)|+|marking(Catch2_84)|+|marking(Catch2_4)|+|marking(Catch2_7)|+|marking(Catch2_100)|+|marking(Catch2_89)|+|marking(Catch2_55)|+|marking(Catch2_59)|+|marking(Catch2_31)|+|marking(Catch2_3)|+|marking(Catch2_77)|+|marking(Catch2_38)|+|marking(Catch2_86)|+|marking(Catch2_2)|+|marking(Catch2_34)|+|marking(Catch2_40)|+|marking(Catch2_13)|+|marking(Catch2_1)|+|marking(Catch2_74)|+|marking(Catch2_10)|+|marking(Catch2_16)|+|marking(Catch2_49)|+|marking(Catch2_27)|+|marking(Catch2_58)|+|marking(Catch2_87)|+|marking(Catch2_99)|+|marking(Catch2_21)|+|marking(Catch2_64)|+|marking(Catch2_25)|+|marking(Catch2_82)|+|marking(Catch2_18)|+|marking(Catch2_11)|+|marking(Catch2_39)|+|marking(Catch2_90)|+|marking(Catch2_28)|+|marking(Catch2_57)|+|marking(Catch2_88)|+|marking(Catch2_8)|+|marking(Catch2_81)|+|marking(Catch2_20)|+|marking(Catch2_41)|+|marking(Catch2_23)|+|marking(Catch2_70)|+|marking(Catch2_71)|+|marking(Catch2_26)|+|marking(Catch2_63)|+|marking(Catch2_30)|+|marking(Catch2_80)|)>(|marking(Think_68)|+|marking(Think_52)|+|marking(Think_44)|+|marking(Think_2)|+|marking(Think_38)|+|marking(Think_36)|+|marking(Think_26)|+|marking(Think_60)|+|marking(Think_6)|+|marking(Think_13)|+|marking(Think_11)|+|marking(Think_4)|+|marking(Think_87)|+|marking(Think_59)|+|marking(Think_9)|+|marking(Think_40)|+|marking(Think_23)|+|marking(Think_99)|+|marking(Think_56)|+|marking(Think_57)|+|marking(Think_94)|+|marking(Think_22)|+|marking(Think_63)|+|marking(Think_74)|+|marking(Think_98)|+|marking(Think_55)|+|marking(Think_92)|+|marking(Think_76)|+|marking(Think_93)|+|marking(Think_12)|+|marking(Think_19)|+|marking(Think_49)|+|marking(Think_53)|+|marking(Think_48)|+|marking(Think_17)|+|marking(Think_8)|+|marking(Think_10)|+|marking(Think_58)|+|marking(Think_15)|+|marking(Think_41)|+|marking(Think_25)|+|marking(Think_77)|+|marking(Think_96)|+|marking(Think_39)|+|marking(Think_62)|+|marking(Think_85)|+|marking(Think_32)|+|marking(Think_78)|+|marking(Think_24)|+|marking(Think_91)|+|marking(Think_7)|+|marking(Think_18)|+|marking(Think_29)|+|marking(Think_21)|+|marking(Think_73)|+|marking(Think_46)|+|marking(Think_16)|+|marking(Think_51)|+|marking(Think_95)|+|marking(Think_79)|+|marking(Think_89)|+|marking(Think_5)|+|marking(Think_97)|+|marking(Think_81)|+|marking(Think_67)|+|marking(Think_75)|+|marking(Think_65)|+|marking(Think_61)|+|marking(Think_100)|+|marking(Think_43)|+|marking(Think_20)|+|marking(Think_64)|+|marking(Think_37)|+|marking(Think_31)|+|marking(Think_71)|+|marking(Think_35)|+|marking(Think_70)|+|marking(Think_88)|+|marking(Think_83)|+|marking(Think_69)|+|marking(Think_42)|+|marking(Think_72)|+|marking(Think_34)|+|marking(Think_66)|+|marking(Think_80)|+|marking(Think_1)|+|marking(Think_50)|+|marking(Think_28)|+|marking(Think_54)|+|marking(Think_45)|+|marking(Think_84)|+|marking(Think_14)|+|marking(Think_90)|+|marking(Think_3)|+|marking(Think_33)|+|marking(Think_27)|+|marking(Think_47)|+|marking(Think_86)|+|marking(Think_30)|+|marking(Think_82)|)))
ctl p_1882_mix_full_or: E F ((FF1a_40? | FF1a_34? | FF1a_69? | FF1a_73? | FF1a_85? | FF1a_80? | FF1a_33? | FF1a_79? | FF1a_20? | FF1a_14? | FF1a_55? | FF1a_44? | FF1a_36? | FF1a_32? | FF1a_67? | FF1a_65? | FF1a_88? | FF1a_30? | FF1a_9? | FF1a_66? | FF1a_86? | FF1a_77? | FF1a_87? | FF1a_13? | FF1a_45? | FF1a_21? | FF1a_78? | FF1a_3? | FF1a_54? | FF1a_47? | FF1a_37? | FF1a_95? | FF1a_64? | FF1a_60? | FF1a_56? | FF1a_5? | FF1a_12? | FF1a_74? | FF1a_97? | FF1a_23? | FF1a_84? | FF1a_68? | FF1a_39? | FF1a_43? | FF1a_46? | FF1a_38? | FF1a_10? | FF1a_59? | FF1a_16? | FF1a_89? | FF1a_7? | FF1a_57? | FF1a_26? | FF1a_99? | FF1a_81? | FF1a_4? | FF1a_8? | FF1a_82? | FF1a_75? | FF1a_71? | FF1a_58? | FF1a_51? | FF1a_25? | FF1a_93? | FF1a_48? | FF1a_50? | FF1a_29? | FF1a_94? | FF1a_53? | FF1a_100? | FF1a_90? | FF1a_35? | FF1a_24? | FF1a_92? | FF1a_63? | FF1a_70? | FF1a_72? | FF1a_62? | FF1a_18? | FF1a_49? | FF1a_96? | FF1a_15? | FF1a_41? | FF1a_17? | FF1a_31? | FF1a_91? | FF1a_27? | FF1a_6? | FF1a_11? | FF1a_19? | FF1a_76? | FF1a_28? | FF1a_98? | FF1a_1? | FF1a_61? | FF1a_42? | FF1a_2? | FF1a_22? | FF1a_52? | FF1a_83?) | ((|marking(Catch2_79)|+|marking(Catch2_52)|+|marking(Catch2_96)|+|marking(Catch2_53)|+|marking(Catch2_69)|+|marking(Catch2_43)|+|marking(Catch2_98)|+|marking(Catch2_44)|+|marking(Catch2_85)|+|marking(Catch2_29)|+|marking(Catch2_76)|+|marking(Catch2_22)|+|marking(Catch2_62)|+|marking(Catch2_19)|+|marking(Catch2_48)|+|marking(Catch2_95)|+|marking(Catch2_78)|+|marking(Catch2_91)|+|marking(Catch2_37)|+|marking(Catch2_12)|+|marking(Catch2_92)|+|marking(Catch2_45)|+|marking(Catch2_47)|+|marking(Catch2_46)|+|marking(Catch2_83)|+|marking(Catch2_15)|+|marking(Catch2_67)|+|marking(Catch2_42)|+|marking(Catch2_68)|+|marking(Catch2_66)|+|marking(Catch2_5)|+|marking(Catch2_14)|+|marking(Catch2_73)|+|marking(Catch2_61)|+|marking(Catch2_50)|+|marking(Catch2_36)|+|marking(Catch2_75)|+|marking(Catch2_35)|+|marking(Catch2_93)|+|marking(Catch2_54)|+|marking(Catch2_32)|+|marking(Catch2_94)|+|marking(Catch2_51)|+|marking(Catch2_24)|+|marking(Catch2_6)|+|marking(Catch2_56)|+|marking(Catch2_60)|+|marking(Catch2_9)|+|marking(Catch2_72)|+|marking(Catch2_97)|+|marking(Catch2_17)|+|marking(Catch2_65)|+|marking(Catch2_33)|+|marking(Catch2_84)|+|marking(Catch2_4)|+|marking(Catch2_7)|+|marking(Catch2_100)|+|marking(Catch2_89)|+|marking(Catch2_55)|+|marking(Catch2_59)|+|marking(Catch2_31)|+|marking(Catch2_3)|+|marking(Catch2_77)|+|marking(Catch2_38)|+|marking(Catch2_86)|+|marking(Catch2_2)|+|marking(Catch2_34)|+|marking(Catch2_40)|+|marking(Catch2_13)|+|marking(Catch2_1)|+|marking(Catch2_74)|+|marking(Catch2_10)|+|marking(Catch2_16)|+|marking(Catch2_49)|+|marking(Catch2_27)|+|marking(Catch2_58)|+|marking(Catch2_87)|+|marking(Catch2_99)|+|marking(Catch2_21)|+|marking(Catch2_64)|+|marking(Catch2_25)|+|marking(Catch2_82)|+|marking(Catch2_18)|+|marking(Catch2_11)|+|marking(Catch2_39)|+|marking(Catch2_90)|+|marking(Catch2_28)|+|marking(Catch2_57)|+|marking(Catch2_88)|+|marking(Catch2_8)|+|marking(Catch2_81)|+|marking(Catch2_20)|+|marking(Catch2_41)|+|marking(Catch2_23)|+|marking(Catch2_70)|+|marking(Catch2_71)|+|marking(Catch2_26)|+|marking(Catch2_63)|+|marking(Catch2_30)|+|marking(Catch2_80)|)>(|marking(Think_68)|+|marking(Think_52)|+|marking(Think_44)|+|marking(Think_2)|+|marking(Think_38)|+|marking(Think_36)|+|marking(Think_26)|+|marking(Think_60)|+|marking(Think_6)|+|marking(Think_13)|+|marking(Think_11)|+|marking(Think_4)|+|marking(Think_87)|+|marking(Think_59)|+|marking(Think_9)|+|marking(Think_40)|+|marking(Think_23)|+|marking(Think_99)|+|marking(Think_56)|+|marking(Think_57)|+|marking(Think_94)|+|marking(Think_22)|+|marking(Think_63)|+|marking(Think_74)|+|marking(Think_98)|+|marking(Think_55)|+|marking(Think_92)|+|marking(Think_76)|+|marking(Think_93)|+|marking(Think_12)|+|marking(Think_19)|+|marking(Think_49)|+|marking(Think_53)|+|marking(Think_48)|+|marking(Think_17)|+|marking(Think_8)|+|marking(Think_10)|+|marking(Think_58)|+|marking(Think_15)|+|marking(Think_41)|+|marking(Think_25)|+|marking(Think_77)|+|marking(Think_96)|+|marking(Think_39)|+|marking(Think_62)|+|marking(Think_85)|+|marking(Think_32)|+|marking(Think_78)|+|marking(Think_24)|+|marking(Think_91)|+|marking(Think_7)|+|marking(Think_18)|+|marking(Think_29)|+|marking(Think_21)|+|marking(Think_73)|+|marking(Think_46)|+|marking(Think_16)|+|marking(Think_51)|+|marking(Think_95)|+|marking(Think_79)|+|marking(Think_89)|+|marking(Think_5)|+|marking(Think_97)|+|marking(Think_81)|+|marking(Think_67)|+|marking(Think_75)|+|marking(Think_65)|+|marking(Think_61)|+|marking(Think_100)|+|marking(Think_43)|+|marking(Think_20)|+|marking(Think_64)|+|marking(Think_37)|+|marking(Think_31)|+|marking(Think_71)|+|marking(Think_35)|+|marking(Think_70)|+|marking(Think_88)|+|marking(Think_83)|+|marking(Think_69)|+|marking(Think_42)|+|marking(Think_72)|+|marking(Think_34)|+|marking(Think_66)|+|marking(Think_80)|+|marking(Think_1)|+|marking(Think_50)|+|marking(Think_28)|+|marking(Think_54)|+|marking(Think_45)|+|marking(Think_84)|+|marking(Think_14)|+|marking(Think_90)|+|marking(Think_3)|+|marking(Think_33)|+|marking(Think_27)|+|marking(Think_47)|+|marking(Think_86)|+|marking(Think_30)|+|marking(Think_82)|)))
ctl p_1883_mix_full_and_notx: A G ((FF1a_40? | FF1a_34? | FF1a_69? | FF1a_73? | FF1a_85? | FF1a_80? | FF1a_33? | FF1a_79? | FF1a_20? | FF1a_14? | FF1a_55? | FF1a_44? | FF1a_36? | FF1a_32? | FF1a_67? | FF1a_65? | FF1a_88? | FF1a_30? | FF1a_9? | FF1a_66? | FF1a_86? | FF1a_77? | FF1a_87? | FF1a_13? | FF1a_45? | FF1a_21? | FF1a_78? | FF1a_3? | FF1a_54? | FF1a_47? | FF1a_37? | FF1a_95? | FF1a_64? | FF1a_60? | FF1a_56? | FF1a_5? | FF1a_12? | FF1a_74? | FF1a_97? | FF1a_23? | FF1a_84? | FF1a_68? | FF1a_39? | FF1a_43? | FF1a_46? | FF1a_38? | FF1a_10? | FF1a_59? | FF1a_16? | FF1a_89? | FF1a_7? | FF1a_57? | FF1a_26? | FF1a_99? | FF1a_81? | FF1a_4? | FF1a_8? | FF1a_82? | FF1a_75? | FF1a_71? | FF1a_58? | FF1a_51? | FF1a_25? | FF1a_93? | FF1a_48? | FF1a_50? | FF1a_29? | FF1a_94? | FF1a_53? | FF1a_100? | FF1a_90? | FF1a_35? | FF1a_24? | FF1a_92? | FF1a_63? | FF1a_70? | FF1a_72? | FF1a_62? | FF1a_18? | FF1a_49? | FF1a_96? | FF1a_15? | FF1a_41? | FF1a_17? | FF1a_31? | FF1a_91? | FF1a_27? | FF1a_6? | FF1a_11? | FF1a_19? | FF1a_76? | FF1a_28? | FF1a_98? | FF1a_1? | FF1a_61? | FF1a_42? | FF1a_2? | FF1a_22? | FF1a_52? | FF1a_83?) & !((|marking(Catch2_79)|+|marking(Catch2_52)|+|marking(Catch2_96)|+|marking(Catch2_53)|+|marking(Catch2_69)|+|marking(Catch2_43)|+|marking(Catch2_98)|+|marking(Catch2_44)|+|marking(Catch2_85)|+|marking(Catch2_29)|+|marking(Catch2_76)|+|marking(Catch2_22)|+|marking(Catch2_62)|+|marking(Catch2_19)|+|marking(Catch2_48)|+|marking(Catch2_95)|+|marking(Catch2_78)|+|marking(Catch2_91)|+|marking(Catch2_37)|+|marking(Catch2_12)|+|marking(Catch2_92)|+|marking(Catch2_45)|+|marking(Catch2_47)|+|marking(Catch2_46)|+|marking(Catch2_83)|+|marking(Catch2_15)|+|marking(Catch2_67)|+|marking(Catch2_42)|+|marking(Catch2_68)|+|marking(Catch2_66)|+|marking(Catch2_5)|+|marking(Catch2_14)|+|marking(Catch2_73)|+|marking(Catch2_61)|+|marking(Catch2_50)|+|marking(Catch2_36)|+|marking(Catch2_75)|+|marking(Catch2_35)|+|marking(Catch2_93)|+|marking(Catch2_54)|+|marking(Catch2_32)|+|marking(Catch2_94)|+|marking(Catch2_51)|+|marking(Catch2_24)|+|marking(Catch2_6)|+|marking(Catch2_56)|+|marking(Catch2_60)|+|marking(Catch2_9)|+|marking(Catch2_72)|+|marking(Catch2_97)|+|marking(Catch2_17)|+|marking(Catch2_65)|+|marking(Catch2_33)|+|marking(Catch2_84)|+|marking(Catch2_4)|+|marking(Catch2_7)|+|marking(Catch2_100)|+|marking(Catch2_89)|+|marking(Catch2_55)|+|marking(Catch2_59)|+|marking(Catch2_31)|+|marking(Catch2_3)|+|marking(Catch2_77)|+|marking(Catch2_38)|+|marking(Catch2_86)|+|marking(Catch2_2)|+|marking(Catch2_34)|+|marking(Catch2_40)|+|marking(Catch2_13)|+|marking(Catch2_1)|+|marking(Catch2_74)|+|marking(Catch2_10)|+|marking(Catch2_16)|+|marking(Catch2_49)|+|marking(Catch2_27)|+|marking(Catch2_58)|+|marking(Catch2_87)|+|marking(Catch2_99)|+|marking(Catch2_21)|+|marking(Catch2_64)|+|marking(Catch2_25)|+|marking(Catch2_82)|+|marking(Catch2_18)|+|marking(Catch2_11)|+|marking(Catch2_39)|+|marking(Catch2_90)|+|marking(Catch2_28)|+|marking(Catch2_57)|+|marking(Catch2_88)|+|marking(Catch2_8)|+|marking(Catch2_81)|+|marking(Catch2_20)|+|marking(Catch2_41)|+|marking(Catch2_23)|+|marking(Catch2_70)|+|marking(Catch2_71)|+|marking(Catch2_26)|+|marking(Catch2_63)|+|marking(Catch2_30)|+|marking(Catch2_80)|)>(|marking(Think_68)|+|marking(Think_52)|+|marking(Think_44)|+|marking(Think_2)|+|marking(Think_38)|+|marking(Think_36)|+|marking(Think_26)|+|marking(Think_60)|+|marking(Think_6)|+|marking(Think_13)|+|marking(Think_11)|+|marking(Think_4)|+|marking(Think_87)|+|marking(Think_59)|+|marking(Think_9)|+|marking(Think_40)|+|marking(Think_23)|+|marking(Think_99)|+|marking(Think_56)|+|marking(Think_57)|+|marking(Think_94)|+|marking(Think_22)|+|marking(Think_63)|+|marking(Think_74)|+|marking(Think_98)|+|marking(Think_55)|+|marking(Think_92)|+|marking(Think_76)|+|marking(Think_93)|+|marking(Think_12)|+|marking(Think_19)|+|marking(Think_49)|+|marking(Think_53)|+|marking(Think_48)|+|marking(Think_17)|+|marking(Think_8)|+|marking(Think_10)|+|marking(Think_58)|+|marking(Think_15)|+|marking(Think_41)|+|marking(Think_25)|+|marking(Think_77)|+|marking(Think_96)|+|marking(Think_39)|+|marking(Think_62)|+|marking(Think_85)|+|marking(Think_32)|+|marking(Think_78)|+|marking(Think_24)|+|marking(Think_91)|+|marking(Think_7)|+|marking(Think_18)|+|marking(Think_29)|+|marking(Think_21)|+|marking(Think_73)|+|marking(Think_46)|+|marking(Think_16)|+|marking(Think_51)|+|marking(Think_95)|+|marking(Think_79)|+|marking(Think_89)|+|marking(Think_5)|+|marking(Think_97)|+|marking(Think_81)|+|marking(Think_67)|+|marking(Think_75)|+|marking(Think_65)|+|marking(Think_61)|+|marking(Think_100)|+|marking(Think_43)|+|marking(Think_20)|+|marking(Think_64)|+|marking(Think_37)|+|marking(Think_31)|+|marking(Think_71)|+|marking(Think_35)|+|marking(Think_70)|+|marking(Think_88)|+|marking(Think_83)|+|marking(Think_69)|+|marking(Think_42)|+|marking(Think_72)|+|marking(Think_34)|+|marking(Think_66)|+|marking(Think_80)|+|marking(Think_1)|+|marking(Think_50)|+|marking(Think_28)|+|marking(Think_54)|+|marking(Think_45)|+|marking(Think_84)|+|marking(Think_14)|+|marking(Think_90)|+|marking(Think_3)|+|marking(Think_33)|+|marking(Think_27)|+|marking(Think_47)|+|marking(Think_86)|+|marking(Think_30)|+|marking(Think_82)|)))


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