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-2
export BK_EXAMINATION=ReachabilityCardinalityComparison
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-2
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is NeoElection-PT-2, examination is ReachabilityCardinalityComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for NeoElection/2 (P/T)

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

execution on node 39: cluster1u41.lip6.fr (runId=136959876601492_n_39)
=====================================================================
runnning marcie on NeoElection-PT-2 (ReachabilityCardinalityComparison)
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-2, examination is ReachabilityCardinalityComparison
=====================================================================

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

START 1369651164

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 438 NrTr: 357)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m0sec


-> reachability set: #nodes 1806 (1.8e+03) #states 241



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

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]]

-> the formula is FALSE

FORMULA p_17_cardinalitycomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) | ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) | ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]]

-> the formula is FALSE

FORMULA p_18_cardinalitycomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) ] & ~ [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]
normalized: ~ [E [true U ~ [[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) ] & ~ [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]]]

-> the formula is TRUE

FORMULA p_19_cardinalitycomparison_eq_and_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) ] | ~ [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]
normalized: ~ [E [true U ~ [[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) ] | ~ [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]]]]

-> the formula is TRUE

FORMULA p_20_cardinalitycomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) xor ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]]
normalized: ~ [E [true U ~ [[[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ~ [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) ]] | [ ( ( electedSecondary_0 + electedSecondary_2 ) + electedSecondary_1 ) != ( ( poll__waitingMessage_2 + poll__waitingMessage_1 ) + poll__waitingMessage_0 ) & ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) != ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) ]]]]]]

-> the formula is FALSE

FORMULA p_21_cardinalitycomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]]]

-> the formula is FALSE

FORMULA p_22_cardinalitycomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) | ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) | ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]]]

-> the formula is FALSE

FORMULA p_23_cardinalitycomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ~ [ ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( poll__networl_2_0_AnsP_1 + poll__networl_1_2_AnnP_2 ) + poll__networl_1_0_RP_1 ) + poll__networl_2_1_RP_1 ) + poll__networl_0_0_AnsP_1 ) + poll__networl_2_0_AnnP_0 ) + poll__networl_2_0_AI_0 ) + poll__networl_1_1_AI_0 ) + poll__networl_1_0_AnnP_2 ) + poll__networl_2_1_AskP_1 ) + poll__networl_0_1_AskP_0 ) + poll__networl_2_2_RI_1 ) + poll__networl_0_0_AnsP_2 ) + poll__networl_2_2_AI_2 ) + poll__networl_2_1_RP_0 ) + poll__networl_1_2_AskP_0 ) + poll__networl_1_1_AskP_1 ) + poll__networl_0_1_AnsP_2 ) + poll__networl_1_2_RI_1 ) + poll__networl_0_2_AI_1 ) + poll__networl_1_1_AI_1 ) + poll__networl_1_2_AnnP_1 ) + poll__networl_0_2_AskP_0 ) + poll__networl_0_0_RI_2 ) + poll__networl_1_1_AnsP_0 ) + poll__networl_1_0_RP_2 ) + poll__networl_0_1_AnnP_1 ) + poll__networl_2_1_AnnP_2 ) + poll__networl_1_2_AskP_1 ) + poll__networl_0_2_AskP_1 ) + poll__networl_1_2_AnsP_1 ) + poll__networl_0_1_AskP_2 ) + poll__networl_2_2_AskP_0 ) + poll__networl_2_0_AI_1 ) + poll__networl_1_0_RP_0 ) + poll__networl_0_2_AI_2 ) + poll__networl_2_1_AnsP_1 ) + poll__networl_1_0_AskP_1 ) + poll__networl_1_0_AskP_2 ) + poll__networl_1_2_RI_0 ) + poll__networl_0_2_RP_2 ) + poll__networl_0_1_RI_1 ) + poll__networl_0_1_AI_2 ) + poll__networl_1_0_AnnP_0 ) + poll__networl_1_2_AnnP_0 ) + poll__networl_2_2_AnnP_2 ) + poll__networl_2_0_RP_2 ) + poll__networl_2_2_AnsP_1 ) + poll__networl_2_1_AskP_0 ) + poll__networl_0_1_RP_0 ) + poll__networl_1_0_AnsP_1 ) + poll__networl_1_2_RP_0 ) + poll__networl_2_0_RP_0 ) + poll__networl_2_2_AI_0 ) + poll__networl_1_2_AI_0 ) + poll__networl_0_1_AnsP_0 ) + poll__networl_0_0_AI_0 ) + poll__networl_1_1_RI_2 ) + poll__networl_0_0_RP_0 ) + poll__networl_1_0_RI_2 ) + poll__networl_1_2_RI_2 ) + poll__networl_1_0_AskP_0 ) + poll__networl_2_2_RI_2 ) + poll__networl_0_0_AI_1 ) + poll__networl_1_1_RP_1 ) + poll__networl_1_0_AnsP_0 ) + poll__networl_2_1_AskP_2 ) + poll__networl_1_0_AI_2 ) + poll__networl_0_1_RI_2 ) + poll__networl_0_2_AnsP_2 ) + poll__networl_1_1_AnnP_0 ) + poll__networl_0_0_RI_1 ) + poll__networl_2_0_AskP_0 ) + poll__networl_2_1_AI_0 ) + poll__networl_1_1_RP_2 ) + poll__networl_1_2_RP_2 ) + poll__networl_2_1_AI_2 ) + poll__networl_0_2_AnnP_2 ) + poll__networl_0_0_AI_2 ) + poll__networl_0_1_AI_1 ) + poll__networl_2_0_RI_1 ) + poll__networl_0_1_AnsP_1 ) + poll__networl_0_0_RP_1 ) + poll__networl_2_2_RI_0 ) + poll__networl_0_1_RP_1 ) + poll__networl_0_2_AnnP_1 ) + poll__networl_2_0_AnsP_0 ) + poll__networl_0_0_AskP_2 ) + poll__networl_1_0_AnnP_1 ) + poll__networl_2_0_RI_0 ) + poll__networl_0_0_RI_0 ) + poll__networl_1_2_AnsP_2 ) + poll__networl_2_0_RI_2 ) + poll__networl_0_2_RI_2 ) + poll__networl_1_1_AnsP_1 ) + poll__networl_1_1_AI_2 ) + poll__networl_0_0_RP_2 ) + poll__networl_0_1_AnnP_2 ) + poll__networl_0_1_RP_2 ) + poll__networl_0_0_AnnP_0 ) + poll__networl_1_1_RP_0 ) + poll__networl_0_0_AskP_1 ) + poll__networl_2_2_RP_2 ) + poll__networl_1_0_RI_0 ) + poll__networl_2_0_AI_2 ) + poll__networl_2_2_AnnP_0 ) + poll__networl_0_2_RP_1 ) + poll__networl_2_1_AI_1 ) + poll__networl_1_1_AnnP_1 ) + poll__networl_2_1_RI_1 ) + poll__networl_1_1_RI_1 ) + poll__networl_0_2_AnsP_0 ) + poll__networl_0_0_AnsP_0 ) + poll__networl_2_1_RP_2 ) + poll__networl_2_2_AskP_1 ) + poll__networl_0_2_RP_0 ) + poll__networl_0_2_AnnP_0 ) + poll__networl_1_0_AnsP_2 ) + poll__networl_1_2_AnsP_0 ) + poll__networl_2_0_AnnP_2 ) + poll__networl_2_2_AnsP_2 ) + poll__networl_2_0_AnnP_1 ) + poll__networl_0_1_AnnP_0 ) + poll__networl_2_1_AnsP_0 ) + poll__networl_0_2_AnsP_1 ) + poll__networl_0_2_AI_0 ) + poll__networl_1_2_AskP_2 ) + poll__networl_2_2_AskP_2 ) + poll__networl_0_1_AI_0 ) + poll__networl_2_1_AnnP_1 ) + poll__networl_0_1_AskP_1 ) + poll__networl_1_1_AnnP_2 ) + poll__networl_1_0_RI_1 ) + poll__networl_2_2_RP_0 ) + poll__networl_1_2_AI_2 ) + poll__networl_2_1_AnnP_0 ) + poll__networl_2_2_AnnP_1 ) + poll__networl_1_2_AI_1 ) + poll__networl_0_2_AskP_2 ) + poll__networl_0_2_RI_0 ) + poll__networl_0_0_AnnP_1 ) + poll__networl_2_0_AnsP_2 ) + poll__networl_0_1_RI_0 ) + poll__networl_2_1_RI_2 ) + poll__networl_2_0_AskP_1 ) + poll__networl_1_0_AI_1 ) + poll__networl_1_1_AnsP_2 ) + poll__networl_1_1_AskP_0 ) + poll__networl_2_0_RP_1 ) + poll__networl_2_2_AnsP_0 ) + poll__networl_1_1_RI_0 ) + poll__networl_2_1_AnsP_2 ) + poll__networl_2_2_AI_1 ) + poll__networl_2_0_AskP_2 ) + poll__networl_0_0_AskP_0 ) + poll__networl_1_1_AskP_2 ) + poll__networl_2_2_RP_1 ) + poll__networl_2_1_RI_0 ) + poll__networl_1_2_RP_1 ) + poll__networl_0_0_AnnP_2 ) + poll__networl_1_0_AI_0 ) + poll__networl_0_2_RI_1 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( network_0_0_RI_0 + network_2_1_AnsP_0 ) + network_2_1_RI_2 ) + network_0_0_AnsP_2 ) + network_0_0_AskP_2 ) + network_1_1_AnsP_1 ) + network_0_1_AnsP_0 ) + network_0_0_RP_0 ) + network_0_0_RP_1 ) + network_1_2_RP_0 ) + network_2_1_RP_0 ) + network_1_0_AI_2 ) + network_0_1_AnnP_0 ) + network_0_1_AskP_1 ) + network_2_0_AI_0 ) + network_2_0_AI_2 ) + network_1_0_RP_2 ) + network_2_2_AI_1 ) + network_1_1_RI_1 ) + network_1_2_RI_2 ) + network_1_0_AI_0 ) + network_0_2_AnnP_0 ) + network_0_2_AnsP_1 ) + network_1_2_AnnP_2 ) + network_1_1_AskP_0 ) + network_0_0_AnnP_2 ) + network_0_1_AI_1 ) + network_0_1_RI_1 ) + network_1_0_AskP_2 ) + network_1_0_RP_1 ) + network_1_2_RI_0 ) + network_2_0_RP_1 ) + network_1_1_RP_0 ) + network_1_2_AI_1 ) + network_1_0_AnnP_2 ) + network_0_1_AnsP_1 ) + network_1_2_AskP_0 ) + network_2_0_RI_0 ) + network_0_2_AI_0 ) + network_0_0_AskP_0 ) + network_2_0_AnsP_1 ) + network_0_2_RP_0 ) + network_2_1_AnnP_0 ) + network_2_2_AI_2 ) + network_2_1_AskP_1 ) + network_2_0_AskP_1 ) + network_0_1_RP_2 ) + network_1_1_AI_0 ) + network_0_2_RI_2 ) + network_2_0_AnsP_2 ) + network_0_1_AI_0 ) + network_0_2_AnsP_2 ) + network_1_1_RI_2 ) + network_0_0_AI_1 ) + network_2_1_AI_0 ) + network_2_1_AI_2 ) + network_1_0_AnnP_1 ) + network_2_2_AnnP_1 ) + network_1_1_RP_1 ) + network_1_1_AI_2 ) + network_2_1_AnnP_1 ) + network_1_2_AnsP_0 ) + network_1_0_RI_1 ) + network_2_1_AskP_2 ) + network_2_0_AnnP_0 ) + network_0_1_RI_0 ) + network_1_1_RI_0 ) + network_1_0_RI_0 ) + network_2_0_AskP_0 ) + network_0_1_AnsP_2 ) + network_0_0_AnnP_0 ) + network_1_0_AskP_1 ) + network_0_0_AskP_1 ) + network_0_2_RI_0 ) + network_2_1_RI_0 ) + network_2_2_RP_0 ) + network_0_1_AI_2 ) + network_2_1_AskP_0 ) + network_2_0_RI_1 ) + network_1_1_AskP_2 ) + network_1_2_AskP_1 ) + network_0_1_RP_0 ) + network_2_2_RI_2 ) + network_1_0_AI_1 ) + network_0_1_AnnP_2 ) + network_2_2_AskP_2 ) + network_2_2_AnsP_1 ) + network_1_1_AI_1 ) + network_0_2_RP_1 ) + network_2_2_AnsP_0 ) + network_0_2_RP_2 ) + network_1_2_AnsP_1 ) + network_2_2_AnnP_2 ) + network_1_0_AnsP_1 ) + network_2_1_RP_2 ) + network_0_0_AI_0 ) + network_2_2_AI_0 ) + network_1_1_AskP_1 ) + network_0_2_AskP_1 ) + network_0_2_AnnP_2 ) + network_0_2_AskP_2 ) + network_2_0_AskP_2 ) + network_1_2_AI_0 ) + network_0_0_RI_2 ) + network_0_0_RP_2 ) + network_2_2_AskP_1 ) + network_0_0_RI_1 ) + network_1_1_AnsP_2 ) + network_1_2_AI_2 ) + network_2_0_AnsP_0 ) + network_2_1_RP_1 ) + network_0_1_AnnP_1 ) + network_0_1_AskP_2 ) + network_1_1_AnsP_0 ) + network_2_2_RP_1 ) + network_1_0_RP_0 ) + network_2_2_RI_1 ) + network_1_2_RP_1 ) + network_1_0_RI_2 ) + network_2_1_AnsP_1 ) + network_1_1_RP_2 ) + network_0_2_AI_1 ) + network_0_2_RI_1 ) + network_0_0_AnnP_1 ) + network_2_2_AnnP_0 ) + network_2_2_AskP_0 ) + network_1_0_AnsP_2 ) + network_0_0_AI_2 ) + network_1_1_AnnP_1 ) + network_2_2_RP_2 ) + network_1_0_AskP_0 ) + network_0_2_AI_2 ) + network_2_1_AI_1 ) + network_1_2_RI_1 ) + network_2_2_AnsP_2 ) + network_2_2_RI_0 ) + network_2_0_RI_2 ) + network_2_0_RP_0 ) + network_2_1_RI_1 ) + network_0_2_AskP_0 ) + network_0_2_AnsP_0 ) + network_2_0_RP_2 ) + network_0_1_RP_1 ) + network_1_0_AnsP_0 ) + network_1_1_AnnP_0 ) + network_2_0_AnnP_1 ) + network_1_2_AskP_2 ) + network_2_0_AnnP_2 ) + network_0_0_AnsP_1 ) + network_1_1_AnnP_2 ) + network_1_0_AnnP_0 ) + network_2_1_AnnP_2 ) + network_0_2_AnnP_1 ) + network_2_0_AI_1 ) + network_0_1_AskP_0 ) + network_1_2_AnnP_0 ) + network_1_2_RP_2 ) + network_2_1_AnsP_2 ) + network_0_1_RI_2 ) + network_1_2_AnnP_1 ) + network_0_0_AnsP_0 ) + network_1_2_AnsP_2 ) & ~ [ ( ( ( ( ( sendAnnPs__broadcasting_0_1 + sendAnnPs__broadcasting_1_2 ) + sendAnnPs__broadcasting_2_2 ) + sendAnnPs__broadcasting_2_1 ) + sendAnnPs__broadcasting_1_1 ) + sendAnnPs__broadcasting_0_2 ) != ( ( ( ( ( startNeg__broadcasting_0_2 + startNeg__broadcasting_1_2 ) + startNeg__broadcasting_2_2 ) + startNeg__broadcasting_2_1 ) + startNeg__broadcasting_0_1 ) + startNeg__broadcasting_1_1 ) ]]]]]

-> the formula is FALSE

FORMULA p_24_cardinalitycomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m2sec

STOP 1369651167

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

1493 1806
iterations count:2309 (6), effective:32 (0)

initing FirstDep: 0m0sec


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

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

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

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

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

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

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