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=ReachabilityPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1660
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 ReachabilityPlaceComparison'
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 25: cluster1u27.lip6.fr (runId=136959876501478_n_25)
=====================================================================
runnning marcie on NeoElection-PT-2 (ReachabilityPlaceComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is NeoElection-PT-2, examination is ReachabilityPlaceComparison
=====================================================================

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

START 1369647772

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


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

-> the formula is FALSE

FORMULA p_7_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is FALSE

FORMULA p_8_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is FALSE

FORMULA p_9_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is TRUE

FORMULA p_10_placecomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is TRUE

FORMULA p_11_placecomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[true & electionFailed_2!=electedPrimary_2] & electionFailed_0!=electedPrimary_0] & electionFailed_1!=electedPrimary_1] & [[true & [[[true & dead_1>electedPrimary_1] & dead_2>electedPrimary_2] & dead_0>electedPrimary_0]] & [[[[false | dead_1>electedPrimary_1] | dead_2>electedPrimary_2] | dead_0>electedPrimary_0] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [dead_0>electedPrimary_0 | [dead_2>electedPrimary_2 | [dead_1>electedPrimary_1 | false]]]] & [[dead_0>electedPrimary_0 & [dead_2>electedPrimary_2 & [dead_1>electedPrimary_1 & true]]] & true]] & [electionFailed_1!=electedPrimary_1 & [electionFailed_0!=electedPrimary_0 & [electionFailed_2!=electedPrimary_2 & true]]]]]]]

-> the formula is FALSE

FORMULA p_12_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[true & electionFailed_2!=electedPrimary_2] & electionFailed_0!=electedPrimary_0] & electionFailed_1!=electedPrimary_1] | [[true & [[[true & dead_1>electedPrimary_1] & dead_2>electedPrimary_2] & dead_0>electedPrimary_0]] & [[[[false | dead_1>electedPrimary_1] | dead_2>electedPrimary_2] | dead_0>electedPrimary_0] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [dead_0>electedPrimary_0 | [dead_2>electedPrimary_2 | [dead_1>electedPrimary_1 | false]]]] & [[dead_0>electedPrimary_0 & [dead_2>electedPrimary_2 & [dead_1>electedPrimary_1 & true]]] & true]] | [electionFailed_1!=electedPrimary_1 & [electionFailed_0!=electedPrimary_0 & [electionFailed_2!=electedPrimary_2 & true]]]]]]]

-> the formula is FALSE

FORMULA p_13_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[true & electionFailed_2!=electedPrimary_2] & electionFailed_0!=electedPrimary_0] & electionFailed_1!=electedPrimary_1] & [[true & [[[true & dead_1>electedPrimary_1] & dead_2>electedPrimary_2] & dead_0>electedPrimary_0]] & [[[[false | dead_1>electedPrimary_1] | dead_2>electedPrimary_2] | dead_0>electedPrimary_0] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [dead_0>electedPrimary_0 | [dead_2>electedPrimary_2 | [dead_1>electedPrimary_1 | false]]]] & [[dead_0>electedPrimary_0 & [dead_2>electedPrimary_2 & [dead_1>electedPrimary_1 & true]]] & true]] & [electionFailed_1!=electedPrimary_1 & [electionFailed_0!=electedPrimary_0 & [electionFailed_2!=electedPrimary_2 & true]]]]]]]

-> the formula is FALSE

FORMULA p_14_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m2sec

STOP 1369647775

--------------------
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.1660: