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=QuasiCertifProtocol-PT-06
export BK_EXAMINATION=ReachabilityPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1655
export BIN_DIR=/home/mcc/BenchKit/bin
BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/QuasiCertifProtocol-PT-06
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is QuasiCertifProtocol-PT-06, examination is ReachabilityPlaceComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo 'START 1371115266'

Execution Outputs of marcie for QuasiCertifProtocol/06 (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=137107412400058_n_2)
=====================================================================
runnning marcie on QuasiCertifProtocol-PT-06 (ReachabilityPlaceComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is QuasiCertifProtocol-PT-06, examination is ReachabilityPlaceComparison
=====================================================================

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

START 1371115266

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 270 NrTr: 116)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m31sec


-> reachability set: #nodes 218170 (2.2e+05) #states 2,271,960 (6)



starting CTL model checker
--------------------------

checking: AG [[[AstopOK=SstopAbort & true] & [[[[n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [[[[n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [[[[n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [[[[n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [[[[n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [[[[n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [[[[n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [[[n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [true & n7_5_2=n8_5_2]]]]] & n7_3_3=n8_3_3] & n7_2_6=n8_2_6]]]] & n7_3_2=n8_3_2] & n7_6_1=n8_6_1] & n7_1_4=n8_1_4]]]] & n7_6_4=n8_6_4] & n7_0_2=n8_0_2] & n7_1_1=n8_1_1]]]] & n7_2_4=n8_2_4] & n7_1_6=n8_1_6] & n7_4_4=n8_4_4]]]] & n7_4_1=n8_4_1] & n7_4_0=n8_4_0] & n7_2_3=n8_2_3]]]] & n7_4_3=n8_4_3] & n7_4_2=n8_4_2] & n7_3_5=n8_3_5]]]] & n7_2_0=n8_2_0] & n7_5_5=n8_5_5] & n7_0_4=n8_0_4]]]] & n7_4_5=n8_4_5] & n7_6_5=n8_6_5] & n7_5_0=n8_5_0]]]
normalized: ~ [E [true U ~ [[[AstopOK=SstopAbort & true] & [n7_5_0=n8_5_0 & [n7_6_5=n8_6_5 & [n7_4_5=n8_4_5 & [n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [n7_2_3=n8_2_3 & [n7_4_0=n8_4_0 & [n7_4_1=n8_4_1 & [n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [n7_4_4=n8_4_4 & [n7_1_6=n8_1_6 & [n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [n7_2_6=n8_2_6 & [n7_3_3=n8_3_3 & [n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [n7_5_2=n8_5_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_7_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m29sec

checking: AG [[[[[[n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [[[[[[n7_6_2=n8_6_2 & [[[[[n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [[n7_6_1=n8_6_1 & [[n7_0_1=n8_0_1 & [[n7_0_0=n8_0_0 & [n7_2_6=n8_2_6 & [n7_3_3=n8_3_3 & [n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [true & n7_5_2=n8_5_2]]]]]]]] & n7_5_3=n8_5_3]] & n7_3_2=n8_3_2]] & n7_1_4=n8_1_4]]]]]]]]]]] & n7_1_6=n8_1_6] & n7_4_4=n8_4_4] & n7_5_6=n8_5_6] & n7_3_1=n8_3_1]] & n7_4_1=n8_4_1] & n7_4_0=n8_4_0] & n7_2_3=n8_2_3] & n7_1_5=n8_1_5] & n7_3_4=n8_3_4]]]]]]]]]]]]]] & n7_4_5=n8_4_5] & n7_6_5=n8_6_5] & n7_5_0=n8_5_0] | [AstopOK=SstopAbort & true]]]
normalized: ~ [E [true U ~ [[[AstopOK=SstopAbort & true] | [n7_5_0=n8_5_0 & [n7_6_5=n8_6_5 & [n7_4_5=n8_4_5 & [n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [n7_2_3=n8_2_3 & [n7_4_0=n8_4_0 & [n7_4_1=n8_4_1 & [n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [n7_4_4=n8_4_4 & [n7_1_6=n8_1_6 & [n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [[[n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [[n7_6_3=n8_6_3 & [n7_5_2=n8_5_2 & true]] & n7_3_0=n8_3_0]]] & n7_3_3=n8_3_3] & n7_2_6=n8_2_6]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_8_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [[[[[[n7_6_2=n8_6_2 & [[[[[n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [[[[[[n7_1_2=n8_1_2 & [[[[n7_5_2=n8_5_2 & true] & n7_6_3=n8_6_3] & n7_3_0=n8_3_0] & n7_1_0=n8_1_0]] & n7_3_3=n8_3_3] & n7_2_6=n8_2_6] & n7_0_0=n8_0_0] & n7_5_3=n8_5_3] & n7_0_1=n8_0_1]]]]]]]]]]]]]] & n7_1_6=n8_1_6] & n7_4_4=n8_4_4] & n7_5_6=n8_5_6] & n7_3_1=n8_3_1]] & n7_4_1=n8_4_1] & n7_4_0=n8_4_0] & n7_2_3=n8_2_3] & n7_1_5=n8_1_5] & n7_3_4=n8_3_4]]]]]]]]]]]]]] & n7_4_5=n8_4_5] & n7_6_5=n8_6_5] & n7_5_0=n8_5_0] & ~ [[true & AstopOK=SstopAbort]]]]
normalized: ~ [E [true U ~ [[~ [[AstopOK=SstopAbort & true]] & [n7_5_0=n8_5_0 & [n7_6_5=n8_6_5 & [n7_4_5=n8_4_5 & [n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [n7_2_3=n8_2_3 & [n7_4_0=n8_4_0 & [n7_4_1=n8_4_1 & [n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [n7_4_4=n8_4_4 & [n7_1_6=n8_1_6 & [n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [n7_2_6=n8_2_6 & [n7_3_3=n8_3_3 & [n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [n7_5_2=n8_5_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_9_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[true & AstopOK=SstopAbort]] | [[[[[n7_5_4=n8_5_4 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[n7_6_4=n8_6_4 & [[[[n7_1_4=n8_1_4 & [[[n7_0_1=n8_0_1 & [[[[n7_3_3=n8_3_3 & [[[[[n7_5_2=n8_5_2 & true] & n7_6_3=n8_6_3] & n7_3_0=n8_3_0] & n7_1_0=n8_1_0] & n7_1_2=n8_1_2]] & n7_2_6=n8_2_6] & n7_0_0=n8_0_0] & n7_5_3=n8_5_3]] & n7_3_2=n8_3_2] & n7_6_1=n8_6_1]] & n7_4_6=n8_4_6] & n7_2_2=n8_2_2] & n7_1_3=n8_1_3]] & n7_0_2=n8_0_2] & n7_1_1=n8_1_1] & n7_0_5=n8_0_5] & n7_6_6=n8_6_6] & n7_0_6=n8_0_6] & n7_2_4=n8_2_4] & n7_1_6=n8_1_6] & n7_4_4=n8_4_4] & n7_5_6=n8_5_6] & n7_3_1=n8_3_1] & n7_6_2=n8_6_2] & n7_4_1=n8_4_1] & n7_4_0=n8_4_0] & n7_2_3=n8_2_3] & n7_1_5=n8_1_5] & n7_3_4=n8_3_4] & n7_2_1=n8_2_1] & n7_4_3=n8_4_3] & n7_4_2=n8_4_2] & n7_3_5=n8_3_5] & n7_0_3=n8_0_3] & n7_5_1=n8_5_1] & n7_2_5=n8_2_5] & n7_2_0=n8_2_0] & n7_5_5=n8_5_5] & n7_0_4=n8_0_4] & n7_3_6=n8_3_6]] & n7_6_0=n8_6_0] & n7_4_5=n8_4_5] & n7_6_5=n8_6_5] & n7_5_0=n8_5_0]]]
normalized: ~ [E [true U ~ [[[n7_5_0=n8_5_0 & [n7_6_5=n8_6_5 & [n7_4_5=n8_4_5 & [n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [n7_2_3=n8_2_3 & [n7_4_0=n8_4_0 & [n7_4_1=n8_4_1 & [n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [n7_4_4=n8_4_4 & [n7_1_6=n8_1_6 & [n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [n7_2_6=n8_2_6 & [n7_3_3=n8_3_3 & [n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [n7_5_2=n8_5_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ~ [[AstopOK=SstopAbort & true]]]]]]

-> the formula is TRUE

FORMULA p_10_placecomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & AstopOK=SstopAbort] | [[[[[n7_5_4=n8_5_4 & [[[[[n7_2_5=n8_2_5 & [[[[[n7_4_3=n8_4_3 & [[[[[[[[[[[[[[[[[[[[[[[[[n7_0_1=n8_0_1 & [[[[[n7_1_2=n8_1_2 & [[[[true & n7_5_2=n8_5_2] & n7_6_3=n8_6_3] & n7_3_0=n8_3_0] & n7_1_0=n8_1_0]] & n7_3_3=n8_3_3] & n7_2_6=n8_2_6] & n7_0_0=n8_0_0] & n7_5_3=n8_5_3]] & n7_3_2=n8_3_2] & n7_6_1=n8_6_1] & n7_1_4=n8_1_4] & n7_4_6=n8_4_6] & n7_2_2=n8_2_2] & n7_1_3=n8_1_3] & n7_6_4=n8_6_4] & n7_0_2=n8_0_2] & n7_1_1=n8_1_1] & n7_0_5=n8_0_5] & n7_6_6=n8_6_6] & n7_0_6=n8_0_6] & n7_2_4=n8_2_4] & n7_1_6=n8_1_6] & n7_4_4=n8_4_4] & n7_5_6=n8_5_6] & n7_3_1=n8_3_1] & n7_6_2=n8_6_2] & n7_4_1=n8_4_1] & n7_4_0=n8_4_0] & n7_2_3=n8_2_3] & n7_1_5=n8_1_5] & n7_3_4=n8_3_4] & n7_2_1=n8_2_1]] & n7_4_2=n8_4_2] & n7_3_5=n8_3_5] & n7_0_3=n8_0_3] & n7_5_1=n8_5_1]] & n7_2_0=n8_2_0] & n7_5_5=n8_5_5] & n7_0_4=n8_0_4] & n7_3_6=n8_3_6]] & n7_6_0=n8_6_0] & n7_4_5=n8_4_5] & n7_6_5=n8_6_5] & n7_5_0=n8_5_0]]]
normalized: ~ [E [true U ~ [[[n7_5_0=n8_5_0 & [n7_6_5=n8_6_5 & [n7_4_5=n8_4_5 & [n7_6_0=n8_6_0 & [n7_5_4=n8_5_4 & [n7_3_6=n8_3_6 & [n7_0_4=n8_0_4 & [n7_5_5=n8_5_5 & [n7_2_0=n8_2_0 & [n7_2_5=n8_2_5 & [n7_5_1=n8_5_1 & [n7_0_3=n8_0_3 & [n7_3_5=n8_3_5 & [n7_4_2=n8_4_2 & [n7_4_3=n8_4_3 & [n7_2_1=n8_2_1 & [n7_3_4=n8_3_4 & [n7_1_5=n8_1_5 & [n7_2_3=n8_2_3 & [n7_4_0=n8_4_0 & [n7_4_1=n8_4_1 & [n7_6_2=n8_6_2 & [n7_3_1=n8_3_1 & [n7_5_6=n8_5_6 & [n7_4_4=n8_4_4 & [n7_1_6=n8_1_6 & [n7_2_4=n8_2_4 & [n7_0_6=n8_0_6 & [n7_6_6=n8_6_6 & [n7_0_5=n8_0_5 & [n7_1_1=n8_1_1 & [n7_0_2=n8_0_2 & [n7_6_4=n8_6_4 & [n7_1_3=n8_1_3 & [n7_2_2=n8_2_2 & [n7_4_6=n8_4_6 & [n7_1_4=n8_1_4 & [n7_6_1=n8_6_1 & [n7_3_2=n8_3_2 & [n7_0_1=n8_0_1 & [n7_5_3=n8_5_3 & [n7_0_0=n8_0_0 & [n7_2_6=n8_2_6 & [n7_3_3=n8_3_3 & [n7_1_2=n8_1_2 & [n7_1_0=n8_1_0 & [n7_3_0=n8_3_0 & [n7_6_3=n8_6_3 & [n7_5_2=n8_5_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [AstopOK=SstopAbort & true]]]]]

-> the formula is FALSE

FORMULA p_11_placecomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[n9_2_6!=n8_2_6 & [[n9_1_0!=n8_1_0 & [[n9_4_1!=n8_4_1 & [[[[[[[n9_6_4!=n8_6_4 & [[[[[[[[[[[[[[[[[[n9_0_3!=n8_0_3 & [[[[[n9_3_1!=n8_3_1 & [[[[true & n9_5_6!=n8_5_6] & n9_5_3!=n8_5_3] & n9_5_5!=n8_5_5] & n9_0_1!=n8_0_1]] & n9_5_0!=n8_5_0] & n9_2_5!=n8_2_5] & n9_2_2!=n8_2_2] & n9_4_2!=n8_4_2]] & n9_4_3!=n8_4_3] & n9_2_3!=n8_2_3] & n9_3_3!=n8_3_3] & n9_3_4!=n8_3_4] & n9_0_0!=n8_0_0] & n9_5_1!=n8_5_1] & n9_6_0!=n8_6_0] & n9_6_6!=n8_6_6] & n9_4_5!=n8_4_5] & n9_1_5!=n8_1_5] & n9_2_0!=n8_2_0] & n9_0_5!=n8_0_5] & n9_4_0!=n8_4_0] & n9_1_4!=n8_1_4] & n9_6_3!=n8_6_3] & n9_2_1!=n8_2_1] & n9_6_2!=n8_6_2]] & n9_1_3!=n8_1_3] & n9_1_2!=n8_1_2] & n9_4_6!=n8_4_6] & n9_3_2!=n8_3_2] & n9_1_6!=n8_1_6] & n9_0_2!=n8_0_2]] & n9_6_1!=n8_6_1]] & n9_5_2!=n8_5_2]] & n9_1_1!=n8_1_1] & n9_5_4!=n8_5_4] & n9_2_4!=n8_2_4] & n9_3_6!=n8_3_6] & n9_4_4!=n8_4_4] & n9_3_5!=n8_3_5] & n9_6_5!=n8_6_5] & n9_0_6!=n8_0_6] & n9_0_4!=n8_0_4] & n9_3_0!=n8_3_0] & [[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[n8_1_4>n7_1_4 & [[[[[[[true & n8_2_2>n7_2_2] & n8_4_1>n7_4_1] & n8_2_0>n7_2_0] & n8_4_6>n7_4_6] & n8_0_6>n7_0_6] & n8_6_4>n7_6_4] & n8_4_5>n7_4_5]] & n8_2_1>n7_2_1] & n8_2_5>n7_2_5] & n8_0_3>n7_0_3] & n8_4_2>n7_4_2] & n8_6_1>n7_6_1] & n8_5_0>n7_5_0] & n8_6_5>n7_6_5] & n8_6_6>n7_6_6] & n8_3_5>n7_3_5] & n8_5_4>n7_5_4] & n8_1_0>n7_1_0] & n8_3_2>n7_3_2] & n8_0_0>n7_0_0] & n8_4_0>n7_4_0] & n8_1_3>n7_1_3] & n8_5_6>n7_5_6] & n8_4_4>n7_4_4] & n8_6_2>n7_6_2] & n8_5_3>n7_5_3] & n8_5_1>n7_5_1] & n8_3_4>n7_3_4] & n8_5_2>n7_5_2] & n8_3_6>n7_3_6] & n8_2_3>n7_2_3] & n8_1_6>n7_1_6] & n8_3_1>n7_3_1] & n8_0_5>n7_0_5] & n8_0_4>n7_0_4] & n8_6_3>n7_6_3] & n8_3_0>n7_3_0] & n8_1_5>n7_1_5] & n8_3_3>n7_3_3] & n8_5_5>n7_5_5] & n8_2_4>n7_2_4] & n8_4_3>n7_4_3] & n8_0_2>n7_0_2] & n8_1_2>n7_1_2] & n8_1_1>n7_1_1] & n8_2_6>n7_2_6] & n8_6_0>n7_6_0] & n8_0_1>n7_0_1]] & [[[[[[[n8_0_2>n7_0_2 | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | n8_2_2>n7_2_2] | n8_4_1>n7_4_1] | n8_2_0>n7_2_0] | n8_4_6>n7_4_6] | n8_0_6>n7_0_6] | n8_6_4>n7_6_4] | n8_4_5>n7_4_5] | n8_1_4>n7_1_4] | n8_2_1>n7_2_1] | n8_2_5>n7_2_5] | n8_0_3>n7_0_3] | n8_4_2>n7_4_2] | n8_6_1>n7_6_1] | n8_5_0>n7_5_0] | n8_6_5>n7_6_5] | n8_6_6>n7_6_6] | n8_3_5>n7_3_5] | n8_5_4>n7_5_4] | n8_1_0>n7_1_0] | n8_3_2>n7_3_2] | n8_0_0>n7_0_0] | n8_4_0>n7_4_0] | n8_1_3>n7_1_3] | n8_5_6>n7_5_6] | n8_4_4>n7_4_4] | n8_6_2>n7_6_2] | n8_5_3>n7_5_3] | n8_5_1>n7_5_1] | n8_3_4>n7_3_4] | n8_5_2>n7_5_2] | n8_3_6>n7_3_6] | n8_2_3>n7_2_3] | n8_1_6>n7_1_6] | n8_3_1>n7_3_1] | n8_0_5>n7_0_5] | n8_0_4>n7_0_4] | n8_6_3>n7_6_3] | n8_3_0>n7_3_0] | n8_1_5>n7_1_5] | n8_3_3>n7_3_3] | n8_5_5>n7_5_5] | n8_2_4>n7_2_4] | n8_4_3>n7_4_3]] | n8_1_2>n7_1_2] | n8_1_1>n7_1_1] | n8_2_6>n7_2_6] | n8_6_0>n7_6_0] | n8_0_1>n7_0_1] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [n8_0_1>n7_0_1 | [n8_6_0>n7_6_0 | [n8_2_6>n7_2_6 | [n8_1_1>n7_1_1 | [n8_1_2>n7_1_2 | [n8_0_2>n7_0_2 | [n8_4_3>n7_4_3 | [n8_2_4>n7_2_4 | [n8_5_5>n7_5_5 | [n8_3_3>n7_3_3 | [n8_1_5>n7_1_5 | [n8_3_0>n7_3_0 | [n8_6_3>n7_6_3 | [n8_0_4>n7_0_4 | [n8_0_5>n7_0_5 | [n8_3_1>n7_3_1 | [n8_1_6>n7_1_6 | [n8_2_3>n7_2_3 | [n8_3_6>n7_3_6 | [n8_5_2>n7_5_2 | [n8_3_4>n7_3_4 | [n8_5_1>n7_5_1 | [n8_5_3>n7_5_3 | [n8_6_2>n7_6_2 | [n8_4_4>n7_4_4 | [n8_5_6>n7_5_6 | [n8_1_3>n7_1_3 | [n8_4_0>n7_4_0 | [n8_0_0>n7_0_0 | [n8_3_2>n7_3_2 | [n8_1_0>n7_1_0 | [n8_5_4>n7_5_4 | [n8_3_5>n7_3_5 | [n8_6_6>n7_6_6 | [n8_6_5>n7_6_5 | [n8_5_0>n7_5_0 | [n8_6_1>n7_6_1 | [n8_4_2>n7_4_2 | [n8_0_3>n7_0_3 | [n8_2_5>n7_2_5 | [n8_2_1>n7_2_1 | [n8_1_4>n7_1_4 | [n8_4_5>n7_4_5 | [n8_6_4>n7_6_4 | [n8_0_6>n7_0_6 | [n8_4_6>n7_4_6 | [n8_2_0>n7_2_0 | [n8_4_1>n7_4_1 | [n8_2_2>n7_2_2 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[n8_0_1>n7_0_1 & [n8_6_0>n7_6_0 & [n8_2_6>n7_2_6 & [n8_1_1>n7_1_1 & [n8_1_2>n7_1_2 & [n8_0_2>n7_0_2 & [n8_4_3>n7_4_3 & [n8_2_4>n7_2_4 & [n8_5_5>n7_5_5 & [n8_3_3>n7_3_3 & [n8_1_5>n7_1_5 & [n8_3_0>n7_3_0 & [n8_6_3>n7_6_3 & [n8_0_4>n7_0_4 & [n8_0_5>n7_0_5 & [n8_3_1>n7_3_1 & [n8_1_6>n7_1_6 & [n8_2_3>n7_2_3 & [n8_3_6>n7_3_6 & [n8_5_2>n7_5_2 & [n8_3_4>n7_3_4 & [n8_5_1>n7_5_1 & [n8_5_3>n7_5_3 & [n8_6_2>n7_6_2 & [n8_4_4>n7_4_4 & [n8_5_6>n7_5_6 & [n8_1_3>n7_1_3 & [n8_4_0>n7_4_0 & [n8_0_0>n7_0_0 & [n8_3_2>n7_3_2 & [n8_1_0>n7_1_0 & [n8_5_4>n7_5_4 & [n8_3_5>n7_3_5 & [n8_6_6>n7_6_6 & [n8_6_5>n7_6_5 & [n8_5_0>n7_5_0 & [n8_6_1>n7_6_1 & [n8_4_2>n7_4_2 & [n8_0_3>n7_0_3 & [n8_2_5>n7_2_5 & [n8_2_1>n7_2_1 & [n8_1_4>n7_1_4 & [n8_4_5>n7_4_5 & [n8_6_4>n7_6_4 & [n8_0_6>n7_0_6 & [n8_4_6>n7_4_6 & [n8_2_0>n7_2_0 & [n8_4_1>n7_4_1 & [n8_2_2>n7_2_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & true]] & [n9_3_0!=n8_3_0 & [n9_0_4!=n8_0_4 & [n9_0_6!=n8_0_6 & [n9_6_5!=n8_6_5 & [n9_3_5!=n8_3_5 & [n9_4_4!=n8_4_4 & [n9_3_6!=n8_3_6 & [n9_2_4!=n8_2_4 & [n9_5_4!=n8_5_4 & [n9_1_1!=n8_1_1 & [n9_2_6!=n8_2_6 & [n9_5_2!=n8_5_2 & [n9_1_0!=n8_1_0 & [n9_6_1!=n8_6_1 & [n9_4_1!=n8_4_1 & [n9_0_2!=n8_0_2 & [n9_1_6!=n8_1_6 & [n9_3_2!=n8_3_2 & [n9_4_6!=n8_4_6 & [n9_1_2!=n8_1_2 & [n9_1_3!=n8_1_3 & [n9_6_4!=n8_6_4 & [n9_6_2!=n8_6_2 & [n9_2_1!=n8_2_1 & [n9_6_3!=n8_6_3 & [n9_1_4!=n8_1_4 & [n9_4_0!=n8_4_0 & [n9_0_5!=n8_0_5 & [n9_2_0!=n8_2_0 & [n9_1_5!=n8_1_5 & [n9_4_5!=n8_4_5 & [n9_6_6!=n8_6_6 & [n9_6_0!=n8_6_0 & [n9_5_1!=n8_5_1 & [n9_0_0!=n8_0_0 & [n9_3_4!=n8_3_4 & [n9_3_3!=n8_3_3 & [n9_2_3!=n8_2_3 & [n9_4_3!=n8_4_3 & [n9_0_3!=n8_0_3 & [n9_4_2!=n8_4_2 & [n9_2_2!=n8_2_2 & [n9_2_5!=n8_2_5 & [n9_5_0!=n8_5_0 & [n9_3_1!=n8_3_1 & [n9_0_1!=n8_0_1 & [n9_5_5!=n8_5_5 & [n9_5_3!=n8_5_3 & [n9_5_6!=n8_5_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_12_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[n8_2_5>n7_2_5 & [[[[[[[[[true & n8_2_2>n7_2_2] & n8_4_1>n7_4_1] & n8_2_0>n7_2_0] & n8_4_6>n7_4_6] & n8_0_6>n7_0_6] & n8_6_4>n7_6_4] & n8_4_5>n7_4_5] & n8_1_4>n7_1_4] & n8_2_1>n7_2_1]] & n8_0_3>n7_0_3] & n8_4_2>n7_4_2] & n8_6_1>n7_6_1] & n8_5_0>n7_5_0] & n8_6_5>n7_6_5] & n8_6_6>n7_6_6] & n8_3_5>n7_3_5] & n8_5_4>n7_5_4] & n8_1_0>n7_1_0] & n8_3_2>n7_3_2] & n8_0_0>n7_0_0] & n8_4_0>n7_4_0] & n8_1_3>n7_1_3] & n8_5_6>n7_5_6] & n8_4_4>n7_4_4] & n8_6_2>n7_6_2] & n8_5_3>n7_5_3] & n8_5_1>n7_5_1] & n8_3_4>n7_3_4] & n8_5_2>n7_5_2] & n8_3_6>n7_3_6] & n8_2_3>n7_2_3] & n8_1_6>n7_1_6] & n8_3_1>n7_3_1] & n8_0_5>n7_0_5] & n8_0_4>n7_0_4] & n8_6_3>n7_6_3] & n8_3_0>n7_3_0] & n8_1_5>n7_1_5] & n8_3_3>n7_3_3] & n8_5_5>n7_5_5] & n8_2_4>n7_2_4] & n8_4_3>n7_4_3] & n8_0_2>n7_0_2] & n8_1_2>n7_1_2] & n8_1_1>n7_1_1] & n8_2_6>n7_2_6] & n8_6_0>n7_6_0] & n8_0_1>n7_0_1] & true] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | n8_2_2>n7_2_2] | n8_4_1>n7_4_1] | n8_2_0>n7_2_0] | n8_4_6>n7_4_6] | n8_0_6>n7_0_6] | n8_6_4>n7_6_4] | n8_4_5>n7_4_5] | n8_1_4>n7_1_4] | n8_2_1>n7_2_1] | n8_2_5>n7_2_5] | n8_0_3>n7_0_3] | n8_4_2>n7_4_2] | n8_6_1>n7_6_1] | n8_5_0>n7_5_0] | n8_6_5>n7_6_5] | n8_6_6>n7_6_6] | n8_3_5>n7_3_5] | n8_5_4>n7_5_4] | n8_1_0>n7_1_0] | n8_3_2>n7_3_2] | n8_0_0>n7_0_0] | n8_4_0>n7_4_0] | n8_1_3>n7_1_3] | n8_5_6>n7_5_6] | n8_4_4>n7_4_4] | n8_6_2>n7_6_2] | n8_5_3>n7_5_3] | n8_5_1>n7_5_1] | n8_3_4>n7_3_4] | n8_5_2>n7_5_2] | n8_3_6>n7_3_6] | n8_2_3>n7_2_3] | n8_1_6>n7_1_6] | n8_3_1>n7_3_1] | n8_0_5>n7_0_5] | n8_0_4>n7_0_4] | n8_6_3>n7_6_3] | n8_3_0>n7_3_0] | n8_1_5>n7_1_5] | n8_3_3>n7_3_3] | n8_5_5>n7_5_5] | n8_2_4>n7_2_4] | n8_4_3>n7_4_3] | n8_0_2>n7_0_2] | n8_1_2>n7_1_2] | n8_1_1>n7_1_1] | n8_2_6>n7_2_6] | n8_6_0>n7_6_0] | n8_0_1>n7_0_1] | false]] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & n9_5_6!=n8_5_6] & n9_5_3!=n8_5_3] & n9_5_5!=n8_5_5] & n9_0_1!=n8_0_1] & n9_3_1!=n8_3_1] & n9_5_0!=n8_5_0] & n9_2_5!=n8_2_5] & n9_2_2!=n8_2_2] & n9_4_2!=n8_4_2] & n9_0_3!=n8_0_3] & n9_4_3!=n8_4_3] & n9_2_3!=n8_2_3] & n9_3_3!=n8_3_3] & n9_3_4!=n8_3_4] & n9_0_0!=n8_0_0] & n9_5_1!=n8_5_1] & n9_6_0!=n8_6_0] & n9_6_6!=n8_6_6] & n9_4_5!=n8_4_5] & n9_1_5!=n8_1_5] & n9_2_0!=n8_2_0] & n9_0_5!=n8_0_5] & n9_4_0!=n8_4_0] & n9_1_4!=n8_1_4] & n9_6_3!=n8_6_3] & n9_2_1!=n8_2_1] & n9_6_2!=n8_6_2] & n9_6_4!=n8_6_4] & n9_1_3!=n8_1_3] & n9_1_2!=n8_1_2] & n9_4_6!=n8_4_6] & n9_3_2!=n8_3_2] & n9_1_6!=n8_1_6] & n9_0_2!=n8_0_2] & n9_4_1!=n8_4_1] & n9_6_1!=n8_6_1] & n9_1_0!=n8_1_0] & n9_5_2!=n8_5_2] & n9_2_6!=n8_2_6] & n9_1_1!=n8_1_1] & n9_5_4!=n8_5_4] & n9_2_4!=n8_2_4] & n9_3_6!=n8_3_6] & n9_4_4!=n8_4_4] & n9_3_5!=n8_3_5] & n9_6_5!=n8_6_5] & n9_0_6!=n8_0_6] & n9_0_4!=n8_0_4] & n9_3_0!=n8_3_0]]]
normalized: ~ [E [true U ~ [[[n9_3_0!=n8_3_0 & [n9_0_4!=n8_0_4 & [n9_0_6!=n8_0_6 & [n9_6_5!=n8_6_5 & [n9_3_5!=n8_3_5 & [n9_4_4!=n8_4_4 & [n9_3_6!=n8_3_6 & [n9_2_4!=n8_2_4 & [n9_5_4!=n8_5_4 & [n9_1_1!=n8_1_1 & [n9_2_6!=n8_2_6 & [n9_5_2!=n8_5_2 & [n9_1_0!=n8_1_0 & [n9_6_1!=n8_6_1 & [n9_4_1!=n8_4_1 & [n9_0_2!=n8_0_2 & [n9_1_6!=n8_1_6 & [n9_3_2!=n8_3_2 & [n9_4_6!=n8_4_6 & [n9_1_2!=n8_1_2 & [n9_1_3!=n8_1_3 & [n9_6_4!=n8_6_4 & [n9_6_2!=n8_6_2 & [n9_2_1!=n8_2_1 & [n9_6_3!=n8_6_3 & [n9_1_4!=n8_1_4 & [n9_4_0!=n8_4_0 & [n9_0_5!=n8_0_5 & [n9_2_0!=n8_2_0 & [n9_1_5!=n8_1_5 & [n9_4_5!=n8_4_5 & [n9_6_6!=n8_6_6 & [n9_6_0!=n8_6_0 & [n9_5_1!=n8_5_1 & [n9_0_0!=n8_0_0 & [n9_3_4!=n8_3_4 & [n9_3_3!=n8_3_3 & [n9_2_3!=n8_2_3 & [n9_4_3!=n8_4_3 & [n9_0_3!=n8_0_3 & [n9_4_2!=n8_4_2 & [n9_2_2!=n8_2_2 & [n9_2_5!=n8_2_5 & [n9_5_0!=n8_5_0 & [n9_3_1!=n8_3_1 & [n9_0_1!=n8_0_1 & [n9_5_5!=n8_5_5 & [n9_5_3!=n8_5_3 & [n9_5_6!=n8_5_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [[false | [n8_0_1>n7_0_1 | [n8_6_0>n7_6_0 | [n8_2_6>n7_2_6 | [n8_1_1>n7_1_1 | [n8_1_2>n7_1_2 | [n8_0_2>n7_0_2 | [n8_4_3>n7_4_3 | [n8_2_4>n7_2_4 | [n8_5_5>n7_5_5 | [n8_3_3>n7_3_3 | [n8_1_5>n7_1_5 | [n8_3_0>n7_3_0 | [n8_6_3>n7_6_3 | [n8_0_4>n7_0_4 | [n8_0_5>n7_0_5 | [n8_3_1>n7_3_1 | [n8_1_6>n7_1_6 | [n8_2_3>n7_2_3 | [n8_3_6>n7_3_6 | [n8_5_2>n7_5_2 | [n8_3_4>n7_3_4 | [n8_5_1>n7_5_1 | [n8_5_3>n7_5_3 | [n8_6_2>n7_6_2 | [n8_4_4>n7_4_4 | [n8_5_6>n7_5_6 | [n8_1_3>n7_1_3 | [n8_4_0>n7_4_0 | [n8_0_0>n7_0_0 | [n8_3_2>n7_3_2 | [n8_1_0>n7_1_0 | [n8_5_4>n7_5_4 | [n8_3_5>n7_3_5 | [n8_6_6>n7_6_6 | [n8_6_5>n7_6_5 | [n8_5_0>n7_5_0 | [n8_6_1>n7_6_1 | [n8_4_2>n7_4_2 | [n8_0_3>n7_0_3 | [n8_2_5>n7_2_5 | [n8_2_1>n7_2_1 | [n8_1_4>n7_1_4 | [n8_4_5>n7_4_5 | [n8_6_4>n7_6_4 | [n8_0_6>n7_0_6 | [n8_4_6>n7_4_6 | [n8_2_0>n7_2_0 | [n8_4_1>n7_4_1 | [n8_2_2>n7_2_2 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [true & [n8_0_1>n7_0_1 & [n8_6_0>n7_6_0 & [n8_2_6>n7_2_6 & [n8_1_1>n7_1_1 & [n8_1_2>n7_1_2 & [n8_0_2>n7_0_2 & [n8_4_3>n7_4_3 & [n8_2_4>n7_2_4 & [n8_5_5>n7_5_5 & [n8_3_3>n7_3_3 & [n8_1_5>n7_1_5 & [n8_3_0>n7_3_0 & [n8_6_3>n7_6_3 & [n8_0_4>n7_0_4 & [n8_0_5>n7_0_5 & [n8_3_1>n7_3_1 & [n8_1_6>n7_1_6 & [n8_2_3>n7_2_3 & [n8_3_6>n7_3_6 & [n8_5_2>n7_5_2 & [n8_3_4>n7_3_4 & [n8_5_1>n7_5_1 & [n8_5_3>n7_5_3 & [n8_6_2>n7_6_2 & [n8_4_4>n7_4_4 & [n8_5_6>n7_5_6 & [n8_1_3>n7_1_3 & [n8_4_0>n7_4_0 & [n8_0_0>n7_0_0 & [n8_3_2>n7_3_2 & [n8_1_0>n7_1_0 & [n8_5_4>n7_5_4 & [n8_3_5>n7_3_5 & [n8_6_6>n7_6_6 & [n8_6_5>n7_6_5 & [n8_5_0>n7_5_0 & [n8_6_1>n7_6_1 & [n8_4_2>n7_4_2 & [n8_0_3>n7_0_3 & [n8_2_5>n7_2_5 & [n8_2_1>n7_2_1 & [n8_1_4>n7_1_4 & [n8_4_5>n7_4_5 & [n8_6_4>n7_6_4 & [n8_0_6>n7_0_6 & [n8_4_6>n7_4_6 & [n8_2_0>n7_2_0 & [n8_4_1>n7_4_1 & [n8_2_2>n7_2_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_13_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & n9_5_6!=n8_5_6] & n9_5_3!=n8_5_3] & n9_5_5!=n8_5_5] & n9_0_1!=n8_0_1] & n9_3_1!=n8_3_1] & n9_5_0!=n8_5_0] & n9_2_5!=n8_2_5] & n9_2_2!=n8_2_2] & n9_4_2!=n8_4_2] & n9_0_3!=n8_0_3] & n9_4_3!=n8_4_3] & n9_2_3!=n8_2_3] & n9_3_3!=n8_3_3] & n9_3_4!=n8_3_4] & n9_0_0!=n8_0_0] & n9_5_1!=n8_5_1] & n9_6_0!=n8_6_0] & n9_6_6!=n8_6_6] & n9_4_5!=n8_4_5] & n9_1_5!=n8_1_5] & n9_2_0!=n8_2_0] & n9_0_5!=n8_0_5] & n9_4_0!=n8_4_0] & n9_1_4!=n8_1_4] & n9_6_3!=n8_6_3] & n9_2_1!=n8_2_1] & n9_6_2!=n8_6_2] & n9_6_4!=n8_6_4] & n9_1_3!=n8_1_3] & n9_1_2!=n8_1_2] & n9_4_6!=n8_4_6] & n9_3_2!=n8_3_2] & n9_1_6!=n8_1_6] & n9_0_2!=n8_0_2] & n9_4_1!=n8_4_1] & n9_6_1!=n8_6_1] & n9_1_0!=n8_1_0] & n9_5_2!=n8_5_2] & n9_2_6!=n8_2_6] & n9_1_1!=n8_1_1] & n9_5_4!=n8_5_4] & n9_2_4!=n8_2_4] & n9_3_6!=n8_3_6] & n9_4_4!=n8_4_4] & n9_3_5!=n8_3_5] & n9_6_5!=n8_6_5] & n9_0_6!=n8_0_6] & n9_0_4!=n8_0_4] & n9_3_0!=n8_3_0] & [[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & n8_2_2>n7_2_2] & n8_4_1>n7_4_1] & n8_2_0>n7_2_0] & n8_4_6>n7_4_6] & n8_0_6>n7_0_6] & n8_6_4>n7_6_4] & n8_4_5>n7_4_5] & n8_1_4>n7_1_4] & n8_2_1>n7_2_1] & n8_2_5>n7_2_5] & n8_0_3>n7_0_3] & n8_4_2>n7_4_2] & n8_6_1>n7_6_1] & n8_5_0>n7_5_0] & n8_6_5>n7_6_5] & n8_6_6>n7_6_6] & n8_3_5>n7_3_5] & n8_5_4>n7_5_4] & n8_1_0>n7_1_0] & n8_3_2>n7_3_2] & n8_0_0>n7_0_0] & n8_4_0>n7_4_0] & n8_1_3>n7_1_3] & n8_5_6>n7_5_6] & n8_4_4>n7_4_4] & n8_6_2>n7_6_2] & n8_5_3>n7_5_3] & n8_5_1>n7_5_1] & n8_3_4>n7_3_4] & n8_5_2>n7_5_2] & n8_3_6>n7_3_6] & n8_2_3>n7_2_3] & n8_1_6>n7_1_6] & n8_3_1>n7_3_1] & n8_0_5>n7_0_5] & n8_0_4>n7_0_4] & n8_6_3>n7_6_3] & n8_3_0>n7_3_0] & n8_1_5>n7_1_5] & n8_3_3>n7_3_3] & n8_5_5>n7_5_5] & n8_2_4>n7_2_4] & n8_4_3>n7_4_3] & n8_0_2>n7_0_2] & n8_1_2>n7_1_2] & n8_1_1>n7_1_1] & n8_2_6>n7_2_6] & n8_6_0>n7_6_0] & n8_0_1>n7_0_1]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | n8_2_2>n7_2_2] | n8_4_1>n7_4_1] | n8_2_0>n7_2_0] | n8_4_6>n7_4_6] | n8_0_6>n7_0_6] | n8_6_4>n7_6_4] | n8_4_5>n7_4_5] | n8_1_4>n7_1_4] | n8_2_1>n7_2_1] | n8_2_5>n7_2_5] | n8_0_3>n7_0_3] | n8_4_2>n7_4_2] | n8_6_1>n7_6_1] | n8_5_0>n7_5_0] | n8_6_5>n7_6_5] | n8_6_6>n7_6_6] | n8_3_5>n7_3_5] | n8_5_4>n7_5_4] | n8_1_0>n7_1_0] | n8_3_2>n7_3_2] | n8_0_0>n7_0_0] | n8_4_0>n7_4_0] | n8_1_3>n7_1_3] | n8_5_6>n7_5_6] | n8_4_4>n7_4_4] | n8_6_2>n7_6_2] | n8_5_3>n7_5_3] | n8_5_1>n7_5_1] | n8_3_4>n7_3_4] | n8_5_2>n7_5_2] | n8_3_6>n7_3_6] | n8_2_3>n7_2_3] | n8_1_6>n7_1_6] | n8_3_1>n7_3_1] | n8_0_5>n7_0_5] | n8_0_4>n7_0_4] | n8_6_3>n7_6_3] | n8_3_0>n7_3_0] | n8_1_5>n7_1_5] | n8_3_3>n7_3_3] | n8_5_5>n7_5_5] | n8_2_4>n7_2_4] | n8_4_3>n7_4_3] | n8_0_2>n7_0_2] | n8_1_2>n7_1_2] | n8_1_1>n7_1_1] | n8_2_6>n7_2_6] | n8_6_0>n7_6_0] | n8_0_1>n7_0_1] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [n8_0_1>n7_0_1 | [n8_6_0>n7_6_0 | [n8_2_6>n7_2_6 | [n8_1_1>n7_1_1 | [n8_1_2>n7_1_2 | [n8_0_2>n7_0_2 | [n8_4_3>n7_4_3 | [n8_2_4>n7_2_4 | [n8_5_5>n7_5_5 | [n8_3_3>n7_3_3 | [n8_1_5>n7_1_5 | [n8_3_0>n7_3_0 | [n8_6_3>n7_6_3 | [n8_0_4>n7_0_4 | [n8_0_5>n7_0_5 | [n8_3_1>n7_3_1 | [n8_1_6>n7_1_6 | [n8_2_3>n7_2_3 | [n8_3_6>n7_3_6 | [n8_5_2>n7_5_2 | [n8_3_4>n7_3_4 | [n8_5_1>n7_5_1 | [n8_5_3>n7_5_3 | [n8_6_2>n7_6_2 | [n8_4_4>n7_4_4 | [n8_5_6>n7_5_6 | [n8_1_3>n7_1_3 | [n8_4_0>n7_4_0 | [n8_0_0>n7_0_0 | [n8_3_2>n7_3_2 | [n8_1_0>n7_1_0 | [n8_5_4>n7_5_4 | [n8_3_5>n7_3_5 | [n8_6_6>n7_6_6 | [n8_6_5>n7_6_5 | [n8_5_0>n7_5_0 | [n8_6_1>n7_6_1 | [n8_4_2>n7_4_2 | [n8_0_3>n7_0_3 | [n8_2_5>n7_2_5 | [n8_2_1>n7_2_1 | [n8_1_4>n7_1_4 | [n8_4_5>n7_4_5 | [n8_6_4>n7_6_4 | [n8_0_6>n7_0_6 | [n8_4_6>n7_4_6 | [n8_2_0>n7_2_0 | [n8_4_1>n7_4_1 | [n8_2_2>n7_2_2 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[n8_0_1>n7_0_1 & [n8_6_0>n7_6_0 & [n8_2_6>n7_2_6 & [n8_1_1>n7_1_1 & [n8_1_2>n7_1_2 & [n8_0_2>n7_0_2 & [n8_4_3>n7_4_3 & [n8_2_4>n7_2_4 & [n8_5_5>n7_5_5 & [n8_3_3>n7_3_3 & [n8_1_5>n7_1_5 & [n8_3_0>n7_3_0 & [n8_6_3>n7_6_3 & [n8_0_4>n7_0_4 & [n8_0_5>n7_0_5 & [n8_3_1>n7_3_1 & [n8_1_6>n7_1_6 & [n8_2_3>n7_2_3 & [n8_3_6>n7_3_6 & [n8_5_2>n7_5_2 & [n8_3_4>n7_3_4 & [n8_5_1>n7_5_1 & [n8_5_3>n7_5_3 & [n8_6_2>n7_6_2 & [n8_4_4>n7_4_4 & [n8_5_6>n7_5_6 & [n8_1_3>n7_1_3 & [n8_4_0>n7_4_0 & [n8_0_0>n7_0_0 & [n8_3_2>n7_3_2 & [n8_1_0>n7_1_0 & [n8_5_4>n7_5_4 & [n8_3_5>n7_3_5 & [n8_6_6>n7_6_6 & [n8_6_5>n7_6_5 & [n8_5_0>n7_5_0 & [n8_6_1>n7_6_1 & [n8_4_2>n7_4_2 & [n8_0_3>n7_0_3 & [n8_2_5>n7_2_5 & [n8_2_1>n7_2_1 & [n8_1_4>n7_1_4 & [n8_4_5>n7_4_5 & [n8_6_4>n7_6_4 & [n8_0_6>n7_0_6 & [n8_4_6>n7_4_6 & [n8_2_0>n7_2_0 & [n8_4_1>n7_4_1 & [n8_2_2>n7_2_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & true]] & [n9_3_0!=n8_3_0 & [n9_0_4!=n8_0_4 & [n9_0_6!=n8_0_6 & [n9_6_5!=n8_6_5 & [n9_3_5!=n8_3_5 & [n9_4_4!=n8_4_4 & [n9_3_6!=n8_3_6 & [n9_2_4!=n8_2_4 & [n9_5_4!=n8_5_4 & [n9_1_1!=n8_1_1 & [n9_2_6!=n8_2_6 & [n9_5_2!=n8_5_2 & [n9_1_0!=n8_1_0 & [n9_6_1!=n8_6_1 & [n9_4_1!=n8_4_1 & [n9_0_2!=n8_0_2 & [n9_1_6!=n8_1_6 & [n9_3_2!=n8_3_2 & [n9_4_6!=n8_4_6 & [n9_1_2!=n8_1_2 & [n9_1_3!=n8_1_3 & [n9_6_4!=n8_6_4 & [n9_6_2!=n8_6_2 & [n9_2_1!=n8_2_1 & [n9_6_3!=n8_6_3 & [n9_1_4!=n8_1_4 & [n9_4_0!=n8_4_0 & [n9_0_5!=n8_0_5 & [n9_2_0!=n8_2_0 & [n9_1_5!=n8_1_5 & [n9_4_5!=n8_4_5 & [n9_6_6!=n8_6_6 & [n9_6_0!=n8_6_0 & [n9_5_1!=n8_5_1 & [n9_0_0!=n8_0_0 & [n9_3_4!=n8_3_4 & [n9_3_3!=n8_3_3 & [n9_2_3!=n8_2_3 & [n9_4_3!=n8_4_3 & [n9_0_3!=n8_0_3 & [n9_4_2!=n8_4_2 & [n9_2_2!=n8_2_2 & [n9_2_5!=n8_2_5 & [n9_5_0!=n8_5_0 & [n9_3_1!=n8_3_1 & [n9_0_1!=n8_0_1 & [n9_5_5!=n8_5_5 & [n9_5_3!=n8_5_3 & [n9_5_6!=n8_5_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_14_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m48sec

STOP 1371115375

--------------------
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


initing FirstDep: 0m0sec

84051 117217 137672 218170
iterations count:4067 (35), effective:116 (1)

initing FirstDep: 0m0sec


iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

iterations count:116 (1), effective:0 (0)

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