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

Execution Outputs of marcie for Philosophers/000050 (P/T)

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

execution on node 1: quadhexa-2.u-paris10.fr (runId=136968525100161_n_1)
=====================================================================
runnning marcie on Philosophers-PT-000050 (ReachabilityMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Philosophers-PT-000050, examination is ReachabilityMix
=====================================================================

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

START 1369697687

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 250 NrTr: 250)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m6sec


RS generation: 0m0sec


-> reachability set: #nodes 1280 (1.3e+03) #states 717,897,987,691,852,588,770,249 (23)



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

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [[Catch1_30=Eat_30 & [[Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [[Catch1_22=Eat_22 & [[[Catch1_6=Eat_6 & [[[Catch1_7=Eat_7 & [[[Catch1_41=Eat_41 & [[[Catch1_39=Eat_39 & [[[Catch1_3=Eat_3 & [[[[[[Catch1_32=Eat_32 & [[[Catch1_17=Eat_17 & [[[Catch1_45=Eat_45 & [[[[[[Catch1_37=Eat_37 & [[[[[[Catch1_4=Eat_4 & [[[Catch1_20=Eat_20 & [true & Catch1_19=Eat_19]] & Catch1_2=Eat_2] & Catch1_47=Eat_47]] & Catch1_15=Eat_15] & Catch1_31=Eat_31] & Catch1_14=Eat_14] & Catch1_26=Eat_26] & Catch1_35=Eat_35]] & Catch1_12=Eat_12] & Catch1_5=Eat_5] & Catch1_46=Eat_46] & Catch1_24=Eat_24] & Catch1_33=Eat_33]] & Catch1_28=Eat_28] & Catch1_49=Eat_49]] & Catch1_34=Eat_34] & Catch1_38=Eat_38]] & Catch1_23=Eat_23] & Catch1_44=Eat_44] & Catch1_21=Eat_21] & Catch1_48=Eat_48] & Catch1_50=Eat_50]] & Catch1_9=Eat_9] & Catch1_18=Eat_18]] & Catch1_11=Eat_11] & Catch1_1=Eat_1]] & Catch1_10=Eat_10] & Catch1_36=Eat_36]] & Catch1_27=Eat_27] & Catch1_25=Eat_25]] & Catch1_13=Eat_13] & Catch1_43=Eat_43]] & Catch1_16=Eat_16]]] & Catch1_29=Eat_29]] & Catch1_42=Eat_42]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [Catch1_3=Eat_3 & [Catch1_50=Eat_50 & [Catch1_48=Eat_48 & [Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [Catch1_49=Eat_49 & [Catch1_28=Eat_28 & [Catch1_45=Eat_45 & [Catch1_33=Eat_33 & [Catch1_24=Eat_24 & [Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [Catch1_26=Eat_26 & [Catch1_14=Eat_14 & [Catch1_31=Eat_31 & [Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_37_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch1_42=Eat_42 & [[Catch1_29=Eat_29 & [[Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [[Catch1_7=Eat_7 & [[Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [[Catch1_50=Eat_50 & [[Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [[Catch1_28=Eat_28 & [[Catch1_33=Eat_33 & [Catch1_24=Eat_24 & [Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [[[[Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]] & Catch1_31=Eat_31] & Catch1_14=Eat_14] & Catch1_26=Eat_26]]]]]]]] & Catch1_45=Eat_45]] & Catch1_49=Eat_49]]]]]]]] & Catch1_48=Eat_48]] & Catch1_3=Eat_3]]]]]]]] & Catch1_36=Eat_36]] & Catch1_27=Eat_27]]]]]]]] & Catch1_8=Eat_8]] & Catch1_30=Eat_30]] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) | [Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [Catch1_3=Eat_3 & [Catch1_50=Eat_50 & [Catch1_48=Eat_48 & [Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [Catch1_49=Eat_49 & [Catch1_28=Eat_28 & [Catch1_45=Eat_45 & [Catch1_33=Eat_33 & [Catch1_24=Eat_24 & [Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [Catch1_26=Eat_26 & [Catch1_14=Eat_14 & [Catch1_31=Eat_31 & [Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_38_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [[[[[[[Catch1_13=Eat_13 & [[[[[Catch1_36=Eat_36 & [[[[[[[[[[[[[[[[[[Catch1_49=Eat_49 & [[[[[Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [Catch1_26=Eat_26 & [Catch1_14=Eat_14 & [Catch1_31=Eat_31 & [Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]]]]]]]]]] & Catch1_24=Eat_24] & Catch1_33=Eat_33] & Catch1_45=Eat_45] & Catch1_28=Eat_28]] & Catch1_17=Eat_17] & Catch1_34=Eat_34] & Catch1_38=Eat_38] & Catch1_32=Eat_32] & Catch1_23=Eat_23] & Catch1_44=Eat_44] & Catch1_21=Eat_21] & Catch1_48=Eat_48] & Catch1_50=Eat_50] & Catch1_3=Eat_3] & Catch1_9=Eat_9] & Catch1_18=Eat_18] & Catch1_39=Eat_39] & Catch1_11=Eat_11] & Catch1_1=Eat_1] & Catch1_41=Eat_41] & Catch1_10=Eat_10]] & Catch1_7=Eat_7] & Catch1_27=Eat_27] & Catch1_25=Eat_25] & Catch1_6=Eat_6]] & Catch1_43=Eat_43] & Catch1_22=Eat_22] & Catch1_16=Eat_16] & Catch1_40=Eat_40] & Catch1_8=Eat_8] & Catch1_29=Eat_29]]]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [Catch1_3=Eat_3 & [Catch1_50=Eat_50 & [Catch1_48=Eat_48 & [Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [Catch1_49=Eat_49 & [Catch1_28=Eat_28 & [Catch1_45=Eat_45 & [Catch1_33=Eat_33 & [Catch1_24=Eat_24 & [Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [Catch1_26=Eat_26 & [Catch1_14=Eat_14 & [Catch1_31=Eat_31 & [Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_39_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch1_42=Eat_42 & [[[[[Catch1_16=Eat_16 & [[[[[[[[[[Catch1_41=Eat_41 & [[[Catch1_39=Eat_39 & [[[[[[[[[[[[[[Catch1_28=Eat_28 & [[[[Catch1_46=Eat_46 & [[[Catch1_37=Eat_37 & [[[[Catch1_31=Eat_31 & [[[Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [[true & Catch1_19=Eat_19] & Catch1_20=Eat_20]]] & Catch1_4=Eat_4] & Catch1_15=Eat_15]] & Catch1_14=Eat_14] & Catch1_26=Eat_26] & Catch1_35=Eat_35]] & Catch1_12=Eat_12] & Catch1_5=Eat_5]] & Catch1_24=Eat_24] & Catch1_33=Eat_33] & Catch1_45=Eat_45]] & Catch1_49=Eat_49] & Catch1_17=Eat_17] & Catch1_34=Eat_34] & Catch1_38=Eat_38] & Catch1_32=Eat_32] & Catch1_23=Eat_23] & Catch1_44=Eat_44] & Catch1_21=Eat_21] & Catch1_48=Eat_48] & Catch1_50=Eat_50] & Catch1_3=Eat_3] & Catch1_9=Eat_9] & Catch1_18=Eat_18]] & Catch1_11=Eat_11] & Catch1_1=Eat_1]] & Catch1_10=Eat_10] & Catch1_36=Eat_36] & Catch1_7=Eat_7] & Catch1_27=Eat_27] & Catch1_25=Eat_25] & Catch1_6=Eat_6] & Catch1_13=Eat_13] & Catch1_43=Eat_43] & Catch1_22=Eat_22]] & Catch1_40=Eat_40] & Catch1_8=Eat_8] & Catch1_29=Eat_29] & Catch1_30=Eat_30]] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[[Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [[[[[[[[[Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [Catch1_49=Eat_49 & [Catch1_28=Eat_28 & [Catch1_45=Eat_45 & [Catch1_33=Eat_33 & [Catch1_24=Eat_24 & [Catch1_46=Eat_46 & [Catch1_5=Eat_5 & [Catch1_12=Eat_12 & [Catch1_37=Eat_37 & [Catch1_35=Eat_35 & [Catch1_26=Eat_26 & [Catch1_14=Eat_14 & [Catch1_31=Eat_31 & [Catch1_15=Eat_15 & [Catch1_4=Eat_4 & [Catch1_47=Eat_47 & [Catch1_2=Eat_2 & [Catch1_20=Eat_20 & [Catch1_19=Eat_19 & true]]]]]]]]]]]]]]]]]]]]]]]]]] & Catch1_48=Eat_48] & Catch1_50=Eat_50] & Catch1_3=Eat_3] & Catch1_9=Eat_9] & Catch1_18=Eat_18] & Catch1_39=Eat_39] & Catch1_11=Eat_11] & Catch1_1=Eat_1]]]]]]]]]]]]]]]]] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]]]

-> the formula is FALSE

FORMULA p_40_mix_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Catch1_30=Eat_30 & [[[[[Catch1_22=Eat_22 & [[[[Catch1_25=Eat_25 & [[[[[[[Catch1_11=Eat_11 & [[[Catch1_9=Eat_9 & [[Catch1_50=Eat_50 & [[[[[Catch1_32=Eat_32 & [[[[[[[[[[[[[[[[[[[[[[Catch1_19=Eat_19 & true] & Catch1_20=Eat_20] & Catch1_2=Eat_2] & Catch1_47=Eat_47] & Catch1_4=Eat_4] & Catch1_15=Eat_15] & Catch1_31=Eat_31] & Catch1_14=Eat_14] & Catch1_26=Eat_26] & Catch1_35=Eat_35] & Catch1_37=Eat_37] & Catch1_12=Eat_12] & Catch1_5=Eat_5] & Catch1_46=Eat_46] & Catch1_24=Eat_24] & Catch1_33=Eat_33] & Catch1_45=Eat_45] & Catch1_28=Eat_28] & Catch1_49=Eat_49] & Catch1_17=Eat_17] & Catch1_34=Eat_34] & Catch1_38=Eat_38]] & Catch1_23=Eat_23] & Catch1_44=Eat_44] & Catch1_21=Eat_21] & Catch1_48=Eat_48]] & Catch1_3=Eat_3]] & Catch1_18=Eat_18] & Catch1_39=Eat_39]] & Catch1_1=Eat_1] & Catch1_41=Eat_41] & Catch1_10=Eat_10] & Catch1_36=Eat_36] & Catch1_7=Eat_7] & Catch1_27=Eat_27]] & Catch1_6=Eat_6] & Catch1_13=Eat_13] & Catch1_43=Eat_43]] & Catch1_16=Eat_16] & Catch1_40=Eat_40] & Catch1_8=Eat_8] & Catch1_29=Eat_29]] & Catch1_42=Eat_42] <-> ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ] & ~ [[Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [Catch1_3=Eat_3 & [Catch1_50=Eat_50 & [Catch1_48=Eat_48 & [Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [[[[[[[[[[[[[[[[[[[true & Catch1_19=Eat_19] & Catch1_20=Eat_20] & Catch1_2=Eat_2] & Catch1_47=Eat_47] & Catch1_4=Eat_4] & Catch1_15=Eat_15] & Catch1_31=Eat_31] & Catch1_14=Eat_14] & Catch1_26=Eat_26] & Catch1_35=Eat_35] & Catch1_37=Eat_37] & Catch1_12=Eat_12] & Catch1_5=Eat_5] & Catch1_46=Eat_46] & Catch1_24=Eat_24] & Catch1_33=Eat_33] & Catch1_45=Eat_45] & Catch1_28=Eat_28] & Catch1_49=Eat_49]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [Catch1_42=Eat_42 & [Catch1_30=Eat_30 & [Catch1_29=Eat_29 & [Catch1_8=Eat_8 & [Catch1_40=Eat_40 & [Catch1_16=Eat_16 & [Catch1_22=Eat_22 & [Catch1_43=Eat_43 & [Catch1_13=Eat_13 & [Catch1_6=Eat_6 & [Catch1_25=Eat_25 & [Catch1_27=Eat_27 & [Catch1_7=Eat_7 & [Catch1_36=Eat_36 & [Catch1_10=Eat_10 & [Catch1_41=Eat_41 & [Catch1_1=Eat_1 & [Catch1_11=Eat_11 & [Catch1_39=Eat_39 & [Catch1_18=Eat_18 & [Catch1_9=Eat_9 & [Catch1_3=Eat_3 & [Catch1_50=Eat_50 & [Catch1_48=Eat_48 & [Catch1_21=Eat_21 & [Catch1_44=Eat_44 & [Catch1_23=Eat_23 & [Catch1_32=Eat_32 & [Catch1_38=Eat_38 & [Catch1_34=Eat_34 & [Catch1_17=Eat_17 & [[[[[[[[[[[[[[[[[[[true & Catch1_19=Eat_19] & Catch1_20=Eat_20] & Catch1_2=Eat_2] & Catch1_47=Eat_47] & Catch1_4=Eat_4] & Catch1_15=Eat_15] & Catch1_31=Eat_31] & Catch1_14=Eat_14] & Catch1_26=Eat_26] & Catch1_35=Eat_35] & Catch1_37=Eat_37] & Catch1_12=Eat_12] & Catch1_5=Eat_5] & Catch1_46=Eat_46] & Catch1_24=Eat_24] & Catch1_33=Eat_33] & Catch1_45=Eat_45] & Catch1_28=Eat_28] & Catch1_49=Eat_49]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_41_mix_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_28" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | [[["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | [[["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | [["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | [[[[[["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | [[["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | [[[["Think_8" \in [1, oo) && "Fork_7" \in [1, oo) | [["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | [["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | [[[[["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | [["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)]] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)]]] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)]] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)]]] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)]] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)]]] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)]]]]] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)]]]] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)]]]]]]]]]] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & [[[[[[[[[["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | [[[["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | [[[[["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | [["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | [[["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | [["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | [[["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | [["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]]]]] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)]] | "Think_8" \in [1, oo) && "Fork_7" \in [1, oo)]]]] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)]]] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)]]]]]] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)]] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)]]] | "Fork_3" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)]]] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Think_29" \in [1, oo) && "Fork_28" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_42_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | [[[["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_4" \in [1, oo) | [[[["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | [[[["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Think_23" \in [1, oo) && "Fork_22" \in [1, oo) | [[[["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | [[["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | [["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | [[[[[[["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | [["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | [["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)]]]]] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)]] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_19" \in [1, oo)]] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)]]] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)]]] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)]]] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)]] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)]]]]] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)]]] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) | ["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | [[[[["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | [["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | [[["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | [[["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | [["Fork_18" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | [["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | [[[[["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)]] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)]] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)]]]]]]] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)]] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)]]] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)]]]] | "Think_23" \in [1, oo) && "Fork_22" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)]]]] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)]]]] | "Fork_3" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)]]]] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)]]]]]]]]]]

-> the formula is FALSE

FORMULA p_43_mix_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m10sec

checking: AG [[[[[[[[[["Fork_9" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_39" \in [1, oo) | [[[[[[[["Fork_37" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_24" \in [1, oo) | [[[[[[["Fork_44" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_46" \in [1, oo) | [[[["Fork_35" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_47" \in [1, oo) | [[["Fork_36" \in [1, oo) && "Think_37" \in [1, oo) | ["Think_19" \in [1, oo) && "Fork_18" \in [1, oo) | [[[[[[[[[[["Fork_4" \in [1, oo) && "Think_5" \in [1, oo) | [[["Fork_5" \in [1, oo) && "Think_6" \in [1, oo) | "Fork_14" \in [1, oo) && "Think_15" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_14" \in [1, oo)]] | "Fork_12" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_22" \in [1, oo)] | "Fork_32" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_26" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_50" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_1" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_32" \in [1, oo)]]] | "Fork_17" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_11" \in [1, oo)]]] | "Fork_24" \in [1, oo) && "Think_25" \in [1, oo)] | "Think_1" \in [1, oo) && "Fork_50" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_31" \in [1, oo)]]] | "Fork_48" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_9" \in [1, oo)]]] | "Fork_39" \in [1, oo) && "Think_40" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_4" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_30" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_28" \in [1, oo)]]] | "Think_17" \in [1, oo) && "Fork_16" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_15" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_35" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_34" \in [1, oo)] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_18 + Fork_7 ) + Fork_4 ) + Fork_26 ) + Fork_48 ) + Fork_46 ) + Fork_39 ) + Fork_43 ) + Fork_28 ) + Fork_33 ) + Fork_6 ) + Fork_11 ) + Fork_35 ) + Fork_50 ) + Fork_34 ) + Fork_20 ) + Fork_24 ) + Fork_10 ) + Fork_49 ) + Fork_12 ) + Fork_22 ) + Fork_37 ) + Fork_45 ) + Fork_8 ) + Fork_19 ) + Fork_1 ) + Fork_25 ) + Fork_9 ) + Fork_36 ) + Fork_29 ) + Fork_27 ) + Fork_30 ) + Fork_17 ) + Fork_3 ) + Fork_41 ) + Fork_38 ) + Fork_44 ) + Fork_42 ) + Fork_32 ) + Fork_21 ) + Fork_31 ) + Fork_2 ) + Fork_14 ) + Fork_15 ) + Fork_40 ) + Fork_13 ) + Fork_16 ) + Fork_47 ) + Fork_5 ) + Fork_23 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_28 + Eat_14 ) + Eat_24 ) + Eat_22 ) + Eat_2 ) + Eat_13 ) + Eat_17 ) + Eat_15 ) + Eat_4 ) + Eat_49 ) + Eat_43 ) + Eat_31 ) + Eat_37 ) + Eat_46 ) + Eat_35 ) + Eat_5 ) + Eat_25 ) + Eat_8 ) + Eat_29 ) + Eat_30 ) + Eat_33 ) + Eat_21 ) + Eat_20 ) + Eat_1 ) + Eat_32 ) + Eat_38 ) + Eat_47 ) + Eat_34 ) + Eat_48 ) + Eat_11 ) + Eat_19 ) + Eat_12 ) + Eat_40 ) + Eat_6 ) + Eat_18 ) + Eat_26 ) + Eat_41 ) + Eat_39 ) + Eat_42 ) + Eat_7 ) + Eat_27 ) + Eat_45 ) + Eat_36 ) + Eat_9 ) + Eat_44 ) + Eat_3 ) + Eat_10 ) + Eat_23 ) + Eat_50 ) + Eat_16 ) & ["Fork_33" \in [1, oo) && "Think_34" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_29" \in [1, oo) | ["Think_16" \in [1, oo) && "Fork_15" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_16" \in [1, oo) | [[["Fork_27" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_4" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_40" \in [1, oo) | [[["Fork_8" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_49" \in [1, oo) | [[["Fork_30" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_1" \in [1, oo) && "Fork_50" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_25" \in [1, oo) | [[["Fork_10" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_17" \in [1, oo) && "Think_18" \in [1, oo) | [[["Fork_31" \in [1, oo) && "Think_32" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_41" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_1" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_3" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_15" \in [1, oo) | "Fork_5" \in [1, oo) && "Think_6" \in [1, oo)]]] | "Fork_4" \in [1, oo) && "Think_5" \in [1, oo)]]]]]]]]]]] | "Think_19" \in [1, oo) && "Fork_18" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_37" \in [1, oo)]]] | "Fork_46" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_36" \in [1, oo)]]]] | "Fork_45" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_45" \in [1, oo)]]]]]]] | "Fork_23" \in [1, oo) && "Think_24" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_38" \in [1, oo)]]]]]]]] | "Fork_38" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_9" \in [1, oo) && "Think_10" \in [1, oo)]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_44_mix_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m18sec

STOP 1369697706

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

1274
iterations count:1143 (4), effective:150 (0)

initing FirstDep: 0m0sec


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

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

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

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

iterations count:250 (1), effective:0 (0)
1608 1551 1484 1543 1540 1537 1532 1532 1530 1450 1498 1476 1374 1520
iterations count:14608 (58), effective:2496 (9)

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

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