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

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

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

START 1369641583

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 972 NrTr: 1016)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m7sec


-> reachability set: #nodes 19347 (1.9e+04) #states 974,325 (5)



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

checking: AG [[[[[[[masterList_3_1_0!=0.000000000000000 & [[masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [[masterList_2_1_2!=0.000000000000000 & [[masterList_0_2_2!=0.000000000000000 & [[masterList_3_3_3!=0.000000000000000 & [[masterList_3_2_0!=0.000000000000000 & [[masterList_2_1_3!=0.000000000000000 & [[masterList_0_1_3!=0.000000000000000 & [[masterList_1_1_3!=0.000000000000000 & [[masterList_2_1_0!=0.000000000000000 & [[masterList_1_3_1!=0.000000000000000 & [[masterList_3_1_3!=0.000000000000000 & [[masterList_1_3_2!=0.000000000000000 & [[masterList_0_2_3!=0.000000000000000 & [[masterList_0_2_0!=0.000000000000000 & [[masterList_0_3_0!=0.000000000000000 & [[masterList_2_3_3!=0.000000000000000 & [[masterList_3_1_2!=0.000000000000000 & [[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[masterList_3_3_1!=0.000000000000000 & [[true & 1.000000000000000!=masterList_2_2_2] & masterList_0_2_1!=0.000000000000000]] & masterList_1_3_0!=0.000000000000000]]] & masterList_0_1_1!=0.000000000000000]] & masterList_2_3_1!=0.000000000000000]] & masterList_2_3_2!=0.000000000000000]] & masterList_3_2_1!=0.000000000000000]] & masterList_2_3_0!=0.000000000000000]] & masterList_3_3_2!=0.000000000000000]] & masterList_2_2_0!=0.000000000000000]] & masterList_3_1_1!=0.000000000000000]] & masterList_0_1_2!=0.000000000000000]] & masterList_1_1_1!=0.000000000000000]] & masterList_0_3_3!=0.000000000000000]] & masterList_1_2_1!=0.000000000000000]] & masterList_3_3_0!=0.000000000000000]] & masterList_1_1_0!=0.000000000000000]] & masterList_1_2_3!=0.000000000000000]] & masterList_3_2_3!=0.000000000000000]] & masterList_2_2_1!=0.000000000000000]] & masterList_1_2_2!=0.000000000000000]] & masterList_1_1_2!=0.000000000000000]] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] & [[masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [[masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [[[[[[[[[[[masterList_0_1_3!=0.000000000000000 & [[[masterList_1_1_1!=0.000000000000000 & [[masterList_2_1_0!=0.000000000000000 & [[masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [[masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]]]]]]]]]]]]]]]]]] & masterList_2_2_0!=0.000000000000000]]]] & masterList_0_1_2!=0.000000000000000]] & masterList_2_2_2!=0.000000000000000]] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000]] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000]]] & masterList_1_2_2!=0.000000000000000]]] & masterList_3_1_0!=0.000000000000000]]] & masterList_0_3_2!=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1866_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m4sec

checking: AG [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [[[[masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [[masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [[[[masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [[masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [[masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]]]]]]]]] & masterList_3_2_1!=0.000000000000000]]]]]]] & masterList_3_1_3!=0.000000000000000]]]] & masterList_2_1_0!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000]]]]]]]]]]]]] & masterList_2_2_1!=0.000000000000000]]]]] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000]]] | [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[[[true & 1.000000000000000!=masterList_2_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [[masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [[[[[masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [[masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [[[masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [[[[[masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000]]]]] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000]]]]]]]]]]]]]]]]] & masterList_0_1_3!=0.000000000000000]]]]] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000]]]]]] & masterList_0_1_0!=0.000000000000000]]]]]] | [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [[[[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_2_2_2] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1867_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [[masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [[masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [[masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [[masterList_1_1_1!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [[masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]]]]]]]]] & masterList_3_2_1!=0.000000000000000]]]]]]]]]]]]] & masterList_1_1_3!=0.000000000000000]]] & masterList_1_2_1!=0.000000000000000]]]]]]]]] & masterList_2_1_2!=0.000000000000000]]]]]]] & masterList_1_3_3!=0.000000000000000]]]] & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [[masterList_2_1_2!=0.000000000000000 & [[[masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [[masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [[masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [[[[[[[[masterList_3_1_1!=0.000000000000000 & [[[masterList_1_3_2!=0.000000000000000 & [[[[[[[[[masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [[[[[masterList_0_2_1!=0.000000000000000 & [true & 1.000000000000000!=masterList_2_2_3]] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000]]]] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000]] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000]] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000]]] & masterList_2_1_3!=0.000000000000000]]] & masterList_1_1_0!=0.000000000000000]]] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000]] & masterList_2_2_1!=0.000000000000000]]]]]]]]]]]
normalized: E [true U [[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [[[masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [[[[[[[[masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [[[[[[[masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]]]]]]]]]]] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000]]]]]]]] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000]]]]]]]]]]]]]] & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1868_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[[[[[masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [[masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [[masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [[masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [[masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [[masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [[masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]]]]]] & masterList_0_1_1!=0.000000000000000]]]]] & masterList_0_3_0!=0.000000000000000]]]]] & masterList_3_3_2!=0.000000000000000]]]]] & masterList_1_3_1!=0.000000000000000]]]]] & masterList_1_1_3!=0.000000000000000]]]]] & masterList_3_3_0!=0.000000000000000]]]]] & masterList_0_2_2!=0.000000000000000]]]]] & masterList_1_2_2!=0.000000000000000]] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] | [[[[[[[[[[[[[masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [[masterList_1_1_0!=0.000000000000000 & [[masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [[[[[[[[[masterList_2_2_0!=0.000000000000000 & [[[[[masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [[masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [[[[[masterList_1_2_0!=0.000000000000000 & [[masterList_3_3_1!=0.000000000000000 & [[true & 1.000000000000000!=masterList_2_2_2] & masterList_0_2_1!=0.000000000000000]] & masterList_1_3_0!=0.000000000000000]] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]]] & masterList_0_3_0!=0.000000000000000]]] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000]] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000]]]]] & masterList_3_2_0!=0.000000000000000]] & masterList_3_3_3!=0.000000000000000]]] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000]]]
normalized: E [true U [[masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [[[masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_3 & true]]]]] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [[[[[masterList_0_3_3!=0.000000000000000 & [[[[[[[[masterList_2_2_0!=0.000000000000000 & [[masterList_3_3_2!=0.000000000000000 & [[[masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [[[masterList_2_3_3!=0.000000000000000 & [[[[[masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000]]] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000]] & masterList_1_3_2!=0.000000000000000]] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000]] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1869_markingcomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [AG [[[masterList_0_3_2!=0.000000000000000 & [[masterList_1_3_3!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_2_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000]]] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000]] & masterList_0_3_1!=0.000000000000000]] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [[[masterList_2_3_2!=0.000000000000000 & [[[[[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]]] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000]] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: EG [~ [E [true U ~ [[[[[masterList_1_3_3!=0.000000000000000 & [[[[[masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [[[[[[masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [[masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [[[[[[[[[true & 1.000000000000000!=masterList_2_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]]]]]]] & masterList_0_2_3!=0.000000000000000]]]]]]]]]]]]]]]]]] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000]]]] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000]] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_2_2_2 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1870_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_3_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_2_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: EG [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_1_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000]]]]]]]] & [masterList_2_2_3!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_3_2_1] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1871_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_2_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [[[[[[masterList_1_1_2!=0.000000000000000 & [[[[masterList_2_2_1!=0.000000000000000 & [[[[[masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [[masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [[masterList_0_3_3!=0.000000000000000 & [[[[masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_3_2_1 & true]]]]]]]]]]]]]]]]]]]]]]] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000]] & masterList_0_1_3!=0.000000000000000]]] & masterList_3_3_0!=0.000000000000000]]]] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000]] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000]] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000]]]
normalized: E [true U [[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_2_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_3_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1872_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [[[masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [[masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_3_2_1 & true]]]]]]]]]]]]]]]]]]]] & masterList_1_3_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000]]] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [[[[[[[[[masterList_1_2_0!=0.000000000000000 & [[[[true & 1.000000000000000!=masterList_1_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000]] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [EG [~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [[[[[[masterList_2_3_2!=0.000000000000000 & [[[masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [[[[[[true & 1.000000000000000!=masterList_1_2_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000]]] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000]] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000]]] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [[[[[[[[[masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [[[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_3_2_1] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000]]]]]]]]]]]]]]]] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1873_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m22sec

STOP 1369641606

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

2413 2983 4406 5170 8021 8230 9312 9485 12146 12633 13261 15641 17360 19352
iterations count:14854 (14), effective:108 (0)

initing FirstDep: 0m0sec

19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)

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