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

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

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

START 1371120479

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 270 NrTr: 116)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m6sec


RS generation: 0m39sec


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



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

checking: AG [[ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]]]

-> the formula is FALSE

FORMULA p_1856_cardinalitycomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m36sec

checking: AF [[ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]
normalized: ~ [EG [~ [[ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1857_cardinalitycomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[~ [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]
normalized: ~ [EG [~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & ~ [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1858_cardinalitycomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) | ~ [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ]]]]]

-> the formula is TRUE

FORMULA p_1859_cardinalitycomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [AG [[EG [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) ]]]
normalized: ~ [E [true U E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n7_2_0 + n7_3_6 ) + n7_1_0 ) + n7_2_5 ) + n7_3_4 ) + n7_6_3 ) + n7_4_1 ) + n7_2_1 ) + n7_6_1 ) + n7_5_0 ) + n7_3_5 ) + n7_4_6 ) + n7_4_3 ) + n7_2_3 ) + n7_0_0 ) + n7_4_4 ) + n7_5_2 ) + n7_5_3 ) + n7_2_4 ) + n7_1_1 ) + n7_5_1 ) + n7_1_3 ) + n7_0_4 ) + n7_1_6 ) + n7_4_5 ) + n7_5_6 ) + n7_2_6 ) + n7_6_6 ) + n7_3_1 ) + n7_6_0 ) + n7_6_5 ) + n7_3_2 ) + n7_1_4 ) + n7_3_3 ) + n7_4_2 ) + n7_0_6 ) + n7_2_2 ) + n7_4_0 ) + n7_0_3 ) + n7_0_1 ) + n7_1_5 ) + n7_5_4 ) + n7_0_2 ) + n7_5_5 ) + n7_6_2 ) + n7_3_0 ) + n7_0_5 ) + n7_1_2 ) + n7_6_4 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & EG [ ( ( ( ( ( ( c1_3 + c1_0 ) + c1_6 ) + c1_1 ) + c1_4 ) + c1_5 ) + c1_2 ) != ( ( ( ( ( ( n5_4 + n5_0 ) + n5_6 ) + n5_3 ) + n5_1 ) + n5_2 ) + n5_5 ) ]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1860_cardinalitycomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1861_cardinalitycomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1862_cardinalitycomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n9_3_1 + n9_4_3 ) + n9_3_3 ) + n9_4_4 ) + n9_0_0 ) + n9_5_3 ) + n9_1_5 ) + n9_2_2 ) + n9_6_1 ) + n9_5_1 ) + n9_1_0 ) + n9_1_6 ) + n9_2_5 ) + n9_4_2 ) + n9_0_3 ) + n9_3_4 ) + n9_4_6 ) + n9_0_5 ) + n9_5_2 ) + n9_1_3 ) + n9_6_2 ) + n9_6_3 ) + n9_1_1 ) + n9_0_2 ) + n9_3_0 ) + n9_5_4 ) + n9_4_0 ) + n9_5_0 ) + n9_2_1 ) + n9_6_5 ) + n9_3_2 ) + n9_0_4 ) + n9_0_1 ) + n9_5_5 ) + n9_3_6 ) + n9_4_1 ) + n9_4_5 ) + n9_2_6 ) + n9_5_6 ) + n9_3_5 ) + n9_6_4 ) + n9_2_0 ) + n9_1_4 ) + n9_1_2 ) + n9_2_3 ) + n9_6_6 ) + n9_2_4 ) + n9_0_6 ) + n9_6_0 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( n8_2_1 + n8_4_0 ) + n8_0_0 ) + n8_2_5 ) + n8_4_6 ) + n8_2_6 ) + n8_0_5 ) + n8_3_0 ) + n8_3_4 ) + n8_0_3 ) + n8_3_3 ) + n8_5_6 ) + n8_3_1 ) + n8_6_5 ) + n8_2_0 ) + n8_0_2 ) + n8_6_6 ) + n8_1_4 ) + n8_0_4 ) + n8_5_4 ) + n8_4_4 ) + n8_6_3 ) + n8_2_4 ) + n8_1_1 ) + n8_4_1 ) + n8_0_1 ) + n8_0_6 ) + n8_6_1 ) + n8_6_4 ) + n8_2_2 ) + n8_6_2 ) + n8_3_6 ) + n8_6_0 ) + n8_1_3 ) + n8_1_5 ) + n8_1_0 ) + n8_4_3 ) + n8_4_2 ) + n8_5_5 ) + n8_4_5 ) + n8_3_5 ) + n8_3_2 ) + n8_5_0 ) + n8_5_2 ) + n8_1_2 ) + n8_5_1 ) + n8_2_3 ) + n8_5_3 ) + n8_1_6 ) ]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1863_cardinalitycomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 2m13sec

STOP 1371120613

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

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