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=CTLMix
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
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 CTLMix'
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=136968525800281_n_1)
=====================================================================
runnning marcie on Philosophers-PT-000050 (CTLMix)
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 CTLMix
=====================================================================

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

START 1369708136

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=CTLMix.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: AF [[["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[["Think_46" \in [1, oo) && "Fork_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]]
normalized: ~ [EG [~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) & ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Think_28" \in [1, oo) && "Fork_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Think_21" \in [1, oo) && "Fork_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Think_43" \in [1, oo) && "Fork_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Think_29" \in [1, oo) && "Fork_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Think_49" \in [1, oo) && "Fork_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Think_18" \in [1, oo) && "Fork_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Think_35" \in [1, oo) && "Fork_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[["Think_46" \in [1, oo) && "Fork_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1876_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Think_26" \in [1, oo) && "Fork_26" \in [1, oo) | [["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | [[["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [[[["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | [[["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | [[[["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]]]]]]]]]]]]]]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)]] | "Think_42" \in [1, oo) && "Fork_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)]] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)]]]]] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)]]] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)]] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)]]]] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]]
normalized: ~ [EG [~ [[[[[[[[[[[[[[[[[[[[[[[[[[[["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | [[[["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Think_37" \in [1, oo) && "Fork_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]]] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]]]]]]]]]]]]]]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)]] | "Think_42" \in [1, oo) && "Fork_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Think_26" \in [1, oo) && "Fork_26" \in [1, oo)] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]]]]

..........................
EG iterations: 26
-> the formula is TRUE

FORMULA p_1877_mix_eq_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m9sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) & [[[[["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | [["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [[["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | [[["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [[["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | [[[[[["Think_8" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Think_44" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [[[["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | [[["Think_14" \in [1, oo) && "Fork_14" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)]] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)]] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]]]]]]]] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)]] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)]]]] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)]] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) & ["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | ["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | ["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | ["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | ["Fork_3" \in [1, oo) && "Think_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | ["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | [["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Think_8" \in [1, oo) && "Fork_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | ["Think_44" \in [1, oo) && "Fork_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | ["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | ["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | [["Think_14" \in [1, oo) && "Fork_14" \in [1, oo) | [[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | [[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)]]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)]] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1878_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | [[[["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | [[["Fork_41" \in [1, oo) && "Think_41" \in [1, oo) | ["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | ["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | [["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | [["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | ["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | [[[[[["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Think_47" \in [1, oo) && "Fork_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | [[["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [[["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | ["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | [[[["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | [["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)] | "Fork_24" \in [1, oo) && "Think_24" \in [1, oo)]]]]]] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)]]]]]]]] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)]]]] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)]]] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)]]] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)]]]] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)]] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]]
normalized: EG [[[[[[[[["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | [[[["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | [[["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | [[["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | ["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | [[[["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | ["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | [["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | [["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | ["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [[[[[[[["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | ["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | [[[[[["Fork_24" \in [1, oo) && "Think_24" \in [1, oo) | ["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)]] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)]]]] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)]]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)]]] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Think_47" \in [1, oo) && "Fork_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)]]]]]] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)]] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)]] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)] | "Fork_41" \in [1, oo) && "Think_41" \in [1, oo)]] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)] | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]]

..
EG iterations: 2
-> the formula is TRUE

FORMULA p_1879_mix_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [A [AG [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ] U AF [["Think_16" \in [1, oo) && "Fork_16" \in [1, oo) | [["Fork_28" \in [1, oo) && "Think_28" \in [1, oo) | [["Think_3" \in [1, oo) && "Fork_3" \in [1, oo) | ["Fork_30" \in [1, oo) && "Think_30" \in [1, oo) | ["Fork_31" \in [1, oo) && "Think_31" \in [1, oo) | ["Think_41" \in [1, oo) && "Fork_41" \in [1, oo) | [["Fork_21" \in [1, oo) && "Think_21" \in [1, oo) | [[[[[["Fork_36" \in [1, oo) && "Think_36" \in [1, oo) | ["Fork_29" \in [1, oo) && "Think_29" \in [1, oo) | ["Fork_11" \in [1, oo) && "Think_11" \in [1, oo) | ["Fork_49" \in [1, oo) && "Think_49" \in [1, oo) | [[[[[[["Fork_18" \in [1, oo) && "Think_18" \in [1, oo) | ["Fork_10" \in [1, oo) && "Think_10" \in [1, oo) | [[[["Fork_35" \in [1, oo) && "Think_35" \in [1, oo) | [["Fork_20" \in [1, oo) && "Think_20" \in [1, oo) | [[[[[[[["Fork_27" \in [1, oo) && "Think_27" \in [1, oo) | ["Fork_48" \in [1, oo) && "Think_48" \in [1, oo) | ["Fork_46" \in [1, oo) && "Think_46" \in [1, oo) | ["Fork_33" \in [1, oo) && "Think_33" \in [1, oo) | ["Fork_12" \in [1, oo) && "Think_12" \in [1, oo) | ["Fork_19" \in [1, oo) && "Think_19" \in [1, oo) | ["Fork_25" \in [1, oo) && "Think_25" \in [1, oo) | ["Think_24" \in [1, oo) && "Fork_24" \in [1, oo) | ["Fork_32" \in [1, oo) && "Think_32" \in [1, oo) | "Fork_1" \in [1, oo) && "Think_1" \in [1, oo)]]]]]]]]] | "Fork_7" \in [1, oo) && "Think_7" \in [1, oo)] | "Fork_38" \in [1, oo) && "Think_38" \in [1, oo)] | "Think_17" \in [1, oo) && "Fork_17" \in [1, oo)] | "Fork_14" \in [1, oo) && "Think_14" \in [1, oo)] | "Fork_15" \in [1, oo) && "Think_15" \in [1, oo)] | "Fork_37" \in [1, oo) && "Think_37" \in [1, oo)] | "Fork_5" \in [1, oo) && "Think_5" \in [1, oo)]] | "Fork_13" \in [1, oo) && "Think_13" \in [1, oo)]] | "Fork_9" \in [1, oo) && "Think_9" \in [1, oo)] | "Fork_4" \in [1, oo) && "Think_4" \in [1, oo)] | "Fork_44" \in [1, oo) && "Think_44" \in [1, oo)]]] | "Fork_42" \in [1, oo) && "Think_42" \in [1, oo)] | "Fork_8" \in [1, oo) && "Think_8" \in [1, oo)] | "Fork_47" \in [1, oo) && "Think_47" \in [1, oo)] | "Fork_40" \in [1, oo) && "Think_40" \in [1, oo)] | "Think_2" \in [1, oo) && "Fork_2" \in [1, oo)] | "Fork_34" \in [1, oo) && "Think_34" \in [1, oo)]]]]] | "Fork_39" \in [1, oo) && "Think_39" \in [1, oo)] | "Fork_6" \in [1, oo) && "Think_6" \in [1, oo)] | "Fork_45" \in [1, oo) && "Think_45" \in [1, oo)] | "Fork_43" \in [1, oo) && "Think_43" \in [1, oo)] | "Fork_26" \in [1, oo) && "Think_26" \in [1, oo)]] | "Fork_50" \in [1, oo) && "Think_50" \in [1, oo)]]]]] | "Fork_23" \in [1, oo) && "Think_23" \in [1, oo)]] | "Fork_22" \in [1, oo) && "Think_22" \in [1, oo)]]]]]
normalized: EG [[~ [EG [EG [~ [[["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | [["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | [[[[["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | [["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [[[[["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[[[[[[[["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]]]]]]]] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]]]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)]]]]]]] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]]]]]] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)]] | "Think_41" \in [1, oo) && "Fork_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)]] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)]] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]]]]] & ~ [E [E [true U ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]] U [E [true U ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_37 + Think_20 ) + Think_44 ) + Think_16 ) + Think_49 ) + Think_27 ) + Think_32 ) + Think_15 ) + Think_12 ) + Think_3 ) + Think_38 ) + Think_30 ) + Think_31 ) + Think_43 ) + Think_1 ) + Think_2 ) + Think_35 ) + Think_9 ) + Think_17 ) + Think_8 ) + Think_34 ) + Think_24 ) + Think_28 ) + Think_29 ) + Think_5 ) + Think_48 ) + Think_45 ) + Think_40 ) + Think_47 ) + Think_19 ) + Think_42 ) + Think_33 ) + Think_26 ) + Think_18 ) + Think_41 ) + Think_36 ) + Think_39 ) + Think_4 ) + Think_46 ) + Think_25 ) + Think_50 ) + Think_7 ) + Think_10 ) + Think_23 ) + Think_13 ) + Think_11 ) + Think_21 ) + Think_14 ) + Think_22 ) + Think_6 ) = ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) ]] & EG [~ [[["Fork_22" \in [1, oo) && "Think_22" \in [1, oo) | [["Fork_23" \in [1, oo) && "Think_23" \in [1, oo) | [[[[["Fork_50" \in [1, oo) && "Think_50" \in [1, oo) | [["Fork_26" \in [1, oo) && "Think_26" \in [1, oo) | ["Fork_43" \in [1, oo) && "Think_43" \in [1, oo) | ["Fork_45" \in [1, oo) && "Think_45" \in [1, oo) | ["Fork_6" \in [1, oo) && "Think_6" \in [1, oo) | ["Fork_39" \in [1, oo) && "Think_39" \in [1, oo) | [[[[["Fork_34" \in [1, oo) && "Think_34" \in [1, oo) | ["Think_2" \in [1, oo) && "Fork_2" \in [1, oo) | ["Fork_40" \in [1, oo) && "Think_40" \in [1, oo) | ["Fork_47" \in [1, oo) && "Think_47" \in [1, oo) | ["Fork_8" \in [1, oo) && "Think_8" \in [1, oo) | ["Fork_42" \in [1, oo) && "Think_42" \in [1, oo) | [[["Fork_44" \in [1, oo) && "Think_44" \in [1, oo) | ["Fork_4" \in [1, oo) && "Think_4" \in [1, oo) | ["Fork_9" \in [1, oo) && "Think_9" \in [1, oo) | [["Fork_13" \in [1, oo) && "Think_13" \in [1, oo) | [["Fork_5" \in [1, oo) && "Think_5" \in [1, oo) | ["Fork_37" \in [1, oo) && "Think_37" \in [1, oo) | ["Fork_15" \in [1, oo) && "Think_15" \in [1, oo) | ["Fork_14" \in [1, oo) && "Think_14" \in [1, oo) | ["Think_17" \in [1, oo) && "Fork_17" \in [1, oo) | ["Fork_38" \in [1, oo) && "Think_38" \in [1, oo) | ["Fork_7" \in [1, oo) && "Think_7" \in [1, oo) | [[[[[[[[["Fork_1" \in [1, oo) && "Think_1" \in [1, oo) | "Fork_32" \in [1, oo) && "Think_32" \in [1, oo)] | "Think_24" \in [1, oo) && "Fork_24" \in [1, oo)] | "Fork_25" \in [1, oo) && "Think_25" \in [1, oo)] | "Fork_19" \in [1, oo) && "Think_19" \in [1, oo)] | "Fork_12" \in [1, oo) && "Think_12" \in [1, oo)] | "Fork_33" \in [1, oo) && "Think_33" \in [1, oo)] | "Fork_46" \in [1, oo) && "Think_46" \in [1, oo)] | "Fork_48" \in [1, oo) && "Think_48" \in [1, oo)] | "Fork_27" \in [1, oo) && "Think_27" \in [1, oo)]]]]]]]] | "Fork_20" \in [1, oo) && "Think_20" \in [1, oo)]] | "Fork_35" \in [1, oo) && "Think_35" \in [1, oo)]]]] | "Fork_10" \in [1, oo) && "Think_10" \in [1, oo)] | "Fork_18" \in [1, oo) && "Think_18" \in [1, oo)]]]]]]] | "Fork_49" \in [1, oo) && "Think_49" \in [1, oo)] | "Fork_11" \in [1, oo) && "Think_11" \in [1, oo)] | "Fork_29" \in [1, oo) && "Think_29" \in [1, oo)] | "Fork_36" \in [1, oo) && "Think_36" \in [1, oo)]]]]]] | "Fork_21" \in [1, oo) && "Think_21" \in [1, oo)]] | "Think_41" \in [1, oo) && "Fork_41" \in [1, oo)] | "Fork_31" \in [1, oo) && "Think_31" \in [1, oo)] | "Fork_30" \in [1, oo) && "Think_30" \in [1, oo)] | "Think_3" \in [1, oo) && "Fork_3" \in [1, oo)]] | "Fork_28" \in [1, oo) && "Think_28" \in [1, oo)]] | "Think_16" \in [1, oo) && "Fork_16" \in [1, oo)]]]]]]]]

..........................
EG iterations: 26
..........................
EG iterations: 26
.
EG iterations: 1
.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1880_mix_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m6sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) & [[[[[[[[[[[[[[[[[[[[[Think_6=Catch2_6 & [[[[Think_4=Catch2_4 & [[[[[[[[[[[Think_29=Catch2_29 & [[[[[[[[[[[[Think_7=Catch2_7 & [[Think_37=Catch2_37 & true] & Think_3=Catch2_3]] & Think_45=Catch2_45] & Think_12=Catch2_12] & Think_44=Catch2_44] & Think_46=Catch2_46] & Think_10=Catch2_10] & Think_38=Catch2_38] & Think_50=Catch2_50] & Think_35=Catch2_35] & Think_24=Catch2_24] & Think_43=Catch2_43] & Think_27=Catch2_27]] & Think_14=Catch2_14] & Think_21=Catch2_21] & Think_8=Catch2_8] & Think_9=Catch2_9] & Think_5=Catch2_5] & Think_40=Catch2_40] & Think_26=Catch2_26] & Think_23=Catch2_23] & Think_19=Catch2_19] & Think_33=Catch2_33]] & Think_42=Catch2_42] & Think_39=Catch2_39] & Think_49=Catch2_49]] & Think_32=Catch2_32] & Think_2=Catch2_2] & Think_20=Catch2_20] & Think_11=Catch2_11] & Think_41=Catch2_41] & Think_18=Catch2_18] & Think_13=Catch2_13] & Think_36=Catch2_36] & Think_16=Catch2_16] & Think_1=Catch2_1] & Think_15=Catch2_15] & Think_48=Catch2_48] & Think_47=Catch2_47] & Think_31=Catch2_31] & Think_28=Catch2_28] & Think_17=Catch2_17] & Think_34=Catch2_34] & Think_25=Catch2_25] & Think_30=Catch2_30] & Think_22=Catch2_22]]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) & [Think_22=Catch2_22 & [Think_30=Catch2_30 & [Think_25=Catch2_25 & [Think_34=Catch2_34 & [Think_17=Catch2_17 & [Think_28=Catch2_28 & [Think_31=Catch2_31 & [Think_47=Catch2_47 & [Think_48=Catch2_48 & [Think_15=Catch2_15 & [Think_1=Catch2_1 & [Think_16=Catch2_16 & [Think_36=Catch2_36 & [Think_13=Catch2_13 & [Think_18=Catch2_18 & [Think_41=Catch2_41 & [Think_11=Catch2_11 & [Think_20=Catch2_20 & [Think_2=Catch2_2 & [Think_32=Catch2_32 & [Think_6=Catch2_6 & [Think_49=Catch2_49 & [Think_39=Catch2_39 & [Think_42=Catch2_42 & [Think_4=Catch2_4 & [Think_33=Catch2_33 & [Think_19=Catch2_19 & [Think_23=Catch2_23 & [Think_26=Catch2_26 & [Think_40=Catch2_40 & [Think_5=Catch2_5 & [Think_9=Catch2_9 & [Think_8=Catch2_8 & [Think_21=Catch2_21 & [Think_14=Catch2_14 & [Think_29=Catch2_29 & [Think_27=Catch2_27 & [Think_43=Catch2_43 & [Think_24=Catch2_24 & [[[[Think_10=Catch2_10 & [Think_46=Catch2_46 & [Think_44=Catch2_44 & [Think_12=Catch2_12 & [Think_45=Catch2_45 & [Think_7=Catch2_7 & [Think_3=Catch2_3 & [Think_37=Catch2_37 & true]]]]]]]] & Think_38=Catch2_38] & Think_50=Catch2_50] & Think_35=Catch2_35]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1881_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) | [[[[[[[[[[[[[[[[[[Think_20=Catch2_20 & [[[[[[[[[[[[[[Think_9=Catch2_9 & [[[[[[[[[[[[[[[[[[true & Think_37=Catch2_37] & Think_3=Catch2_3] & Think_7=Catch2_7] & Think_45=Catch2_45] & Think_12=Catch2_12] & Think_44=Catch2_44] & Think_46=Catch2_46] & Think_10=Catch2_10] & Think_38=Catch2_38] & Think_50=Catch2_50] & Think_35=Catch2_35] & Think_24=Catch2_24] & Think_43=Catch2_43] & Think_27=Catch2_27] & Think_29=Catch2_29] & Think_14=Catch2_14] & Think_21=Catch2_21] & Think_8=Catch2_8]] & Think_5=Catch2_5] & Think_40=Catch2_40] & Think_26=Catch2_26] & Think_23=Catch2_23] & Think_19=Catch2_19] & Think_33=Catch2_33] & Think_4=Catch2_4] & Think_42=Catch2_42] & Think_39=Catch2_39] & Think_49=Catch2_49] & Think_6=Catch2_6] & Think_32=Catch2_32] & Think_2=Catch2_2]] & Think_11=Catch2_11] & Think_41=Catch2_41] & Think_18=Catch2_18] & Think_13=Catch2_13] & Think_36=Catch2_36] & Think_16=Catch2_16] & Think_1=Catch2_1] & Think_15=Catch2_15] & Think_48=Catch2_48] & Think_47=Catch2_47] & Think_31=Catch2_31] & Think_28=Catch2_28] & Think_17=Catch2_17] & Think_34=Catch2_34] & Think_25=Catch2_25] & Think_30=Catch2_30] & Think_22=Catch2_22]]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) | [Think_22=Catch2_22 & [Think_30=Catch2_30 & [Think_25=Catch2_25 & [Think_34=Catch2_34 & [Think_17=Catch2_17 & [Think_28=Catch2_28 & [Think_31=Catch2_31 & [Think_47=Catch2_47 & [Think_48=Catch2_48 & [Think_15=Catch2_15 & [Think_1=Catch2_1 & [Think_16=Catch2_16 & [Think_36=Catch2_36 & [Think_13=Catch2_13 & [Think_18=Catch2_18 & [Think_41=Catch2_41 & [Think_11=Catch2_11 & [Think_20=Catch2_20 & [Think_2=Catch2_2 & [Think_32=Catch2_32 & [Think_6=Catch2_6 & [Think_49=Catch2_49 & [Think_39=Catch2_39 & [Think_42=Catch2_42 & [Think_4=Catch2_4 & [Think_33=Catch2_33 & [Think_19=Catch2_19 & [Think_23=Catch2_23 & [Think_26=Catch2_26 & [Think_40=Catch2_40 & [Think_5=Catch2_5 & [Think_9=Catch2_9 & [Think_8=Catch2_8 & [Think_21=Catch2_21 & [Think_14=Catch2_14 & [Think_29=Catch2_29 & [Think_27=Catch2_27 & [Think_43=Catch2_43 & [Think_24=Catch2_24 & [Think_35=Catch2_35 & [Think_50=Catch2_50 & [Think_38=Catch2_38 & [Think_10=Catch2_10 & [Think_46=Catch2_46 & [Think_44=Catch2_44 & [Think_12=Catch2_12 & [Think_45=Catch2_45 & [Think_7=Catch2_7 & [Think_3=Catch2_3 & [Think_37=Catch2_37 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1882_mix_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) ] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Think_37=Catch2_37] & Think_3=Catch2_3] & Think_7=Catch2_7] & Think_45=Catch2_45] & Think_12=Catch2_12] & Think_44=Catch2_44] & Think_46=Catch2_46] & Think_10=Catch2_10] & Think_38=Catch2_38] & Think_50=Catch2_50] & Think_35=Catch2_35] & Think_24=Catch2_24] & Think_43=Catch2_43] & Think_27=Catch2_27] & Think_29=Catch2_29] & Think_14=Catch2_14] & Think_21=Catch2_21] & Think_8=Catch2_8] & Think_9=Catch2_9] & Think_5=Catch2_5] & Think_40=Catch2_40] & Think_26=Catch2_26] & Think_23=Catch2_23] & Think_19=Catch2_19] & Think_33=Catch2_33] & Think_4=Catch2_4] & Think_42=Catch2_42] & Think_39=Catch2_39] & Think_49=Catch2_49] & Think_6=Catch2_6] & Think_32=Catch2_32] & Think_2=Catch2_2] & Think_20=Catch2_20] & Think_11=Catch2_11] & Think_41=Catch2_41] & Think_18=Catch2_18] & Think_13=Catch2_13] & Think_36=Catch2_36] & Think_16=Catch2_16] & Think_1=Catch2_1] & Think_15=Catch2_15] & Think_48=Catch2_48] & Think_47=Catch2_47] & Think_31=Catch2_31] & Think_28=Catch2_28] & Think_17=Catch2_17] & Think_34=Catch2_34] & Think_25=Catch2_25] & Think_30=Catch2_30] & Think_22=Catch2_22]]]
normalized: ~ [E [true U ~ [[[Think_22=Catch2_22 & [Think_30=Catch2_30 & [Think_25=Catch2_25 & [Think_34=Catch2_34 & [Think_17=Catch2_17 & [Think_28=Catch2_28 & [Think_31=Catch2_31 & [Think_47=Catch2_47 & [Think_48=Catch2_48 & [Think_15=Catch2_15 & [Think_1=Catch2_1 & [Think_16=Catch2_16 & [Think_36=Catch2_36 & [Think_13=Catch2_13 & [Think_18=Catch2_18 & [Think_41=Catch2_41 & [Think_11=Catch2_11 & [Think_20=Catch2_20 & [Think_2=Catch2_2 & [Think_32=Catch2_32 & [Think_6=Catch2_6 & [Think_49=Catch2_49 & [Think_39=Catch2_39 & [Think_42=Catch2_42 & [Think_4=Catch2_4 & [Think_33=Catch2_33 & [Think_19=Catch2_19 & [Think_23=Catch2_23 & [Think_26=Catch2_26 & [Think_40=Catch2_40 & [Think_5=Catch2_5 & [Think_9=Catch2_9 & [Think_8=Catch2_8 & [Think_21=Catch2_21 & [Think_14=Catch2_14 & [Think_29=Catch2_29 & [Think_27=Catch2_27 & [Think_43=Catch2_43 & [Think_24=Catch2_24 & [Think_35=Catch2_35 & [Think_50=Catch2_50 & [Think_38=Catch2_38 & [Think_10=Catch2_10 & [Think_46=Catch2_46 & [Think_44=Catch2_44 & [Think_12=Catch2_12 & [Think_45=Catch2_45 & [Think_7=Catch2_7 & [Think_3=Catch2_3 & [Think_37=Catch2_37 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch2_21 + Catch2_26 ) + Catch2_43 ) + Catch2_35 ) + Catch2_44 ) + Catch2_47 ) + Catch2_18 ) + Catch2_12 ) + Catch2_1 ) + Catch2_16 ) + Catch2_37 ) + Catch2_34 ) + Catch2_25 ) + Catch2_17 ) + Catch2_36 ) + Catch2_2 ) + Catch2_4 ) + Catch2_10 ) + Catch2_38 ) + Catch2_30 ) + Catch2_14 ) + Catch2_15 ) + Catch2_29 ) + Catch2_39 ) + Catch2_48 ) + Catch2_20 ) + Catch2_50 ) + Catch2_28 ) + Catch2_33 ) + Catch2_23 ) + Catch2_3 ) + Catch2_32 ) + Catch2_27 ) + Catch2_19 ) + Catch2_49 ) + Catch2_40 ) + Catch2_46 ) + Catch2_9 ) + Catch2_42 ) + Catch2_8 ) + Catch2_5 ) + Catch2_41 ) + Catch2_31 ) + Catch2_7 ) + Catch2_45 ) + Catch2_13 ) + Catch2_22 ) + Catch2_24 ) + Catch2_11 ) + Catch2_6 ) > ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Catch1_30 + Catch1_38 ) + Catch1_14 ) + Catch1_36 ) + Catch1_48 ) + Catch1_47 ) + Catch1_41 ) + Catch1_40 ) + Catch1_11 ) + Catch1_1 ) + Catch1_26 ) + Catch1_19 ) + Catch1_13 ) + Catch1_31 ) + Catch1_2 ) + Catch1_29 ) + Catch1_46 ) + Catch1_15 ) + Catch1_32 ) + Catch1_45 ) + Catch1_17 ) + Catch1_8 ) + Catch1_21 ) + Catch1_6 ) + Catch1_24 ) + Catch1_50 ) + Catch1_4 ) + Catch1_5 ) + Catch1_28 ) + Catch1_34 ) + Catch1_16 ) + Catch1_23 ) + Catch1_33 ) + Catch1_22 ) + Catch1_39 ) + Catch1_10 ) + Catch1_42 ) + Catch1_44 ) + Catch1_12 ) + Catch1_18 ) + Catch1_49 ) + Catch1_7 ) + Catch1_3 ) + Catch1_27 ) + Catch1_25 ) + Catch1_20 ) + Catch1_37 ) + Catch1_35 ) + Catch1_43 ) + Catch1_9 ) ]]]]]

-> the formula is FALSE

FORMULA p_1883_mix_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m24sec

STOP 1369708161

--------------------
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)
825 892 891 918 1002 1024 984 1095 1159 1039 1215 1166 1089 1275 1130 1281 1138 1166 1252 1323 1374 1428 1444 1422 1398 1359 1300 1259 1270
iterations count:29418 (117), effective:4991 (19)

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

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

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