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

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

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

execution on node 2: quadhexa-2.u-paris10.fr (runId=136968525700258_n_2)
=====================================================================
runnning marcie on Philosophers-PT-000100 (CTLMarkingComparison)
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-000100, examination is CTLMarkingComparison
=====================================================================

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

START 1369718822

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 500 NrTr: 500)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


-> reachability set: #nodes 2580 (2.6e+03) #states 515,377,520,732,011,331,036,461,129,765,621,272,702,107,522,001 (47)



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

checking: AF [[[[[Catch2_77=0.000000000000000 & [[Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [[[Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [[[[[[[[Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [[Catch2_23=0.000000000000000 & [[[[[Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [[[Catch2_4=0.000000000000000 & [[[[Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [[[[[[[Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [[Catch2_75=0.000000000000000 & [[[[Catch2_85=0.000000000000000 & [[[Catch2_93=0.000000000000000 & [[[[Catch2_14=0.000000000000000 & [[Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [[[[Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [[Catch2_16=0.000000000000000 & [[[[[Catch2_87=0.000000000000000 & [[Catch2_38=0.000000000000000 & [[Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [[[Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [[Catch2_90=0.000000000000000 & [[Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [[[Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [[Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [[Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [[true & 1.000000000000000=Catch2_69] & Catch2_66=0.000000000000000]]] & Catch2_95=0.000000000000000]]] & Catch2_45=0.000000000000000]]] & Catch2_68=0.000000000000000] & Catch2_21=0.000000000000000]]]] & Catch2_63=0.000000000000000]] & Catch2_3=0.000000000000000]]] & Catch2_7=0.000000000000000] & Catch2_43=0.000000000000000]]] & Catch2_11=0.000000000000000]] & Catch2_97=0.000000000000000]] & Catch2_49=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_52=0.000000000000000]] & Catch2_10=0.000000000000000]]] & Catch2_64=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_31=0.000000000000000]]]] & Catch2_80=0.000000000000000]] & Catch2_8=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_78=0.000000000000000]] & Catch2_42=0.000000000000000] & Catch2_39=0.000000000000000]] & Catch2_20=0.000000000000000] & Catch2_1=0.000000000000000] & Catch2_22=0.000000000000000]] & Catch2_35=0.000000000000000]]]] & Catch2_73=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_54=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_94=0.000000000000000]]] & Catch2_29=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_53=0.000000000000000]] & Catch2_44=0.000000000000000] & Catch2_62=0.000000000000000]]] & Catch2_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000]] & Catch2_41=0.000000000000000]]] & Catch2_57=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_83=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_59=0.000000000000000] & Catch2_19=0.000000000000000]]] & Catch2_32=0.000000000000000] & Catch2_47=0.000000000000000]]] & Catch2_61=0.000000000000000]] & Catch2_25=0.000000000000000] & Catch2_24=0.000000000000000] & [[[Fork_13=0.000000000000000 & [[Fork_9=0.000000000000000 & [[[[Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [[[[[[[[[[[[Fork_82=0.000000000000000 & [[[[[Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [[[Fork_79=0.000000000000000 & [[Fork_14=0.000000000000000 & [[Fork_76=0.000000000000000 & [[[Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [[[Fork_62=0.000000000000000 & [[[[[[Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [[Fork_33=0.000000000000000 & [[[Fork_70=0.000000000000000 & [[[Fork_20=0.000000000000000 & [[[[Fork_43=0.000000000000000 & [[Fork_93=0.000000000000000 & [[[Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [[Fork_50=0.000000000000000 & [[[[[Fork_73=0.000000000000000 & [[Fork_87=0.000000000000000 & [[[Fork_92=0.000000000000000 & [[[[[[Fork_94=0.000000000000000 & [[Fork_47=0.000000000000000 & [[[[Fork_54=0.000000000000000 & [[[Fork_74=0.000000000000000 & [[Fork_81=0.000000000000000 & [[true & 1.000000000000000=Fork_75] & Fork_52=0.000000000000000]] & Fork_96=0.000000000000000]] & Fork_80=0.000000000000000] & Fork_15=0.000000000000000]] & Fork_24=0.000000000000000] & Fork_1=0.000000000000000] & Fork_29=0.000000000000000]] & Fork_34=0.000000000000000]] & Fork_2=0.000000000000000] & Fork_57=0.000000000000000] & Fork_44=0.000000000000000] & Fork_21=0.000000000000000] & Fork_31=0.000000000000000]] & Fork_22=0.000000000000000] & Fork_37=0.000000000000000]] & Fork_39=0.000000000000000]] & Fork_28=0.000000000000000] & Fork_35=0.000000000000000] & Fork_17=0.000000000000000] & Fork_72=0.000000000000000]] & Fork_85=0.000000000000000]]] & Fork_25=0.000000000000000] & Fork_7=0.000000000000000]] & Fork_5=0.000000000000000]] & Fork_83=0.000000000000000] & Fork_53=0.000000000000000] & Fork_11=0.000000000000000]] & Fork_46=0.000000000000000] & Fork_30=0.000000000000000]] & Fork_27=0.000000000000000] & Fork_45=0.000000000000000]] & Fork_8=0.000000000000000]]]] & Fork_38=0.000000000000000] & Fork_6=0.000000000000000] & Fork_19=0.000000000000000] & Fork_100=0.000000000000000] & Fork_58=0.000000000000000]] & Fork_51=0.000000000000000] & Fork_89=0.000000000000000]]] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000]] & Fork_12=0.000000000000000]] & Fork_66=0.000000000000000]] & Fork_32=0.000000000000000] & Fork_69=0.000000000000000]]] & Fork_64=0.000000000000000] & Fork_88=0.000000000000000] & Fork_99=0.000000000000000] & Fork_90=0.000000000000000]] & Fork_77=0.000000000000000] & Fork_18=0.000000000000000] & Fork_3=0.000000000000000] & Fork_78=0.000000000000000] & Fork_42=0.000000000000000] & Fork_61=0.000000000000000] & Fork_60=0.000000000000000] & Fork_68=0.000000000000000] & Fork_40=0.000000000000000] & Fork_84=0.000000000000000] & Fork_10=0.000000000000000]]]] & Fork_95=0.000000000000000] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000]] & Fork_55=0.000000000000000]] & Fork_91=0.000000000000000] & Fork_36=0.000000000000000]]]
normalized: ~ [EG [~ [[[Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_66=0.000000000000000 & [1.000000000000000=Catch2_69 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [Fork_84=0.000000000000000 & [Fork_40=0.000000000000000 & [Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [Fork_61=0.000000000000000 & [Fork_42=0.000000000000000 & [Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [Fork_14=0.000000000000000 & [Fork_12=0.000000000000000 & [Fork_76=0.000000000000000 & [Fork_56=0.000000000000000 & [Fork_63=0.000000000000000 & [Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [Fork_62=0.000000000000000 & [Fork_58=0.000000000000000 & [Fork_100=0.000000000000000 & [Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [Fork_8=0.000000000000000 & [Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [Fork_20=0.000000000000000 & [Fork_11=0.000000000000000 & [Fork_53=0.000000000000000 & [Fork_83=0.000000000000000 & [Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [Fork_92=0.000000000000000 & [Fork_31=0.000000000000000 & [Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [Fork_1=0.000000000000000 & [Fork_24=0.000000000000000 & [Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [Fork_52=0.000000000000000 & [1.000000000000000=Fork_75 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1866_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [[[[[Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [[[[[Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [[[[[Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [[[[[Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [[[[[Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [[[[[Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [[[[[[Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [[[[[[Catch2_97=0.000000000000000 & [[[[[[[Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [[Catch2_90=0.000000000000000 & [[[[[Catch2_21=0.000000000000000 & [[[[[[Catch2_37=0.000000000000000 & [[[[[1.000000000000000=Catch2_69 & true] & Catch2_66=0.000000000000000] & Catch2_99=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_95=0.000000000000000]] & Catch2_96=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_56=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_68=0.000000000000000]] & Catch2_86=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_63=0.000000000000000]] & Catch2_3=0.000000000000000]]] & Catch2_7=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_84=0.000000000000000] & Catch2_50=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_38=0.000000000000000]] & Catch2_87=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_52=0.000000000000000]]] & Catch2_30=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_31=0.000000000000000]]]]] & Catch2_14=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_78=0.000000000000000]]]]]]] & Catch2_22=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_72=0.000000000000000]]]]]]] & Catch2_58=0.000000000000000] & Catch2_94=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_71=0.000000000000000]]]]]]] & Catch2_81=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_89=0.000000000000000]]]]]]] & Catch2_57=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_83=0.000000000000000]]]]]]] & Catch2_47=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_61=0.000000000000000]]]] | [Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [[[[[[Fork_40=0.000000000000000 & [[[[[Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [[[[[[[[[[Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [[Fork_58=0.000000000000000 & [[Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [[[[[[Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [[[[[[[Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [[[[[Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [[[[[Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [[[[[Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [[true & 1.000000000000000=Fork_75] & Fork_52=0.000000000000000]]]]]]] & Fork_24=0.000000000000000] & Fork_1=0.000000000000000] & Fork_29=0.000000000000000] & Fork_47=0.000000000000000]]]]]]] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000] & Fork_22=0.000000000000000] & Fork_37=0.000000000000000]]]]]]] & Fork_72=0.000000000000000] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000] & Fork_65=0.000000000000000]]]]]]] & Fork_83=0.000000000000000] & Fork_53=0.000000000000000] & Fork_11=0.000000000000000] & Fork_20=0.000000000000000] & Fork_46=0.000000000000000] & Fork_30=0.000000000000000]]]]] & Fork_8=0.000000000000000] & Fork_86=0.000000000000000] & Fork_49=0.000000000000000] & Fork_67=0.000000000000000] & Fork_38=0.000000000000000]]] & Fork_100=0.000000000000000]] & Fork_62=0.000000000000000]]] & Fork_41=0.000000000000000] & Fork_4=0.000000000000000] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000] & Fork_76=0.000000000000000] & Fork_12=0.000000000000000] & Fork_14=0.000000000000000] & Fork_66=0.000000000000000] & Fork_79=0.000000000000000]]]]]]]]]]]]]] & Fork_42=0.000000000000000] & Fork_61=0.000000000000000] & Fork_60=0.000000000000000] & Fork_68=0.000000000000000]] & Fork_84=0.000000000000000] & Fork_10=0.000000000000000] & Fork_48=0.000000000000000] & Fork_98=0.000000000000000] & Fork_16=0.000000000000000]]]]]]]]]]]
normalized: EG [[[Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [Fork_84=0.000000000000000 & [Fork_40=0.000000000000000 & [Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [Fork_61=0.000000000000000 & [Fork_42=0.000000000000000 & [Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [Fork_14=0.000000000000000 & [Fork_12=0.000000000000000 & [Fork_76=0.000000000000000 & [Fork_56=0.000000000000000 & [Fork_63=0.000000000000000 & [Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [Fork_62=0.000000000000000 & [Fork_58=0.000000000000000 & [Fork_100=0.000000000000000 & [Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [Fork_8=0.000000000000000 & [Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [Fork_20=0.000000000000000 & [Fork_11=0.000000000000000 & [Fork_53=0.000000000000000 & [Fork_83=0.000000000000000 & [Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [Fork_92=0.000000000000000 & [Fork_31=0.000000000000000 & [Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [Fork_1=0.000000000000000 & [Fork_24=0.000000000000000 & [Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [Fork_52=0.000000000000000 & [1.000000000000000=Fork_75 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_66=0.000000000000000 & [1.000000000000000=Catch2_69 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1867_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[~ [[Fork_36=0.000000000000000 & [[[[Fork_9=0.000000000000000 & [[[Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [[[Fork_10=0.000000000000000 & [[[[[[[[Fork_3=0.000000000000000 & [[[[Fork_90=0.000000000000000 & [[[[Fork_23=0.000000000000000 & [[[[Fork_79=0.000000000000000 & [[[[Fork_76=0.000000000000000 & [[[[Fork_41=0.000000000000000 & [[[[Fork_58=0.000000000000000 & [[[[Fork_38=0.000000000000000 & [[[[Fork_8=0.000000000000000 & [[[[Fork_70=0.000000000000000 & [[[[Fork_11=0.000000000000000 & [[[[Fork_5=0.000000000000000 & [[[[Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [[[[Fork_17=0.000000000000000 & [[[[Fork_39=0.000000000000000 & [[[[[[Fork_21=0.000000000000000 & [[[[Fork_94=0.000000000000000 & [[[[[Fork_24=0.000000000000000 & [[[[[Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [[true & 1.000000000000000=Fork_75] & Fork_52=0.000000000000000]]] & Fork_74=0.000000000000000] & Fork_80=0.000000000000000] & Fork_15=0.000000000000000] & Fork_54=0.000000000000000]] & Fork_1=0.000000000000000] & Fork_29=0.000000000000000] & Fork_47=0.000000000000000] & Fork_34=0.000000000000000]] & Fork_2=0.000000000000000] & Fork_57=0.000000000000000] & Fork_44=0.000000000000000]] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000] & Fork_22=0.000000000000000] & Fork_37=0.000000000000000] & Fork_87=0.000000000000000]] & Fork_73=0.000000000000000] & Fork_28=0.000000000000000] & Fork_35=0.000000000000000]] & Fork_72=0.000000000000000] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000]]] & Fork_25=0.000000000000000] & Fork_7=0.000000000000000] & Fork_93=0.000000000000000]] & Fork_43=0.000000000000000] & Fork_83=0.000000000000000] & Fork_53=0.000000000000000]] & Fork_20=0.000000000000000] & Fork_46=0.000000000000000] & Fork_30=0.000000000000000]] & Fork_27=0.000000000000000] & Fork_45=0.000000000000000] & Fork_33=0.000000000000000]] & Fork_86=0.000000000000000] & Fork_49=0.000000000000000] & Fork_67=0.000000000000000]] & Fork_6=0.000000000000000] & Fork_19=0.000000000000000] & Fork_100=0.000000000000000]] & Fork_62=0.000000000000000] & Fork_51=0.000000000000000] & Fork_89=0.000000000000000]] & Fork_4=0.000000000000000] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000]] & Fork_12=0.000000000000000] & Fork_14=0.000000000000000] & Fork_66=0.000000000000000]] & Fork_32=0.000000000000000] & Fork_69=0.000000000000000] & Fork_71=0.000000000000000]] & Fork_64=0.000000000000000] & Fork_88=0.000000000000000] & Fork_99=0.000000000000000]] & Fork_82=0.000000000000000] & Fork_77=0.000000000000000] & Fork_18=0.000000000000000]] & Fork_78=0.000000000000000] & Fork_42=0.000000000000000] & Fork_61=0.000000000000000] & Fork_60=0.000000000000000] & Fork_68=0.000000000000000] & Fork_40=0.000000000000000] & Fork_84=0.000000000000000]] & Fork_48=0.000000000000000] & Fork_98=0.000000000000000]]] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000]] & Fork_55=0.000000000000000] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000]]] & ~ [[Catch2_24=0.000000000000000 & [[[[[[[[[[Catch2_19=0.000000000000000 & [[Catch2_33=0.000000000000000 & [[[[Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [[[[[[[[[Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [[[Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [[[[Catch2_6=0.000000000000000 & [[[[[[[[[[[[[[[[Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [[[[[[Catch2_49=0.000000000000000 & [[[[[Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [[[[[[Catch2_37=0.000000000000000 & [[[[[1.000000000000000=Catch2_69 & true] & Catch2_66=0.000000000000000] & Catch2_99=0.000000000000000] & Catch2_67=0.000000000000000] & Catch2_95=0.000000000000000]] & Catch2_96=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_56=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_68=0.000000000000000]]]]]]]]]]]]]] & Catch2_11=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_97=0.000000000000000] & Catch2_87=0.000000000000000]] & Catch2_79=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_52=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_10=0.000000000000000]]]]]]]]]]]]]] & Catch2_93=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_20=0.000000000000000] & Catch2_1=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_72=0.000000000000000] & Catch2_55=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_54=0.000000000000000]] & Catch2_58=0.000000000000000] & Catch2_94=0.000000000000000] & Catch2_70=0.000000000000000]]] & Catch2_60=0.000000000000000] & Catch2_53=0.000000000000000]]] & Catch2_62=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_23=0.000000000000000]]]]] & Catch2_100=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_83=0.000000000000000]] & Catch2_59=0.000000000000000]] & Catch2_91=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_61=0.000000000000000] & Catch2_77=0.000000000000000] & Catch2_25=0.000000000000000]]]]]
normalized: ~ [EG [~ [[~ [[Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_66=0.000000000000000 & [1.000000000000000=Catch2_69 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [[Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [Fork_84=0.000000000000000 & [Fork_40=0.000000000000000 & [Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [Fork_61=0.000000000000000 & [Fork_42=0.000000000000000 & [Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [Fork_14=0.000000000000000 & [Fork_12=0.000000000000000 & [Fork_76=0.000000000000000 & [Fork_56=0.000000000000000 & [Fork_63=0.000000000000000 & [Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [Fork_62=0.000000000000000 & [Fork_58=0.000000000000000 & [Fork_100=0.000000000000000 & [Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [Fork_8=0.000000000000000 & [Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [Fork_20=0.000000000000000 & [Fork_11=0.000000000000000 & [Fork_53=0.000000000000000 & [Fork_83=0.000000000000000 & [Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [Fork_92=0.000000000000000 & [Fork_31=0.000000000000000 & [Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [Fork_1=0.000000000000000 & [Fork_24=0.000000000000000 & [Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [Fork_52=0.000000000000000 & [1.000000000000000=Fork_75 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is TRUE

FORMULA p_1868_markingcomparison_eq_and_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[Catch2_24=0.000000000000000 & [[[[[[[[Catch2_18=0.000000000000000 & [[[[[[[[[[[[[Catch2_82=0.000000000000000 & [[[[[[[[[[[[[[[[[Catch2_54=0.000000000000000 & [[[[[[[Catch2_75=0.000000000000000 & [[[[[[[[[[[Catch2_14=0.000000000000000 & [[[Catch2_13=0.000000000000000 & [[[[[[[[[Catch2_52=0.000000000000000 & [[[[[[[[[[[Catch2_7=0.000000000000000 & [[[Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [[[Catch2_74=0.000000000000000 & [[[Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [[[Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [[[Catch2_99=0.000000000000000 & [[true & 1.000000000000000=Catch2_69] & Catch2_66=0.000000000000000]] & Catch2_67=0.000000000000000] & Catch2_95=0.000000000000000]]] & Catch2_45=0.000000000000000] & Catch2_56=0.000000000000000]]] & Catch2_21=0.000000000000000] & Catch2_86=0.000000000000000]] & Catch2_5=0.000000000000000] & Catch2_63=0.000000000000000]]] & Catch2_65=0.000000000000000] & Catch2_26=0.000000000000000]] & Catch2_43=0.000000000000000] & Catch2_84=0.000000000000000] & Catch2_50=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_97=0.000000000000000] & Catch2_87=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_17=0.000000000000000]] & Catch2_16=0.000000000000000] & Catch2_10=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_31=0.000000000000000] & Catch2_98=0.000000000000000]] & Catch2_2=0.000000000000000] & Catch2_80=0.000000000000000]] & Catch2_8=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_78=0.000000000000000] & Catch2_93=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_85=0.000000000000000] & Catch2_20=0.000000000000000] & Catch2_1=0.000000000000000] & Catch2_22=0.000000000000000]] & Catch2_35=0.000000000000000] & Catch2_72=0.000000000000000] & Catch2_55=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_15=0.000000000000000]] & Catch2_6=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_94=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_71=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_53=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_62=0.000000000000000] & Catch2_81=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000]] & Catch2_23=0.000000000000000] & Catch2_41=0.000000000000000] & Catch2_51=0.000000000000000] & Catch2_76=0.000000000000000] & Catch2_57=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_83=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_59=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_91=0.000000000000000]] & Catch2_32=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_61=0.000000000000000] & Catch2_77=0.000000000000000] & Catch2_25=0.000000000000000]]] | ~ [[Fork_36=0.000000000000000 & [[[[[[[Fork_95=0.000000000000000 & [[[[[Fork_84=0.000000000000000 & [[[[[[[[[[[Fork_90=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Fork_19=0.000000000000000 & [[[[[[[[[[[[[[[[[Fork_43=0.000000000000000 & [[[Fork_7=0.000000000000000 & [[Fork_26=0.000000000000000 & [[[[[[[[[[[[[[[[[Fork_57=0.000000000000000 & [[[[[Fork_29=0.000000000000000 & [[[[[Fork_80=0.000000000000000 & [[[Fork_81=0.000000000000000 & [[true & 1.000000000000000=Fork_75] & Fork_52=0.000000000000000]] & Fork_96=0.000000000000000] & Fork_74=0.000000000000000]] & Fork_15=0.000000000000000] & Fork_54=0.000000000000000] & Fork_24=0.000000000000000] & Fork_1=0.000000000000000]] & Fork_47=0.000000000000000] & Fork_34=0.000000000000000] & Fork_94=0.000000000000000] & Fork_2=0.000000000000000]] & Fork_44=0.000000000000000] & Fork_21=0.000000000000000] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000] & Fork_22=0.000000000000000] & Fork_37=0.000000000000000] & Fork_87=0.000000000000000] & Fork_39=0.000000000000000] & Fork_73=0.000000000000000] & Fork_28=0.000000000000000] & Fork_35=0.000000000000000] & Fork_17=0.000000000000000] & Fork_72=0.000000000000000] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000] & Fork_65=0.000000000000000]] & Fork_25=0.000000000000000]] & Fork_93=0.000000000000000] & Fork_5=0.000000000000000]] & Fork_83=0.000000000000000] & Fork_53=0.000000000000000] & Fork_11=0.000000000000000] & Fork_20=0.000000000000000] & Fork_46=0.000000000000000] & Fork_30=0.000000000000000] & Fork_70=0.000000000000000] & Fork_27=0.000000000000000] & Fork_45=0.000000000000000] & Fork_33=0.000000000000000] & Fork_8=0.000000000000000] & Fork_86=0.000000000000000] & Fork_49=0.000000000000000] & Fork_67=0.000000000000000] & Fork_38=0.000000000000000] & Fork_6=0.000000000000000]] & Fork_100=0.000000000000000] & Fork_58=0.000000000000000] & Fork_62=0.000000000000000] & Fork_51=0.000000000000000] & Fork_89=0.000000000000000] & Fork_41=0.000000000000000] & Fork_4=0.000000000000000] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000] & Fork_76=0.000000000000000] & Fork_12=0.000000000000000] & Fork_14=0.000000000000000] & Fork_66=0.000000000000000] & Fork_79=0.000000000000000] & Fork_32=0.000000000000000] & Fork_69=0.000000000000000] & Fork_71=0.000000000000000] & Fork_23=0.000000000000000] & Fork_64=0.000000000000000] & Fork_88=0.000000000000000] & Fork_99=0.000000000000000]] & Fork_82=0.000000000000000] & Fork_77=0.000000000000000] & Fork_18=0.000000000000000] & Fork_3=0.000000000000000] & Fork_78=0.000000000000000] & Fork_42=0.000000000000000] & Fork_61=0.000000000000000] & Fork_60=0.000000000000000] & Fork_68=0.000000000000000] & Fork_40=0.000000000000000]] & Fork_10=0.000000000000000] & Fork_48=0.000000000000000] & Fork_98=0.000000000000000] & Fork_16=0.000000000000000]] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000] & Fork_9=0.000000000000000] & Fork_55=0.000000000000000] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000]]]]]
normalized: ~ [E [true U ~ [[~ [[Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [Fork_84=0.000000000000000 & [Fork_40=0.000000000000000 & [Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [Fork_61=0.000000000000000 & [Fork_42=0.000000000000000 & [Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [Fork_14=0.000000000000000 & [Fork_12=0.000000000000000 & [Fork_76=0.000000000000000 & [Fork_56=0.000000000000000 & [Fork_63=0.000000000000000 & [Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [Fork_62=0.000000000000000 & [Fork_58=0.000000000000000 & [Fork_100=0.000000000000000 & [Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [Fork_8=0.000000000000000 & [Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [Fork_20=0.000000000000000 & [Fork_11=0.000000000000000 & [Fork_53=0.000000000000000 & [Fork_83=0.000000000000000 & [Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [Fork_92=0.000000000000000 & [Fork_31=0.000000000000000 & [Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [Fork_1=0.000000000000000 & [Fork_24=0.000000000000000 & [Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [Fork_52=0.000000000000000 & [1.000000000000000=Fork_75 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ~ [[Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_66=0.000000000000000 & [1.000000000000000=Catch2_69 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_1869_markingcomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [E [AF [[[[Catch2_77=0.000000000000000 & [[[[[[Catch2_18=0.000000000000000 & [[[[[[[[[[[[[[[[[[Catch2_81=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Catch2_20=0.000000000000000 & [[[[[[[[[[[Catch2_13=0.000000000000000 & [[[[[[[[[[[[[[[Catch2_38=0.000000000000000 & [[[Catch2_84=0.000000000000000 & [[[[[[[[[[[[[[[Catch2_45=0.000000000000000 & [[[[Catch2_67=0.000000000000000 & [[[true & 1.000000000000000=Catch2_69] & Catch2_66=0.000000000000000] & Catch2_99=0.000000000000000]] & Catch2_95=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_96=0.000000000000000]] & Catch2_56=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_68=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_86=0.000000000000000] & Catch2_74=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_63=0.000000000000000] & Catch2_90=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_65=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_43=0.000000000000000]] & Catch2_50=0.000000000000000] & Catch2_11=0.000000000000000]] & Catch2_97=0.000000000000000] & Catch2_87=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_79=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_52=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_10=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_64=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_31=0.000000000000000] & Catch2_98=0.000000000000000]] & Catch2_2=0.000000000000000] & Catch2_80=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_88=0.000000000000000] & Catch2_78=0.000000000000000] & Catch2_93=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_85=0.000000000000000]] & Catch2_1=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_75=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_72=0.000000000000000] & Catch2_55=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_73=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_54=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_58=0.000000000000000] & Catch2_94=0.000000000000000] & Catch2_70=0.000000000000000] & Catch2_71=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_60=0.000000000000000] & Catch2_53=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_62=0.000000000000000]] & Catch2_12=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_41=0.000000000000000] & Catch2_51=0.000000000000000] & Catch2_76=0.000000000000000] & Catch2_57=0.000000000000000] & Catch2_100=0.000000000000000] & Catch2_92=0.000000000000000] & Catch2_83=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_59=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_91=0.000000000000000]] & Catch2_32=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_61=0.000000000000000]] & Catch2_25=0.000000000000000] & Catch2_24=0.000000000000000]] U EG [[[[[[[[[[[[[[[[[Fork_60=0.000000000000000 & [[[[[[[Fork_82=0.000000000000000 & [[[[Fork_64=0.000000000000000 & [[[[[[[[[[[[[[[[[[Fork_100=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Fork_25=0.000000000000000 & [[[[[[[[[[[[[[[Fork_31=0.000000000000000 & [[[[[[[Fork_47=0.000000000000000 & [[[[Fork_54=0.000000000000000 & [[[[[[[1.000000000000000=Fork_75 & true] & Fork_52=0.000000000000000] & Fork_81=0.000000000000000] & Fork_96=0.000000000000000] & Fork_74=0.000000000000000] & Fork_80=0.000000000000000] & Fork_15=0.000000000000000]] & Fork_24=0.000000000000000] & Fork_1=0.000000000000000] & Fork_29=0.000000000000000]] & Fork_34=0.000000000000000] & Fork_94=0.000000000000000] & Fork_2=0.000000000000000] & Fork_57=0.000000000000000] & Fork_44=0.000000000000000] & Fork_21=0.000000000000000]] & Fork_92=0.000000000000000] & Fork_22=0.000000000000000] & Fork_37=0.000000000000000] & Fork_87=0.000000000000000] & Fork_39=0.000000000000000] & Fork_73=0.000000000000000] & Fork_28=0.000000000000000] & Fork_35=0.000000000000000] & Fork_17=0.000000000000000] & Fork_72=0.000000000000000] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000] & Fork_65=0.000000000000000] & Fork_26=0.000000000000000]] & Fork_7=0.000000000000000] & Fork_93=0.000000000000000] & Fork_5=0.000000000000000] & Fork_43=0.000000000000000] & Fork_83=0.000000000000000] & Fork_53=0.000000000000000] & Fork_11=0.000000000000000] & Fork_20=0.000000000000000] & Fork_46=0.000000000000000] & Fork_30=0.000000000000000] & Fork_70=0.000000000000000] & Fork_27=0.000000000000000] & Fork_45=0.000000000000000] & Fork_33=0.000000000000000] & Fork_8=0.000000000000000] & Fork_86=0.000000000000000] & Fork_49=0.000000000000000] & Fork_67=0.000000000000000] & Fork_38=0.000000000000000] & Fork_6=0.000000000000000] & Fork_19=0.000000000000000]] & Fork_58=0.000000000000000] & Fork_62=0.000000000000000] & Fork_51=0.000000000000000] & Fork_89=0.000000000000000] & Fork_41=0.000000000000000] & Fork_4=0.000000000000000] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000] & Fork_76=0.000000000000000] & Fork_12=0.000000000000000] & Fork_14=0.000000000000000] & Fork_66=0.000000000000000] & Fork_79=0.000000000000000] & Fork_32=0.000000000000000] & Fork_69=0.000000000000000] & Fork_71=0.000000000000000] & Fork_23=0.000000000000000]] & Fork_88=0.000000000000000] & Fork_99=0.000000000000000] & Fork_90=0.000000000000000]] & Fork_77=0.000000000000000] & Fork_18=0.000000000000000] & Fork_3=0.000000000000000] & Fork_78=0.000000000000000] & Fork_42=0.000000000000000] & Fork_61=0.000000000000000]] & Fork_68=0.000000000000000] & Fork_40=0.000000000000000] & Fork_84=0.000000000000000] & Fork_10=0.000000000000000] & Fork_48=0.000000000000000] & Fork_98=0.000000000000000] & Fork_16=0.000000000000000] & Fork_95=0.000000000000000] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000] & Fork_9=0.000000000000000] & Fork_55=0.000000000000000] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000] & Fork_36=0.000000000000000]]]]
normalized: ~ [EG [~ [E [~ [EG [~ [[Catch2_24=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_77=0.000000000000000 & [Catch2_61=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_91=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_59=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_83=0.000000000000000 & [Catch2_92=0.000000000000000 & [Catch2_100=0.000000000000000 & [Catch2_57=0.000000000000000 & [Catch2_76=0.000000000000000 & [Catch2_51=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_82=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_89=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_81=0.000000000000000 & [Catch2_62=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_53=0.000000000000000 & [Catch2_60=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_71=0.000000000000000 & [Catch2_70=0.000000000000000 & [Catch2_94=0.000000000000000 & [Catch2_58=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_54=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_73=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_55=0.000000000000000 & [Catch2_72=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_75=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_1=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_85=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_93=0.000000000000000 & [Catch2_78=0.000000000000000 & [Catch2_88=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_80=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_98=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_64=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_10=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_52=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_79=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_87=0.000000000000000 & [Catch2_97=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_50=0.000000000000000 & [Catch2_84=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_65=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_90=0.000000000000000 & [Catch2_63=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_74=0.000000000000000 & [Catch2_86=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_68=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_56=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_96=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_95=0.000000000000000 & [Catch2_67=0.000000000000000 & [Catch2_99=0.000000000000000 & [Catch2_66=0.000000000000000 & [1.000000000000000=Catch2_69 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] U EG [[Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [Fork_13=0.000000000000000 & [Fork_55=0.000000000000000 & [Fork_9=0.000000000000000 & [Fork_59=0.000000000000000 & [Fork_97=0.000000000000000 & [Fork_95=0.000000000000000 & [Fork_16=0.000000000000000 & [Fork_98=0.000000000000000 & [Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [Fork_84=0.000000000000000 & [Fork_40=0.000000000000000 & [Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [Fork_61=0.000000000000000 & [Fork_42=0.000000000000000 & [Fork_78=0.000000000000000 & [Fork_3=0.000000000000000 & [Fork_18=0.000000000000000 & [Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_99=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [Fork_32=0.000000000000000 & [Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [Fork_14=0.000000000000000 & [Fork_12=0.000000000000000 & [Fork_76=0.000000000000000 & [Fork_56=0.000000000000000 & [Fork_63=0.000000000000000 & [Fork_4=0.000000000000000 & [Fork_41=0.000000000000000 & [Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [Fork_62=0.000000000000000 & [Fork_58=0.000000000000000 & [Fork_100=0.000000000000000 & [Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [Fork_67=0.000000000000000 & [Fork_49=0.000000000000000 & [Fork_86=0.000000000000000 & [Fork_8=0.000000000000000 & [Fork_33=0.000000000000000 & [Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [Fork_70=0.000000000000000 & [Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [Fork_20=0.000000000000000 & [Fork_11=0.000000000000000 & [Fork_53=0.000000000000000 & [Fork_83=0.000000000000000 & [Fork_43=0.000000000000000 & [Fork_5=0.000000000000000 & [Fork_93=0.000000000000000 & [Fork_7=0.000000000000000 & [Fork_25=0.000000000000000 & [Fork_26=0.000000000000000 & [Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [Fork_28=0.000000000000000 & [Fork_73=0.000000000000000 & [Fork_39=0.000000000000000 & [Fork_87=0.000000000000000 & [Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [Fork_92=0.000000000000000 & [Fork_31=0.000000000000000 & [Fork_21=0.000000000000000 & [Fork_44=0.000000000000000 & [Fork_57=0.000000000000000 & [Fork_2=0.000000000000000 & [Fork_94=0.000000000000000 & [Fork_34=0.000000000000000 & [Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [Fork_1=0.000000000000000 & [Fork_24=0.000000000000000 & [Fork_54=0.000000000000000 & [Fork_15=0.000000000000000 & [Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [Fork_96=0.000000000000000 & [Fork_81=0.000000000000000 & [Fork_52=0.000000000000000 & [1.000000000000000=Fork_75 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1

EG iterations: 0

EG iterations: 0
-> the formula is FALSE

FORMULA p_1870_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[[[[Catch1_58!=0.000000000000000 & [[[[[[[[Catch1_72!=0.000000000000000 & [[[[[[[[[[[[[Catch1_2!=0.000000000000000 & [[[[[Catch1_93!=0.000000000000000 & [[[[[Catch1_16!=0.000000000000000 & [[Catch1_34!=0.000000000000000 & [[[[[Catch1_97!=0.000000000000000 & [[[[[[[[[[[[[Catch1_84!=0.000000000000000 & [[[[[[[[[Catch1_35!=0.000000000000000 & [[Catch1_36!=0.000000000000000 & [[[[[[[Catch1_29!=0.000000000000000 & [[Catch1_41!=0.000000000000000 & [[Catch1_74!=0.000000000000000 & [[[[[[[[[[[Catch1_55!=0.000000000000000 & [[[[[[Catch1_15!=0.000000000000000 & [[Catch1_95!=0.000000000000000 & [[[true & 1.000000000000000!=Catch1_87] & Catch1_90!=0.000000000000000] & Catch1_8!=0.000000000000000]] & Catch1_48!=0.000000000000000]] & Catch1_64!=0.000000000000000] & Catch1_26!=0.000000000000000] & Catch1_96!=0.000000000000000] & Catch1_6!=0.000000000000000] & Catch1_42!=0.000000000000000]] & Catch1_83!=0.000000000000000] & Catch1_94!=0.000000000000000] & Catch1_13!=0.000000000000000] & Catch1_10!=0.000000000000000] & Catch1_71!=0.000000000000000] & Catch1_14!=0.000000000000000] & Catch1_12!=0.000000000000000] & Catch1_69!=0.000000000000000] & Catch1_37!=0.000000000000000] & Catch1_82!=0.000000000000000]] & Catch1_38!=0.000000000000000]] & Catch1_22!=0.000000000000000]] & Catch1_56!=0.000000000000000] & Catch1_59!=0.000000000000000] & Catch1_80!=0.000000000000000] & Catch1_45!=0.000000000000000] & Catch1_46!=0.000000000000000] & Catch1_78!=0.000000000000000]] & Catch1_81!=0.000000000000000]] & Catch1_9!=0.000000000000000] & Catch1_11!=0.000000000000000] & Catch1_89!=0.000000000000000] & Catch1_32!=0.000000000000000] & Catch1_92!=0.000000000000000] & Catch1_75!=0.000000000000000] & Catch1_88!=0.000000000000000] & Catch1_27!=0.000000000000000]] & Catch1_65!=0.000000000000000] & Catch1_68!=0.000000000000000] & Catch1_25!=0.000000000000000] & Catch1_73!=0.000000000000000] & Catch1_50!=0.000000000000000] & Catch1_85!=0.000000000000000] & Catch1_40!=0.000000000000000] & Catch1_52!=0.000000000000000] & Catch1_86!=0.000000000000000] & Catch1_20!=0.000000000000000] & Catch1_91!=0.000000000000000] & Catch1_47!=0.000000000000000]] & Catch1_100!=0.000000000000000] & Catch1_4!=0.000000000000000] & Catch1_3!=0.000000000000000] & Catch1_79!=0.000000000000000]] & Catch1_31!=0.000000000000000]] & Catch1_21!=0.000000000000000] & Catch1_62!=0.000000000000000] & Catch1_49!=0.000000000000000] & Catch1_1!=0.000000000000000]] & Catch1_77!=0.000000000000000] & Catch1_63!=0.000000000000000] & Catch1_70!=0.000000000000000] & Catch1_66!=0.000000000000000]] & Catch1_18!=0.000000000000000] & Catch1_54!=0.000000000000000] & Catch1_57!=0.000000000000000] & Catch1_43!=0.000000000000000] & Catch1_67!=0.000000000000000] & Catch1_7!=0.000000000000000] & Catch1_99!=0.000000000000000] & Catch1_19!=0.000000000000000] & Catch1_33!=0.000000000000000] & Catch1_44!=0.000000000000000] & Catch1_39!=0.000000000000000] & Catch1_24!=0.000000000000000]] & Catch1_23!=0.000000000000000] & Catch1_51!=0.000000000000000] & Catch1_76!=0.000000000000000] & Catch1_28!=0.000000000000000] & Catch1_61!=0.000000000000000] & Catch1_53!=0.000000000000000] & Catch1_17!=0.000000000000000]] & Catch1_5!=0.000000000000000] & Catch1_98!=0.000000000000000] & Catch1_60!=0.000000000000000] & Catch1_30!=0.000000000000000] & [Catch2_24!=0.000000000000000 & [[[[Catch2_69!=0.000000000000000 & [[[[Catch2_32!=0.000000000000000 & [[[[Catch2_59!=0.000000000000000 & [[[[[[Catch2_76!=0.000000000000000 & [[Catch2_41!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[Catch2_36!=0.000000000000000 & [[[[[[[[[[[[[Catch2_88!=0.000000000000000 & [[[[[[[Catch2_31!=0.000000000000000 & [[Catch2_64!=0.000000000000000 & [[Catch2_30!=0.000000000000000 & [[[[[[[[[[[Catch2_50!=0.000000000000000 & [[[[[[[[[[[[[[[[[[Catch2_37!=0.000000000000000 & [[[[[true & 1.000000000000000!=Catch2_40] & Catch2_66!=0.000000000000000] & Catch2_99!=0.000000000000000] & Catch2_67!=0.000000000000000] & Catch2_95!=0.000000000000000]] & Catch2_96!=0.000000000000000] & Catch2_45!=0.000000000000000] & Catch2_56!=0.000000000000000] & Catch2_46!=0.000000000000000] & Catch2_68!=0.000000000000000] & Catch2_21!=0.000000000000000] & Catch2_86!=0.000000000000000] & Catch2_74!=0.000000000000000] & Catch2_5!=0.000000000000000] & Catch2_63!=0.000000000000000] & Catch2_90!=0.000000000000000] & Catch2_3!=0.000000000000000] & Catch2_65!=0.000000000000000] & Catch2_26!=0.000000000000000] & Catch2_7!=0.000000000000000] & Catch2_43!=0.000000000000000] & Catch2_84!=0.000000000000000]] & Catch2_11!=0.000000000000000] & Catch2_38!=0.000000000000000] & Catch2_97!=0.000000000000000] & Catch2_87!=0.000000000000000] & Catch2_49!=0.000000000000000] & Catch2_79!=0.000000000000000] & Catch2_17!=0.000000000000000] & Catch2_52!=0.000000000000000] & Catch2_16!=0.000000000000000] & Catch2_10!=0.000000000000000]] & Catch2_28!=0.000000000000000]] & Catch2_48!=0.000000000000000]] & Catch2_98!=0.000000000000000] & Catch2_13!=0.000000000000000] & Catch2_2!=0.000000000000000] & Catch2_80!=0.000000000000000] & Catch2_14!=0.000000000000000] & Catch2_8!=0.000000000000000]] & Catch2_78!=0.000000000000000] & Catch2_93!=0.000000000000000] & Catch2_42!=0.000000000000000] & Catch2_39!=0.000000000000000] & Catch2_85!=0.000000000000000] & Catch2_20!=0.000000000000000] & Catch2_1!=0.000000000000000] & Catch2_22!=0.000000000000000] & Catch2_75!=0.000000000000000] & Catch2_35!=0.000000000000000] & Catch2_72!=0.000000000000000] & Catch2_55!=0.000000000000000]] & Catch2_73!=0.000000000000000] & Catch2_15!=0.000000000000000] & Catch2_54!=0.000000000000000] & Catch2_6!=0.000000000000000] & Catch2_58!=0.000000000000000] & Catch2_94!=0.000000000000000] & Catch2_70!=0.000000000000000] & Catch2_71!=0.000000000000000] & Catch2_29!=0.000000000000000] & Catch2_60!=0.000000000000000] & Catch2_53!=0.000000000000000] & Catch2_4!=0.000000000000000] & Catch2_44!=0.000000000000000] & Catch2_62!=0.000000000000000] & Catch2_81!=0.000000000000000] & Catch2_12!=0.000000000000000] & Catch2_89!=0.000000000000000] & Catch2_34!=0.000000000000000] & Catch2_82!=0.000000000000000] & Catch2_23!=0.000000000000000]] & Catch2_51!=0.000000000000000]] & Catch2_57!=0.000000000000000] & Catch2_100!=0.000000000000000] & Catch2_92!=0.000000000000000] & Catch2_83!=0.000000000000000] & Catch2_33!=0.000000000000000]] & Catch2_19!=0.000000000000000] & Catch2_91!=0.000000000000000] & Catch2_18!=0.000000000000000]] & Catch2_47!=0.000000000000000] & Catch2_27!=0.000000000000000] & Catch2_9!=0.000000000000000]] & Catch2_61!=0.000000000000000] & Catch2_77!=0.000000000000000] & Catch2_25!=0.000000000000000]]]]
normalized: E [true U [[Catch2_24!=0.000000000000000 & [Catch2_25!=0.000000000000000 & [Catch2_77!=0.000000000000000 & [Catch2_61!=0.000000000000000 & [Catch2_69!=0.000000000000000 & [Catch2_9!=0.000000000000000 & [Catch2_27!=0.000000000000000 & [Catch2_47!=0.000000000000000 & [Catch2_32!=0.000000000000000 & [Catch2_18!=0.000000000000000 & [Catch2_91!=0.000000000000000 & [Catch2_19!=0.000000000000000 & [Catch2_59!=0.000000000000000 & [Catch2_33!=0.000000000000000 & [Catch2_83!=0.000000000000000 & [Catch2_92!=0.000000000000000 & [Catch2_100!=0.000000000000000 & [Catch2_57!=0.000000000000000 & [Catch2_76!=0.000000000000000 & [Catch2_51!=0.000000000000000 & [Catch2_41!=0.000000000000000 & [Catch2_23!=0.000000000000000 & [Catch2_82!=0.000000000000000 & [Catch2_34!=0.000000000000000 & [Catch2_89!=0.000000000000000 & [Catch2_12!=0.000000000000000 & [Catch2_81!=0.000000000000000 & [Catch2_62!=0.000000000000000 & [Catch2_44!=0.000000000000000 & [Catch2_4!=0.000000000000000 & [Catch2_53!=0.000000000000000 & [Catch2_60!=0.000000000000000 & [Catch2_29!=0.000000000000000 & [Catch2_71!=0.000000000000000 & [Catch2_70!=0.000000000000000 & [Catch2_94!=0.000000000000000 & [Catch2_58!=0.000000000000000 & [Catch2_6!=0.000000000000000 & [Catch2_54!=0.000000000000000 & [Catch2_15!=0.000000000000000 & [Catch2_73!=0.000000000000000 & [Catch2_36!=0.000000000000000 & [Catch2_55!=0.000000000000000 & [Catch2_72!=0.000000000000000 & [Catch2_35!=0.000000000000000 & [Catch2_75!=0.000000000000000 & [Catch2_22!=0.000000000000000 & [Catch2_1!=0.000000000000000 & [Catch2_20!=0.000000000000000 & [Catch2_85!=0.000000000000000 & [Catch2_39!=0.000000000000000 & [Catch2_42!=0.000000000000000 & [Catch2_93!=0.000000000000000 & [Catch2_78!=0.000000000000000 & [Catch2_88!=0.000000000000000 & [Catch2_8!=0.000000000000000 & [Catch2_14!=0.000000000000000 & [Catch2_80!=0.000000000000000 & [Catch2_2!=0.000000000000000 & [Catch2_13!=0.000000000000000 & [Catch2_98!=0.000000000000000 & [Catch2_31!=0.000000000000000 & [Catch2_48!=0.000000000000000 & [Catch2_64!=0.000000000000000 & [Catch2_28!=0.000000000000000 & [Catch2_30!=0.000000000000000 & [Catch2_10!=0.000000000000000 & [Catch2_16!=0.000000000000000 & [Catch2_52!=0.000000000000000 & [Catch2_17!=0.000000000000000 & [Catch2_79!=0.000000000000000 & [Catch2_49!=0.000000000000000 & [Catch2_87!=0.000000000000000 & [Catch2_97!=0.000000000000000 & [Catch2_38!=0.000000000000000 & [Catch2_11!=0.000000000000000 & [Catch2_50!=0.000000000000000 & [Catch2_84!=0.000000000000000 & [Catch2_43!=0.000000000000000 & [Catch2_7!=0.000000000000000 & [Catch2_26!=0.000000000000000 & [Catch2_65!=0.000000000000000 & [Catch2_3!=0.000000000000000 & [Catch2_90!=0.000000000000000 & [Catch2_63!=0.000000000000000 & [Catch2_5!=0.000000000000000 & [Catch2_74!=0.000000000000000 & [Catch2_86!=0.000000000000000 & [Catch2_21!=0.000000000000000 & [Catch2_68!=0.000000000000000 & [Catch2_46!=0.000000000000000 & [Catch2_56!=0.000000000000000 & [Catch2_45!=0.000000000000000 & [Catch2_96!=0.000000000000000 & [Catch2_37!=0.000000000000000 & [Catch2_95!=0.000000000000000 & [Catch2_67!=0.000000000000000 & [Catch2_99!=0.000000000000000 & [Catch2_66!=0.000000000000000 & [1.000000000000000!=Catch2_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch1_30!=0.000000000000000 & [Catch1_60!=0.000000000000000 & [Catch1_98!=0.000000000000000 & [Catch1_5!=0.000000000000000 & [Catch1_58!=0.000000000000000 & [Catch1_17!=0.000000000000000 & [Catch1_53!=0.000000000000000 & [Catch1_61!=0.000000000000000 & [Catch1_28!=0.000000000000000 & [Catch1_76!=0.000000000000000 & [Catch1_51!=0.000000000000000 & [Catch1_23!=0.000000000000000 & [Catch1_72!=0.000000000000000 & [Catch1_24!=0.000000000000000 & [Catch1_39!=0.000000000000000 & [Catch1_44!=0.000000000000000 & [Catch1_33!=0.000000000000000 & [Catch1_19!=0.000000000000000 & [Catch1_99!=0.000000000000000 & [Catch1_7!=0.000000000000000 & [Catch1_67!=0.000000000000000 & [Catch1_43!=0.000000000000000 & [Catch1_57!=0.000000000000000 & [Catch1_54!=0.000000000000000 & [Catch1_18!=0.000000000000000 & [Catch1_2!=0.000000000000000 & [Catch1_66!=0.000000000000000 & [Catch1_70!=0.000000000000000 & [Catch1_63!=0.000000000000000 & [Catch1_77!=0.000000000000000 & [Catch1_93!=0.000000000000000 & [Catch1_1!=0.000000000000000 & [Catch1_49!=0.000000000000000 & [Catch1_62!=0.000000000000000 & [Catch1_21!=0.000000000000000 & [Catch1_16!=0.000000000000000 & [Catch1_31!=0.000000000000000 & [Catch1_34!=0.000000000000000 & [Catch1_79!=0.000000000000000 & [Catch1_3!=0.000000000000000 & [Catch1_4!=0.000000000000000 & [Catch1_100!=0.000000000000000 & [Catch1_97!=0.000000000000000 & [Catch1_47!=0.000000000000000 & [Catch1_91!=0.000000000000000 & [Catch1_20!=0.000000000000000 & [Catch1_86!=0.000000000000000 & [Catch1_52!=0.000000000000000 & [Catch1_40!=0.000000000000000 & [Catch1_85!=0.000000000000000 & [Catch1_50!=0.000000000000000 & [Catch1_73!=0.000000000000000 & [Catch1_25!=0.000000000000000 & [Catch1_68!=0.000000000000000 & [Catch1_65!=0.000000000000000 & [Catch1_84!=0.000000000000000 & [Catch1_27!=0.000000000000000 & [Catch1_88!=0.000000000000000 & [Catch1_75!=0.000000000000000 & [Catch1_92!=0.000000000000000 & [Catch1_32!=0.000000000000000 & [Catch1_89!=0.000000000000000 & [Catch1_11!=0.000000000000000 & [Catch1_9!=0.000000000000000 & [Catch1_35!=0.000000000000000 & [Catch1_81!=0.000000000000000 & [Catch1_36!=0.000000000000000 & [Catch1_78!=0.000000000000000 & [Catch1_46!=0.000000000000000 & [Catch1_45!=0.000000000000000 & [Catch1_80!=0.000000000000000 & [Catch1_59!=0.000000000000000 & [Catch1_56!=0.000000000000000 & [Catch1_29!=0.000000000000000 & [Catch1_22!=0.000000000000000 & [Catch1_41!=0.000000000000000 & [Catch1_38!=0.000000000000000 & [Catch1_74!=0.000000000000000 & [Catch1_82!=0.000000000000000 & [Catch1_37!=0.000000000000000 & [Catch1_69!=0.000000000000000 & [Catch1_12!=0.000000000000000 & [Catch1_14!=0.000000000000000 & [Catch1_71!=0.000000000000000 & [Catch1_10!=0.000000000000000 & [Catch1_13!=0.000000000000000 & [Catch1_94!=0.000000000000000 & [Catch1_83!=0.000000000000000 & [Catch1_55!=0.000000000000000 & [Catch1_42!=0.000000000000000 & [Catch1_6!=0.000000000000000 & [Catch1_96!=0.000000000000000 & [Catch1_26!=0.000000000000000 & [Catch1_64!=0.000000000000000 & [Catch1_15!=0.000000000000000 & [Catch1_48!=0.000000000000000 & [Catch1_95!=0.000000000000000 & [Catch1_8!=0.000000000000000 & [Catch1_90!=0.000000000000000 & [1.000000000000000!=Catch1_87 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1871_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch1_2!=0.000000000000000 & [[[[[[[[[Catch1_21!=0.000000000000000 & [[[[[[[[[[[[[Catch1_52!=0.000000000000000 & [[[[[[[[Catch1_84!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[Catch1_22!=0.000000000000000 & [[[[[[[[[[Catch1_10!=0.000000000000000 & [[[[[[[[[[[[[[[true & 1.000000000000000!=Catch1_87] & Catch1_90!=0.000000000000000] & Catch1_8!=0.000000000000000] & Catch1_95!=0.000000000000000] & Catch1_48!=0.000000000000000] & Catch1_15!=0.000000000000000] & Catch1_64!=0.000000000000000] & Catch1_26!=0.000000000000000] & Catch1_96!=0.000000000000000] & Catch1_6!=0.000000000000000] & Catch1_42!=0.000000000000000] & Catch1_55!=0.000000000000000] & Catch1_83!=0.000000000000000] & Catch1_94!=0.000000000000000] & Catch1_13!=0.000000000000000]] & Catch1_71!=0.000000000000000] & Catch1_14!=0.000000000000000] & Catch1_12!=0.000000000000000] & Catch1_69!=0.000000000000000] & Catch1_37!=0.000000000000000] & Catch1_82!=0.000000000000000] & Catch1_74!=0.000000000000000] & Catch1_38!=0.000000000000000] & Catch1_41!=0.000000000000000]] & Catch1_29!=0.000000000000000] & Catch1_56!=0.000000000000000] & Catch1_59!=0.000000000000000] & Catch1_80!=0.000000000000000] & Catch1_45!=0.000000000000000] & Catch1_46!=0.000000000000000] & Catch1_78!=0.000000000000000] & Catch1_36!=0.000000000000000] & Catch1_81!=0.000000000000000] & Catch1_35!=0.000000000000000] & Catch1_9!=0.000000000000000] & Catch1_11!=0.000000000000000] & Catch1_89!=0.000000000000000] & Catch1_32!=0.000000000000000] & Catch1_92!=0.000000000000000] & Catch1_75!=0.000000000000000] & Catch1_88!=0.000000000000000] & Catch1_27!=0.000000000000000]] & Catch1_65!=0.000000000000000] & Catch1_68!=0.000000000000000] & Catch1_25!=0.000000000000000] & Catch1_73!=0.000000000000000] & Catch1_50!=0.000000000000000] & Catch1_85!=0.000000000000000] & Catch1_40!=0.000000000000000]] & Catch1_86!=0.000000000000000] & Catch1_20!=0.000000000000000] & Catch1_91!=0.000000000000000] & Catch1_47!=0.000000000000000] & Catch1_97!=0.000000000000000] & Catch1_100!=0.000000000000000] & Catch1_4!=0.000000000000000] & Catch1_3!=0.000000000000000] & Catch1_79!=0.000000000000000] & Catch1_34!=0.000000000000000] & Catch1_31!=0.000000000000000] & Catch1_16!=0.000000000000000]] & Catch1_62!=0.000000000000000] & Catch1_49!=0.000000000000000] & Catch1_1!=0.000000000000000] & Catch1_93!=0.000000000000000] & Catch1_77!=0.000000000000000] & Catch1_63!=0.000000000000000] & Catch1_70!=0.000000000000000] & Catch1_66!=0.000000000000000]] & Catch1_18!=0.000000000000000] & Catch1_54!=0.000000000000000] & Catch1_57!=0.000000000000000] & Catch1_43!=0.000000000000000] & Catch1_67!=0.000000000000000] & Catch1_7!=0.000000000000000] & Catch1_99!=0.000000000000000] & Catch1_19!=0.000000000000000] & Catch1_33!=0.000000000000000] & Catch1_44!=0.000000000000000] & Catch1_39!=0.000000000000000] & Catch1_24!=0.000000000000000] & Catch1_72!=0.000000000000000] & Catch1_23!=0.000000000000000] & Catch1_51!=0.000000000000000] & Catch1_76!=0.000000000000000] & Catch1_28!=0.000000000000000] & Catch1_61!=0.000000000000000] & Catch1_53!=0.000000000000000] & Catch1_17!=0.000000000000000] & Catch1_58!=0.000000000000000] & Catch1_5!=0.000000000000000] & Catch1_98!=0.000000000000000] & Catch1_60!=0.000000000000000] & Catch1_30!=0.000000000000000] | [[[[[[[Catch2_27!=0.000000000000000 & [[[[[[[[[Catch2_92!=0.000000000000000 & [[[Catch2_76!=0.000000000000000 & [[[Catch2_23!=0.000000000000000 & [[[[[[Catch2_62!=0.000000000000000 & [[[[[[[[[[[Catch2_54!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[Catch2_2!=0.000000000000000 & [[[[[[[[[[[[[[[[Catch2_38!=0.000000000000000 & [[[[[[[[[[[[[[[[[[Catch2_45!=0.000000000000000 & [[[[[[[true & 1.000000000000000!=Catch2_40] & Catch2_66!=0.000000000000000] & Catch2_99!=0.000000000000000] & Catch2_67!=0.000000000000000] & Catch2_95!=0.000000000000000] & Catch2_37!=0.000000000000000] & Catch2_96!=0.000000000000000]] & Catch2_56!=0.000000000000000] & Catch2_46!=0.000000000000000] & Catch2_68!=0.000000000000000] & Catch2_21!=0.000000000000000] & Catch2_86!=0.000000000000000] & Catch2_74!=0.000000000000000] & Catch2_5!=0.000000000000000] & Catch2_63!=0.000000000000000] & Catch2_90!=0.000000000000000] & Catch2_3!=0.000000000000000] & Catch2_65!=0.000000000000000] & Catch2_26!=0.000000000000000] & Catch2_7!=0.000000000000000] & Catch2_43!=0.000000000000000] & Catch2_84!=0.000000000000000] & Catch2_50!=0.000000000000000] & Catch2_11!=0.000000000000000]] & Catch2_97!=0.000000000000000] & Catch2_87!=0.000000000000000] & Catch2_49!=0.000000000000000] & Catch2_79!=0.000000000000000] & Catch2_17!=0.000000000000000] & Catch2_52!=0.000000000000000] & Catch2_16!=0.000000000000000] & Catch2_10!=0.000000000000000] & Catch2_30!=0.000000000000000] & Catch2_28!=0.000000000000000] & Catch2_64!=0.000000000000000] & Catch2_48!=0.000000000000000] & Catch2_31!=0.000000000000000] & Catch2_98!=0.000000000000000] & Catch2_13!=0.000000000000000]] & Catch2_80!=0.000000000000000] & Catch2_14!=0.000000000000000] & Catch2_8!=0.000000000000000] & Catch2_88!=0.000000000000000] & Catch2_78!=0.000000000000000] & Catch2_93!=0.000000000000000] & Catch2_42!=0.000000000000000] & Catch2_39!=0.000000000000000] & Catch2_85!=0.000000000000000] & Catch2_20!=0.000000000000000] & Catch2_1!=0.000000000000000] & Catch2_22!=0.000000000000000] & Catch2_75!=0.000000000000000] & Catch2_35!=0.000000000000000] & Catch2_72!=0.000000000000000] & Catch2_55!=0.000000000000000] & Catch2_36!=0.000000000000000] & Catch2_73!=0.000000000000000] & Catch2_15!=0.000000000000000]] & Catch2_6!=0.000000000000000] & Catch2_58!=0.000000000000000] & Catch2_94!=0.000000000000000] & Catch2_70!=0.000000000000000] & Catch2_71!=0.000000000000000] & Catch2_29!=0.000000000000000] & Catch2_60!=0.000000000000000] & Catch2_53!=0.000000000000000] & Catch2_4!=0.000000000000000] & Catch2_44!=0.000000000000000]] & Catch2_81!=0.000000000000000] & Catch2_12!=0.000000000000000] & Catch2_89!=0.000000000000000] & Catch2_34!=0.000000000000000] & Catch2_82!=0.000000000000000]] & Catch2_41!=0.000000000000000] & Catch2_51!=0.000000000000000]] & Catch2_57!=0.000000000000000] & Catch2_100!=0.000000000000000]] & Catch2_83!=0.000000000000000] & Catch2_33!=0.000000000000000] & Catch2_59!=0.000000000000000] & Catch2_19!=0.000000000000000] & Catch2_91!=0.000000000000000] & Catch2_18!=0.000000000000000] & Catch2_32!=0.000000000000000] & Catch2_47!=0.000000000000000]] & Catch2_9!=0.000000000000000] & Catch2_69!=0.000000000000000] & Catch2_61!=0.000000000000000] & Catch2_77!=0.000000000000000] & Catch2_25!=0.000000000000000] & Catch2_24!=0.000000000000000]]]
normalized: ~ [EG [~ [[[Catch2_24!=0.000000000000000 & [Catch2_25!=0.000000000000000 & [Catch2_77!=0.000000000000000 & [Catch2_61!=0.000000000000000 & [Catch2_69!=0.000000000000000 & [Catch2_9!=0.000000000000000 & [Catch2_27!=0.000000000000000 & [Catch2_47!=0.000000000000000 & [Catch2_32!=0.000000000000000 & [Catch2_18!=0.000000000000000 & [Catch2_91!=0.000000000000000 & [Catch2_19!=0.000000000000000 & [Catch2_59!=0.000000000000000 & [Catch2_33!=0.000000000000000 & [Catch2_83!=0.000000000000000 & [Catch2_92!=0.000000000000000 & [Catch2_100!=0.000000000000000 & [Catch2_57!=0.000000000000000 & [Catch2_76!=0.000000000000000 & [Catch2_51!=0.000000000000000 & [Catch2_41!=0.000000000000000 & [Catch2_23!=0.000000000000000 & [Catch2_82!=0.000000000000000 & [Catch2_34!=0.000000000000000 & [Catch2_89!=0.000000000000000 & [Catch2_12!=0.000000000000000 & [Catch2_81!=0.000000000000000 & [Catch2_62!=0.000000000000000 & [Catch2_44!=0.000000000000000 & [Catch2_4!=0.000000000000000 & [Catch2_53!=0.000000000000000 & [Catch2_60!=0.000000000000000 & [Catch2_29!=0.000000000000000 & [Catch2_71!=0.000000000000000 & [Catch2_70!=0.000000000000000 & [Catch2_94!=0.000000000000000 & [Catch2_58!=0.000000000000000 & [Catch2_6!=0.000000000000000 & [Catch2_54!=0.000000000000000 & [Catch2_15!=0.000000000000000 & [Catch2_73!=0.000000000000000 & [Catch2_36!=0.000000000000000 & [Catch2_55!=0.000000000000000 & [Catch2_72!=0.000000000000000 & [Catch2_35!=0.000000000000000 & [Catch2_75!=0.000000000000000 & [Catch2_22!=0.000000000000000 & [Catch2_1!=0.000000000000000 & [Catch2_20!=0.000000000000000 & [Catch2_85!=0.000000000000000 & [Catch2_39!=0.000000000000000 & [Catch2_42!=0.000000000000000 & [Catch2_93!=0.000000000000000 & [Catch2_78!=0.000000000000000 & [Catch2_88!=0.000000000000000 & [Catch2_8!=0.000000000000000 & [Catch2_14!=0.000000000000000 & [Catch2_80!=0.000000000000000 & [Catch2_2!=0.000000000000000 & [Catch2_13!=0.000000000000000 & [Catch2_98!=0.000000000000000 & [Catch2_31!=0.000000000000000 & [Catch2_48!=0.000000000000000 & [Catch2_64!=0.000000000000000 & [Catch2_28!=0.000000000000000 & [Catch2_30!=0.000000000000000 & [Catch2_10!=0.000000000000000 & [Catch2_16!=0.000000000000000 & [Catch2_52!=0.000000000000000 & [Catch2_17!=0.000000000000000 & [Catch2_79!=0.000000000000000 & [Catch2_49!=0.000000000000000 & [Catch2_87!=0.000000000000000 & [Catch2_97!=0.000000000000000 & [Catch2_38!=0.000000000000000 & [Catch2_11!=0.000000000000000 & [Catch2_50!=0.000000000000000 & [Catch2_84!=0.000000000000000 & [Catch2_43!=0.000000000000000 & [Catch2_7!=0.000000000000000 & [Catch2_26!=0.000000000000000 & [Catch2_65!=0.000000000000000 & [Catch2_3!=0.000000000000000 & [Catch2_90!=0.000000000000000 & [Catch2_63!=0.000000000000000 & [Catch2_5!=0.000000000000000 & [Catch2_74!=0.000000000000000 & [Catch2_86!=0.000000000000000 & [Catch2_21!=0.000000000000000 & [Catch2_68!=0.000000000000000 & [Catch2_46!=0.000000000000000 & [Catch2_56!=0.000000000000000 & [Catch2_45!=0.000000000000000 & [Catch2_96!=0.000000000000000 & [Catch2_37!=0.000000000000000 & [Catch2_95!=0.000000000000000 & [Catch2_67!=0.000000000000000 & [Catch2_99!=0.000000000000000 & [Catch2_66!=0.000000000000000 & [1.000000000000000!=Catch2_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch1_30!=0.000000000000000 & [Catch1_60!=0.000000000000000 & [Catch1_98!=0.000000000000000 & [Catch1_5!=0.000000000000000 & [Catch1_58!=0.000000000000000 & [Catch1_17!=0.000000000000000 & [Catch1_53!=0.000000000000000 & [Catch1_61!=0.000000000000000 & [Catch1_28!=0.000000000000000 & [Catch1_76!=0.000000000000000 & [Catch1_51!=0.000000000000000 & [Catch1_23!=0.000000000000000 & [Catch1_72!=0.000000000000000 & [Catch1_24!=0.000000000000000 & [Catch1_39!=0.000000000000000 & [Catch1_44!=0.000000000000000 & [Catch1_33!=0.000000000000000 & [Catch1_19!=0.000000000000000 & [Catch1_99!=0.000000000000000 & [Catch1_7!=0.000000000000000 & [Catch1_67!=0.000000000000000 & [Catch1_43!=0.000000000000000 & [Catch1_57!=0.000000000000000 & [Catch1_54!=0.000000000000000 & [Catch1_18!=0.000000000000000 & [Catch1_2!=0.000000000000000 & [Catch1_66!=0.000000000000000 & [Catch1_70!=0.000000000000000 & [Catch1_63!=0.000000000000000 & [Catch1_77!=0.000000000000000 & [Catch1_93!=0.000000000000000 & [Catch1_1!=0.000000000000000 & [Catch1_49!=0.000000000000000 & [Catch1_62!=0.000000000000000 & [Catch1_21!=0.000000000000000 & [Catch1_16!=0.000000000000000 & [Catch1_31!=0.000000000000000 & [Catch1_34!=0.000000000000000 & [Catch1_79!=0.000000000000000 & [Catch1_3!=0.000000000000000 & [Catch1_4!=0.000000000000000 & [Catch1_100!=0.000000000000000 & [Catch1_97!=0.000000000000000 & [Catch1_47!=0.000000000000000 & [Catch1_91!=0.000000000000000 & [Catch1_20!=0.000000000000000 & [Catch1_86!=0.000000000000000 & [Catch1_52!=0.000000000000000 & [Catch1_40!=0.000000000000000 & [Catch1_85!=0.000000000000000 & [Catch1_50!=0.000000000000000 & [Catch1_73!=0.000000000000000 & [Catch1_25!=0.000000000000000 & [Catch1_68!=0.000000000000000 & [Catch1_65!=0.000000000000000 & [Catch1_84!=0.000000000000000 & [Catch1_27!=0.000000000000000 & [Catch1_88!=0.000000000000000 & [Catch1_75!=0.000000000000000 & [Catch1_92!=0.000000000000000 & [Catch1_32!=0.000000000000000 & [Catch1_89!=0.000000000000000 & [Catch1_11!=0.000000000000000 & [Catch1_9!=0.000000000000000 & [Catch1_35!=0.000000000000000 & [Catch1_81!=0.000000000000000 & [Catch1_36!=0.000000000000000 & [Catch1_78!=0.000000000000000 & [Catch1_46!=0.000000000000000 & [Catch1_45!=0.000000000000000 & [Catch1_80!=0.000000000000000 & [Catch1_59!=0.000000000000000 & [Catch1_56!=0.000000000000000 & [Catch1_29!=0.000000000000000 & [Catch1_22!=0.000000000000000 & [Catch1_41!=0.000000000000000 & [Catch1_38!=0.000000000000000 & [Catch1_74!=0.000000000000000 & [Catch1_82!=0.000000000000000 & [Catch1_37!=0.000000000000000 & [Catch1_69!=0.000000000000000 & [Catch1_12!=0.000000000000000 & [Catch1_14!=0.000000000000000 & [Catch1_71!=0.000000000000000 & [Catch1_10!=0.000000000000000 & [Catch1_13!=0.000000000000000 & [Catch1_94!=0.000000000000000 & [Catch1_83!=0.000000000000000 & [Catch1_55!=0.000000000000000 & [Catch1_42!=0.000000000000000 & [Catch1_6!=0.000000000000000 & [Catch1_96!=0.000000000000000 & [Catch1_26!=0.000000000000000 & [Catch1_64!=0.000000000000000 & [Catch1_15!=0.000000000000000 & [Catch1_48!=0.000000000000000 & [Catch1_95!=0.000000000000000 & [Catch1_8!=0.000000000000000 & [Catch1_90!=0.000000000000000 & [1.000000000000000!=Catch1_87 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1872_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=Catch2_40] & Catch2_66!=0.000000000000000] & Catch2_99!=0.000000000000000] & Catch2_67!=0.000000000000000] & Catch2_95!=0.000000000000000] & Catch2_37!=0.000000000000000] & Catch2_96!=0.000000000000000] & Catch2_45!=0.000000000000000] & Catch2_56!=0.000000000000000] & Catch2_46!=0.000000000000000] & Catch2_68!=0.000000000000000] & Catch2_21!=0.000000000000000] & Catch2_86!=0.000000000000000] & Catch2_74!=0.000000000000000] & Catch2_5!=0.000000000000000] & Catch2_63!=0.000000000000000] & Catch2_90!=0.000000000000000] & Catch2_3!=0.000000000000000] & Catch2_65!=0.000000000000000] & Catch2_26!=0.000000000000000] & Catch2_7!=0.000000000000000] & Catch2_43!=0.000000000000000] & Catch2_84!=0.000000000000000] & Catch2_50!=0.000000000000000] & Catch2_11!=0.000000000000000] & Catch2_38!=0.000000000000000] & Catch2_97!=0.000000000000000] & Catch2_87!=0.000000000000000] & Catch2_49!=0.000000000000000] & Catch2_79!=0.000000000000000] & Catch2_17!=0.000000000000000] & Catch2_52!=0.000000000000000] & Catch2_16!=0.000000000000000] & Catch2_10!=0.000000000000000] & Catch2_30!=0.000000000000000] & Catch2_28!=0.000000000000000] & Catch2_64!=0.000000000000000] & Catch2_48!=0.000000000000000] & Catch2_31!=0.000000000000000] & Catch2_98!=0.000000000000000] & Catch2_13!=0.000000000000000] & Catch2_2!=0.000000000000000] & Catch2_80!=0.000000000000000] & Catch2_14!=0.000000000000000] & Catch2_8!=0.000000000000000] & Catch2_88!=0.000000000000000] & Catch2_78!=0.000000000000000] & Catch2_93!=0.000000000000000] & Catch2_42!=0.000000000000000] & Catch2_39!=0.000000000000000] & Catch2_85!=0.000000000000000] & Catch2_20!=0.000000000000000] & Catch2_1!=0.000000000000000] & Catch2_22!=0.000000000000000] & Catch2_75!=0.000000000000000] & Catch2_35!=0.000000000000000] & Catch2_72!=0.000000000000000] & Catch2_55!=0.000000000000000] & Catch2_36!=0.000000000000000] & Catch2_73!=0.000000000000000] & Catch2_15!=0.000000000000000] & Catch2_54!=0.000000000000000] & Catch2_6!=0.000000000000000] & Catch2_58!=0.000000000000000] & Catch2_94!=0.000000000000000] & Catch2_70!=0.000000000000000] & Catch2_71!=0.000000000000000] & Catch2_29!=0.000000000000000] & Catch2_60!=0.000000000000000] & Catch2_53!=0.000000000000000] & Catch2_4!=0.000000000000000] & Catch2_44!=0.000000000000000] & Catch2_62!=0.000000000000000] & Catch2_81!=0.000000000000000] & Catch2_12!=0.000000000000000] & Catch2_89!=0.000000000000000] & Catch2_34!=0.000000000000000] & Catch2_82!=0.000000000000000] & Catch2_23!=0.000000000000000] & Catch2_41!=0.000000000000000] & Catch2_51!=0.000000000000000] & Catch2_76!=0.000000000000000] & Catch2_57!=0.000000000000000] & Catch2_100!=0.000000000000000] & Catch2_92!=0.000000000000000] & Catch2_83!=0.000000000000000] & Catch2_33!=0.000000000000000] & Catch2_59!=0.000000000000000] & Catch2_19!=0.000000000000000] & Catch2_91!=0.000000000000000] & Catch2_18!=0.000000000000000] & Catch2_32!=0.000000000000000] & Catch2_47!=0.000000000000000] & Catch2_27!=0.000000000000000] & Catch2_9!=0.000000000000000] & Catch2_69!=0.000000000000000] & Catch2_61!=0.000000000000000] & Catch2_77!=0.000000000000000] & Catch2_25!=0.000000000000000] & Catch2_24!=0.000000000000000] & ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=Catch1_87] & Catch1_90!=0.000000000000000] & Catch1_8!=0.000000000000000] & Catch1_95!=0.000000000000000] & Catch1_48!=0.000000000000000] & Catch1_15!=0.000000000000000] & Catch1_64!=0.000000000000000] & Catch1_26!=0.000000000000000] & Catch1_96!=0.000000000000000] & Catch1_6!=0.000000000000000] & Catch1_42!=0.000000000000000] & Catch1_55!=0.000000000000000] & Catch1_83!=0.000000000000000] & Catch1_94!=0.000000000000000] & Catch1_13!=0.000000000000000] & Catch1_10!=0.000000000000000] & Catch1_71!=0.000000000000000] & Catch1_14!=0.000000000000000] & Catch1_12!=0.000000000000000] & Catch1_69!=0.000000000000000] & Catch1_37!=0.000000000000000] & Catch1_82!=0.000000000000000] & Catch1_74!=0.000000000000000] & Catch1_38!=0.000000000000000] & Catch1_41!=0.000000000000000] & Catch1_22!=0.000000000000000] & Catch1_29!=0.000000000000000] & Catch1_56!=0.000000000000000] & Catch1_59!=0.000000000000000] & Catch1_80!=0.000000000000000] & Catch1_45!=0.000000000000000] & Catch1_46!=0.000000000000000] & Catch1_78!=0.000000000000000] & Catch1_36!=0.000000000000000] & Catch1_81!=0.000000000000000] & Catch1_35!=0.000000000000000] & Catch1_9!=0.000000000000000] & Catch1_11!=0.000000000000000] & Catch1_89!=0.000000000000000] & Catch1_32!=0.000000000000000] & Catch1_92!=0.000000000000000] & Catch1_75!=0.000000000000000] & Catch1_88!=0.000000000000000] & Catch1_27!=0.000000000000000] & Catch1_84!=0.000000000000000] & Catch1_65!=0.000000000000000] & Catch1_68!=0.000000000000000] & Catch1_25!=0.000000000000000] & Catch1_73!=0.000000000000000] & Catch1_50!=0.000000000000000] & Catch1_85!=0.000000000000000] & Catch1_40!=0.000000000000000] & Catch1_52!=0.000000000000000] & Catch1_86!=0.000000000000000] & Catch1_20!=0.000000000000000] & Catch1_91!=0.000000000000000] & Catch1_47!=0.000000000000000] & Catch1_97!=0.000000000000000] & Catch1_100!=0.000000000000000] & Catch1_4!=0.000000000000000] & Catch1_3!=0.000000000000000] & Catch1_79!=0.000000000000000] & Catch1_34!=0.000000000000000] & Catch1_31!=0.000000000000000] & Catch1_16!=0.000000000000000] & Catch1_21!=0.000000000000000] & Catch1_62!=0.000000000000000] & Catch1_49!=0.000000000000000] & Catch1_1!=0.000000000000000] & Catch1_93!=0.000000000000000] & Catch1_77!=0.000000000000000] & Catch1_63!=0.000000000000000] & Catch1_70!=0.000000000000000] & Catch1_66!=0.000000000000000] & Catch1_2!=0.000000000000000] & Catch1_18!=0.000000000000000] & Catch1_54!=0.000000000000000] & Catch1_57!=0.000000000000000] & Catch1_43!=0.000000000000000] & Catch1_67!=0.000000000000000] & Catch1_7!=0.000000000000000] & Catch1_99!=0.000000000000000] & Catch1_19!=0.000000000000000] & Catch1_33!=0.000000000000000] & Catch1_44!=0.000000000000000] & Catch1_39!=0.000000000000000] & Catch1_24!=0.000000000000000] & Catch1_72!=0.000000000000000] & Catch1_23!=0.000000000000000] & Catch1_51!=0.000000000000000] & Catch1_76!=0.000000000000000] & Catch1_28!=0.000000000000000] & Catch1_61!=0.000000000000000] & Catch1_53!=0.000000000000000] & Catch1_17!=0.000000000000000] & Catch1_58!=0.000000000000000] & Catch1_5!=0.000000000000000] & Catch1_98!=0.000000000000000] & Catch1_60!=0.000000000000000] & Catch1_30!=0.000000000000000]]]]
normalized: EG [[~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=Catch1_87] & Catch1_90!=0.000000000000000] & Catch1_8!=0.000000000000000] & Catch1_95!=0.000000000000000] & Catch1_48!=0.000000000000000] & Catch1_15!=0.000000000000000] & Catch1_64!=0.000000000000000] & Catch1_26!=0.000000000000000] & Catch1_96!=0.000000000000000] & Catch1_6!=0.000000000000000] & Catch1_42!=0.000000000000000] & Catch1_55!=0.000000000000000] & Catch1_83!=0.000000000000000] & Catch1_94!=0.000000000000000] & Catch1_13!=0.000000000000000] & Catch1_10!=0.000000000000000] & Catch1_71!=0.000000000000000] & Catch1_14!=0.000000000000000] & Catch1_12!=0.000000000000000] & Catch1_69!=0.000000000000000] & Catch1_37!=0.000000000000000] & Catch1_82!=0.000000000000000] & Catch1_74!=0.000000000000000] & Catch1_38!=0.000000000000000] & Catch1_41!=0.000000000000000] & Catch1_22!=0.000000000000000] & Catch1_29!=0.000000000000000] & Catch1_56!=0.000000000000000] & Catch1_59!=0.000000000000000] & Catch1_80!=0.000000000000000] & Catch1_45!=0.000000000000000] & Catch1_46!=0.000000000000000] & Catch1_78!=0.000000000000000] & Catch1_36!=0.000000000000000] & Catch1_81!=0.000000000000000] & Catch1_35!=0.000000000000000] & Catch1_9!=0.000000000000000] & Catch1_11!=0.000000000000000] & Catch1_89!=0.000000000000000] & Catch1_32!=0.000000000000000] & Catch1_92!=0.000000000000000] & Catch1_75!=0.000000000000000] & Catch1_88!=0.000000000000000] & Catch1_27!=0.000000000000000] & Catch1_84!=0.000000000000000] & Catch1_65!=0.000000000000000] & Catch1_68!=0.000000000000000] & Catch1_25!=0.000000000000000] & Catch1_73!=0.000000000000000] & Catch1_50!=0.000000000000000] & Catch1_85!=0.000000000000000] & Catch1_40!=0.000000000000000] & Catch1_52!=0.000000000000000] & Catch1_86!=0.000000000000000] & Catch1_20!=0.000000000000000] & Catch1_91!=0.000000000000000] & Catch1_47!=0.000000000000000] & Catch1_97!=0.000000000000000] & Catch1_100!=0.000000000000000] & Catch1_4!=0.000000000000000] & Catch1_3!=0.000000000000000] & Catch1_79!=0.000000000000000] & Catch1_34!=0.000000000000000] & Catch1_31!=0.000000000000000] & Catch1_16!=0.000000000000000] & Catch1_21!=0.000000000000000] & Catch1_62!=0.000000000000000] & Catch1_49!=0.000000000000000] & Catch1_1!=0.000000000000000] & Catch1_93!=0.000000000000000] & Catch1_77!=0.000000000000000] & Catch1_63!=0.000000000000000] & Catch1_70!=0.000000000000000] & Catch1_66!=0.000000000000000] & Catch1_2!=0.000000000000000] & Catch1_18!=0.000000000000000] & Catch1_54!=0.000000000000000] & Catch1_57!=0.000000000000000] & Catch1_43!=0.000000000000000] & Catch1_67!=0.000000000000000] & Catch1_7!=0.000000000000000] & Catch1_99!=0.000000000000000] & Catch1_19!=0.000000000000000] & Catch1_33!=0.000000000000000] & Catch1_44!=0.000000000000000] & Catch1_39!=0.000000000000000] & Catch1_24!=0.000000000000000] & Catch1_72!=0.000000000000000] & Catch1_23!=0.000000000000000] & Catch1_51!=0.000000000000000] & Catch1_76!=0.000000000000000] & Catch1_28!=0.000000000000000] & Catch1_61!=0.000000000000000] & Catch1_53!=0.000000000000000] & Catch1_17!=0.000000000000000] & Catch1_58!=0.000000000000000] & Catch1_5!=0.000000000000000] & Catch1_98!=0.000000000000000] & Catch1_60!=0.000000000000000] & Catch1_30!=0.000000000000000]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_73!=0.000000000000000 & [Catch2_36!=0.000000000000000 & [Catch2_55!=0.000000000000000 & [Catch2_72!=0.000000000000000 & [Catch2_35!=0.000000000000000 & [Catch2_75!=0.000000000000000 & [Catch2_22!=0.000000000000000 & [Catch2_1!=0.000000000000000 & [Catch2_20!=0.000000000000000 & [Catch2_85!=0.000000000000000 & [Catch2_39!=0.000000000000000 & [Catch2_42!=0.000000000000000 & [Catch2_93!=0.000000000000000 & [Catch2_78!=0.000000000000000 & [Catch2_88!=0.000000000000000 & [Catch2_8!=0.000000000000000 & [Catch2_14!=0.000000000000000 & [Catch2_80!=0.000000000000000 & [Catch2_2!=0.000000000000000 & [Catch2_13!=0.000000000000000 & [Catch2_98!=0.000000000000000 & [Catch2_31!=0.000000000000000 & [Catch2_48!=0.000000000000000 & [Catch2_64!=0.000000000000000 & [Catch2_28!=0.000000000000000 & [Catch2_30!=0.000000000000000 & [Catch2_10!=0.000000000000000 & [Catch2_16!=0.000000000000000 & [Catch2_52!=0.000000000000000 & [Catch2_17!=0.000000000000000 & [Catch2_79!=0.000000000000000 & [Catch2_49!=0.000000000000000 & [Catch2_87!=0.000000000000000 & [Catch2_97!=0.000000000000000 & [Catch2_38!=0.000000000000000 & [Catch2_11!=0.000000000000000 & [Catch2_50!=0.000000000000000 & [Catch2_84!=0.000000000000000 & [Catch2_43!=0.000000000000000 & [Catch2_7!=0.000000000000000 & [Catch2_26!=0.000000000000000 & [Catch2_65!=0.000000000000000 & [Catch2_3!=0.000000000000000 & [Catch2_90!=0.000000000000000 & [Catch2_63!=0.000000000000000 & [Catch2_5!=0.000000000000000 & [Catch2_74!=0.000000000000000 & [Catch2_86!=0.000000000000000 & [Catch2_21!=0.000000000000000 & [Catch2_68!=0.000000000000000 & [Catch2_46!=0.000000000000000 & [Catch2_56!=0.000000000000000 & [Catch2_45!=0.000000000000000 & [Catch2_96!=0.000000000000000 & [Catch2_37!=0.000000000000000 & [Catch2_95!=0.000000000000000 & [Catch2_67!=0.000000000000000 & [Catch2_99!=0.000000000000000 & [Catch2_66!=0.000000000000000 & [1.000000000000000!=Catch2_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Catch2_15!=0.000000000000000] & Catch2_54!=0.000000000000000] & Catch2_6!=0.000000000000000] & Catch2_58!=0.000000000000000] & Catch2_94!=0.000000000000000] & Catch2_70!=0.000000000000000] & Catch2_71!=0.000000000000000] & Catch2_29!=0.000000000000000] & Catch2_60!=0.000000000000000] & Catch2_53!=0.000000000000000] & Catch2_4!=0.000000000000000] & Catch2_44!=0.000000000000000] & Catch2_62!=0.000000000000000] & Catch2_81!=0.000000000000000] & Catch2_12!=0.000000000000000] & Catch2_89!=0.000000000000000] & Catch2_34!=0.000000000000000] & Catch2_82!=0.000000000000000] & Catch2_23!=0.000000000000000] & Catch2_41!=0.000000000000000] & Catch2_51!=0.000000000000000] & Catch2_76!=0.000000000000000] & Catch2_57!=0.000000000000000] & Catch2_100!=0.000000000000000] & Catch2_92!=0.000000000000000] & Catch2_83!=0.000000000000000] & Catch2_33!=0.000000000000000] & Catch2_59!=0.000000000000000] & Catch2_19!=0.000000000000000] & Catch2_91!=0.000000000000000] & Catch2_18!=0.000000000000000] & Catch2_32!=0.000000000000000] & Catch2_47!=0.000000000000000] & Catch2_27!=0.000000000000000] & Catch2_9!=0.000000000000000] & Catch2_69!=0.000000000000000] & Catch2_61!=0.000000000000000] & Catch2_77!=0.000000000000000] & Catch2_25!=0.000000000000000] & Catch2_24!=0.000000000000000]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1873_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m10sec

STOP 1369718833

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

952 2216
iterations count:2292 (4), effective:300 (0)

initing FirstDep: 0m0sec


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