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=ReachabilityMarkingComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1657
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 ReachabilityMarkingComparison'
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=136968525000138_n_2)
=====================================================================
runnning marcie on Philosophers-PT-000100 (ReachabilityMarkingComparison)
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 ReachabilityMarkingComparison
=====================================================================

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

START 1369702593

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=ReachabilityMarkingComparison.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: AG [[[Fork_36=0.000000000000000 & [[[Fork_55=0.000000000000000 & [[[[Fork_95=0.000000000000000 & [[[Fork_48=0.000000000000000 & [Fork_10=0.000000000000000 & [[Fork_40=0.000000000000000 & [[[[[[[[Fork_77=0.000000000000000 & [Fork_82=0.000000000000000 & [[[[[Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [[Fork_79=0.000000000000000 & [Fork_66=0.000000000000000 & [[[[[[Fork_4=0.000000000000000 & [[Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [[[Fork_100=0.000000000000000 & [[Fork_6=0.000000000000000 & [Fork_38=0.000000000000000 & [[Fork_49=0.000000000000000 & [[[[Fork_45=0.000000000000000 & [[[[Fork_46=0.000000000000000 & [[[[Fork_83=0.000000000000000 & [[Fork_5=0.000000000000000 & [[[[[Fork_65=0.000000000000000 & [[[Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [Fork_35=0.000000000000000 & [[[[[Fork_37=0.000000000000000 & [Fork_22=0.000000000000000 & [[[Fork_21=0.000000000000000 & [[[[[Fork_94=0.000000000000000 & [[[[[[[[[[Fork_96=0.000000000000000 & [[Fork_52=0.000000000000000 & [1.000000000000000=Fork_99 & true]] & Fork_81=0.000000000000000]] & Fork_74=0.000000000000000] & Fork_80=0.000000000000000] & Fork_15=0.000000000000000] & Fork_54=0.000000000000000] & Fork_24=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_75=0.000000000000000] & Fork_44=0.000000000000000]] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000]]] & Fork_87=0.000000000000000] & Fork_39=0.000000000000000] & Fork_73=0.000000000000000] & Fork_28=0.000000000000000]]]] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000]] & Fork_26=0.000000000000000] & Fork_25=0.000000000000000] & Fork_7=0.000000000000000] & Fork_93=0.000000000000000]] & Fork_43=0.000000000000000]] & Fork_53=0.000000000000000] & Fork_11=0.000000000000000] & Fork_20=0.000000000000000]] & Fork_30=0.000000000000000] & Fork_70=0.000000000000000] & Fork_27=0.000000000000000]] & Fork_33=0.000000000000000] & Fork_8=0.000000000000000] & Fork_86=0.000000000000000]] & Fork_67=0.000000000000000]]] & Fork_19=0.000000000000000]] & Fork_58=0.000000000000000] & Fork_62=0.000000000000000]]] & Fork_41=0.000000000000000]] & Fork_63=0.000000000000000] & Fork_56=0.000000000000000] & Fork_76=0.000000000000000] & Fork_12=0.000000000000000] & Fork_14=0.000000000000000]]] & Fork_32=0.000000000000000]]] & Fork_23=0.000000000000000] & Fork_64=0.000000000000000] & Fork_88=0.000000000000000] & Fork_90=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_84=0.000000000000000]]] & Fork_98=0.000000000000000] & Fork_16=0.000000000000000]] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000] & Fork_9=0.000000000000000]] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000]] & [[[[[[[[[[Catch1_76=0.000000000000000 & [[[[[Catch1_39=0.000000000000000 & [Catch1_44=0.000000000000000 & [Catch1_33=0.000000000000000 & [[[[[Catch1_43=0.000000000000000 & [[[[[Catch1_66=0.000000000000000 & [[[[[Catch1_1=0.000000000000000 & [[[[Catch1_16=0.000000000000000 & [[Catch1_34=0.000000000000000 & [Catch1_79=0.000000000000000 & [[[Catch1_100=0.000000000000000 & [[[Catch1_91=0.000000000000000 & [[Catch1_86=0.000000000000000 & [[[Catch1_85=0.000000000000000 & [[[[Catch1_68=0.000000000000000 & [[Catch1_27=0.000000000000000 & [[Catch1_75=0.000000000000000 & [Catch1_92=0.000000000000000 & [[[Catch1_11=0.000000000000000 & [[[Catch1_81=0.000000000000000 & [[Catch1_78=0.000000000000000 & [[[[[[[Catch1_22=0.000000000000000 & [Catch1_41=0.000000000000000 & [[Catch1_74=0.000000000000000 & [[[[Catch1_12=0.000000000000000 & [Catch1_87=0.000000000000000 & [[[Catch1_10=0.000000000000000 & [[Catch1_94=0.000000000000000 & [Catch1_83=0.000000000000000 & [[[Catch1_6=0.000000000000000 & [Catch1_96=0.000000000000000 & [[[[Catch1_48=0.000000000000000 & [[[Catch1_90=0.000000000000000 & [true & 1.000000000000000=Catch1_84]] & Catch1_8=0.000000000000000] & Catch1_95=0.000000000000000]] & Catch1_15=0.000000000000000] & Catch1_64=0.000000000000000] & Catch1_26=0.000000000000000]]] & Catch1_42=0.000000000000000] & Catch1_55=0.000000000000000]]] & Catch1_13=0.000000000000000]] & Catch1_71=0.000000000000000] & Catch1_14=0.000000000000000]]] & Catch1_69=0.000000000000000] & Catch1_37=0.000000000000000] & Catch1_82=0.000000000000000]] & Catch1_38=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_36=0.000000000000000]] & Catch1_35=0.000000000000000] & Catch1_9=0.000000000000000]] & Catch1_89=0.000000000000000] & Catch1_32=0.000000000000000]]] & Catch1_88=0.000000000000000]] & Catch1_65=0.000000000000000]] & Catch1_25=0.000000000000000] & Catch1_73=0.000000000000000] & Catch1_50=0.000000000000000]] & Catch1_40=0.000000000000000] & Catch1_52=0.000000000000000]] & Catch1_20=0.000000000000000]] & Catch1_47=0.000000000000000] & Catch1_97=0.000000000000000]] & Catch1_4=0.000000000000000] & Catch1_3=0.000000000000000]]] & Catch1_31=0.000000000000000]] & Catch1_21=0.000000000000000] & Catch1_62=0.000000000000000] & Catch1_49=0.000000000000000]] & Catch1_93=0.000000000000000] & Catch1_77=0.000000000000000] & Catch1_63=0.000000000000000] & Catch1_70=0.000000000000000]] & Catch1_2=0.000000000000000] & Catch1_18=0.000000000000000] & Catch1_54=0.000000000000000] & Catch1_57=0.000000000000000]] & Catch1_67=0.000000000000000] & Catch1_7=0.000000000000000] & Catch1_99=0.000000000000000] & Catch1_19=0.000000000000000]]]] & Catch1_24=0.000000000000000] & Catch1_72=0.000000000000000] & Catch1_23=0.000000000000000] & Catch1_51=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: ~ [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_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_75=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_99 & 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_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_87=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_84 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_27_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Fork_36=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_48=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_18=0.000000000000000 & [[Fork_82=0.000000000000000 & [Fork_90=0.000000000000000 & [Fork_88=0.000000000000000 & [Fork_64=0.000000000000000 & [Fork_23=0.000000000000000 & [Fork_71=0.000000000000000 & [Fork_69=0.000000000000000 & [[Fork_79=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_51=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_8=0.000000000000000 & [[Fork_45=0.000000000000000 & [Fork_27=0.000000000000000 & [[Fork_30=0.000000000000000 & [Fork_46=0.000000000000000 & [[[[[Fork_43=0.000000000000000 & [[Fork_93=0.000000000000000 & [[[[Fork_65=0.000000000000000 & [Fork_85=0.000000000000000 & [Fork_50=0.000000000000000 & [Fork_72=0.000000000000000 & [Fork_17=0.000000000000000 & [[[[Fork_39=0.000000000000000 & [[[[[[Fork_21=0.000000000000000 & [[Fork_75=0.000000000000000 & [[[[[Fork_47=0.000000000000000 & [Fork_29=0.000000000000000 & [[Fork_24=0.000000000000000 & [[[Fork_80=0.000000000000000 & [[[Fork_81=0.000000000000000 & [[1.000000000000000=Fork_99 & true] & Fork_52=0.000000000000000]] & Fork_96=0.000000000000000] & Fork_74=0.000000000000000]] & Fork_15=0.000000000000000] & Fork_54=0.000000000000000]] & Fork_1=0.000000000000000]]] & Fork_34=0.000000000000000] & Fork_94=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_26=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_20=0.000000000000000]]] & Fork_70=0.000000000000000]]] & Fork_33=0.000000000000000]] & Fork_86=0.000000000000000]]]]]]]] & Fork_62=0.000000000000000]] & Fork_89=0.000000000000000]]]]]]]] & Fork_66=0.000000000000000]] & Fork_32=0.000000000000000]]]]]]]] & Fork_77=0.000000000000000]] & Fork_3=0.000000000000000]]]]]]]] & Fork_10=0.000000000000000]] & Fork_98=0.000000000000000]]]]]]]] & Fork_91=0.000000000000000]] | [[[[Catch1_5=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_66=0.000000000000000 & [[[[[Catch1_1=0.000000000000000 & [Catch1_49=0.000000000000000 & [[Catch1_21=0.000000000000000 & [Catch1_16=0.000000000000000 & [[Catch1_34=0.000000000000000 & [[[Catch1_4=0.000000000000000 & [Catch1_100=0.000000000000000 & [[[[[Catch1_86=0.000000000000000 & [Catch1_52=0.000000000000000 & [Catch1_40=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_46=0.000000000000000 & [Catch1_45=0.000000000000000 & [Catch1_80=0.000000000000000 & [Catch1_59=0.000000000000000 & [Catch1_56=0.000000000000000 & [Catch1_29=0.000000000000000 & [[[[[Catch1_82=0.000000000000000 & [Catch1_37=0.000000000000000 & [Catch1_69=0.000000000000000 & [Catch1_12=0.000000000000000 & [Catch1_87=0.000000000000000 & [Catch1_14=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_8=0.000000000000000 & [Catch1_90=0.000000000000000 & [1.000000000000000=Catch1_84 & true]]] & Catch1_95=0.000000000000000] & Catch1_48=0.000000000000000] & Catch1_15=0.000000000000000] & Catch1_64=0.000000000000000]]]]]]] & Catch1_94=0.000000000000000] & Catch1_13=0.000000000000000] & Catch1_10=0.000000000000000] & Catch1_71=0.000000000000000]]]]]]] & Catch1_74=0.000000000000000] & Catch1_38=0.000000000000000] & Catch1_41=0.000000000000000] & Catch1_22=0.000000000000000]]]]]]] & Catch1_78=0.000000000000000] & Catch1_36=0.000000000000000] & Catch1_81=0.000000000000000] & Catch1_35=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_20=0.000000000000000] & Catch1_91=0.000000000000000] & Catch1_47=0.000000000000000] & Catch1_97=0.000000000000000]]] & Catch1_3=0.000000000000000] & Catch1_79=0.000000000000000]] & Catch1_31=0.000000000000000]]] & Catch1_62=0.000000000000000]]] & Catch1_93=0.000000000000000] & Catch1_77=0.000000000000000] & Catch1_63=0.000000000000000] & Catch1_70=0.000000000000000]] & Catch1_2=0.000000000000000] & Catch1_18=0.000000000000000] & Catch1_54=0.000000000000000] & Catch1_57=0.000000000000000] & Catch1_43=0.000000000000000]]]]]]]]]]]]]] & Catch1_61=0.000000000000000] & Catch1_53=0.000000000000000] & Catch1_17=0.000000000000000] & Catch1_58=0.000000000000000]] & Catch1_98=0.000000000000000] & Catch1_60=0.000000000000000] & Catch1_30=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[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_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_87=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_84 & 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_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_75=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_99 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_28_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[Fork_36=0.000000000000000 & [Fork_91=0.000000000000000 & [[[[Fork_59=0.000000000000000 & [[[[[Fork_48=0.000000000000000 & [[[[Fork_68=0.000000000000000 & [Fork_60=0.000000000000000 & [[[[[[[[Fork_90=0.000000000000000 & [[[[[[[Fork_79=0.000000000000000 & [[Fork_14=0.000000000000000 & [[Fork_76=0.000000000000000 & [[Fork_63=0.000000000000000 & [[[Fork_89=0.000000000000000 & [Fork_51=0.000000000000000 & [[Fork_58=0.000000000000000 & [[Fork_19=0.000000000000000 & [Fork_6=0.000000000000000 & [[[Fork_49=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_43=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_57=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_99 & true]]]]]]]]]]] & Fork_47=0.000000000000000] & Fork_34=0.000000000000000] & Fork_94=0.000000000000000] & Fork_2=0.000000000000000]] & Fork_75=0.000000000000000] & Fork_44=0.000000000000000] & Fork_21=0.000000000000000] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000]]]]]]]]]]]]]] & Fork_25=0.000000000000000] & Fork_7=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_86=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_56=0.000000000000000]] & Fork_12=0.000000000000000]] & Fork_66=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_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_40=0.000000000000000] & Fork_84=0.000000000000000] & Fork_10=0.000000000000000]] & Fork_98=0.000000000000000] & Fork_16=0.000000000000000] & Fork_95=0.000000000000000] & Fork_97=0.000000000000000]] & Fork_9=0.000000000000000] & Fork_55=0.000000000000000] & Fork_13=0.000000000000000]]]] & [[Catch1_60=0.000000000000000 & [[[Catch1_58=0.000000000000000 & [[[[Catch1_28=0.000000000000000 & [[[Catch1_23=0.000000000000000 & [Catch1_72=0.000000000000000 & [[[Catch1_44=0.000000000000000 & [[[Catch1_99=0.000000000000000 & [Catch1_7=0.000000000000000 & [[[Catch1_57=0.000000000000000 & [Catch1_54=0.000000000000000 & [[[Catch1_66=0.000000000000000 & [[[Catch1_77=0.000000000000000 & [[[[Catch1_62=0.000000000000000 & [Catch1_21=0.000000000000000 & [[[Catch1_34=0.000000000000000 & [Catch1_79=0.000000000000000 & [[[Catch1_100=0.000000000000000 & [Catch1_97=0.000000000000000 & [[[Catch1_20=0.000000000000000 & [Catch1_86=0.000000000000000 & [[[Catch1_85=0.000000000000000 & [Catch1_50=0.000000000000000 & [[[Catch1_68=0.000000000000000 & [Catch1_65=0.000000000000000 & [[[Catch1_75=0.000000000000000 & [Catch1_92=0.000000000000000 & [[[Catch1_11=0.000000000000000 & [Catch1_9=0.000000000000000 & [[[Catch1_36=0.000000000000000 & [Catch1_78=0.000000000000000 & [[[Catch1_80=0.000000000000000 & [[[[Catch1_22=0.000000000000000 & [[[[[[[[[[Catch1_71=0.000000000000000 & [Catch1_10=0.000000000000000 & [[[[[[[[[[[[[Catch1_8=0.000000000000000 & [[true & 1.000000000000000=Catch1_84] & Catch1_90=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_14=0.000000000000000] & Catch1_87=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_45=0.000000000000000] & Catch1_46=0.000000000000000]]] & Catch1_81=0.000000000000000] & Catch1_35=0.000000000000000]]] & Catch1_89=0.000000000000000] & Catch1_32=0.000000000000000]]] & Catch1_88=0.000000000000000] & Catch1_27=0.000000000000000]]] & Catch1_25=0.000000000000000] & Catch1_73=0.000000000000000]]] & Catch1_40=0.000000000000000] & Catch1_52=0.000000000000000]]] & Catch1_91=0.000000000000000] & Catch1_47=0.000000000000000]]] & Catch1_4=0.000000000000000] & Catch1_3=0.000000000000000]]] & Catch1_31=0.000000000000000] & Catch1_16=0.000000000000000]]] & Catch1_49=0.000000000000000] & Catch1_1=0.000000000000000] & Catch1_93=0.000000000000000]] & Catch1_63=0.000000000000000] & Catch1_70=0.000000000000000]] & Catch1_2=0.000000000000000] & Catch1_18=0.000000000000000]]] & Catch1_43=0.000000000000000] & Catch1_67=0.000000000000000]]] & Catch1_19=0.000000000000000] & Catch1_33=0.000000000000000]] & Catch1_39=0.000000000000000] & Catch1_24=0.000000000000000]]] & Catch1_51=0.000000000000000] & Catch1_76=0.000000000000000]] & Catch1_61=0.000000000000000] & Catch1_53=0.000000000000000] & Catch1_17=0.000000000000000]] & Catch1_5=0.000000000000000] & Catch1_98=0.000000000000000]] & Catch1_30=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[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_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_87=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_84 & 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_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_75=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_99 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_29_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[[[Fork_55=0.000000000000000 & [[[[[Fork_16=0.000000000000000 & [[[Fork_10=0.000000000000000 & [[[[[Fork_61=0.000000000000000 & [[[[[Fork_77=0.000000000000000 & [[[[[Fork_23=0.000000000000000 & [[[Fork_32=0.000000000000000 & [[Fork_66=0.000000000000000 & [[[[[[[[Fork_89=0.000000000000000 & [[[Fork_58=0.000000000000000 & [[[[[[[[[[[Fork_27=0.000000000000000 & [[[Fork_46=0.000000000000000 & [[[[[[[[[[Fork_26=0.000000000000000 & [[[Fork_50=0.000000000000000 & [[Fork_17=0.000000000000000 & [[[Fork_73=0.000000000000000 & [[[Fork_37=0.000000000000000 & [[[[[[[Fork_57=0.000000000000000 & [[[[[[Fork_1=0.000000000000000 & [[[[Fork_80=0.000000000000000 & [Fork_74=0.000000000000000 & [[[Fork_52=0.000000000000000 & [true & 1.000000000000000=Fork_99]] & Fork_81=0.000000000000000] & Fork_96=0.000000000000000]]] & Fork_15=0.000000000000000] & Fork_54=0.000000000000000] & Fork_24=0.000000000000000]] & Fork_29=0.000000000000000] & Fork_47=0.000000000000000] & Fork_34=0.000000000000000] & Fork_94=0.000000000000000] & Fork_2=0.000000000000000]] & Fork_75=0.000000000000000] & Fork_44=0.000000000000000] & Fork_21=0.000000000000000] & Fork_31=0.000000000000000] & Fork_92=0.000000000000000] & Fork_22=0.000000000000000]] & Fork_87=0.000000000000000] & Fork_39=0.000000000000000]] & Fork_28=0.000000000000000] & Fork_35=0.000000000000000]] & Fork_72=0.000000000000000]] & Fork_85=0.000000000000000] & Fork_65=0.000000000000000]] & Fork_25=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_30=0.000000000000000] & Fork_70=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_100=0.000000000000000]] & Fork_62=0.000000000000000] & Fork_51=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_79=0.000000000000000]] & Fork_69=0.000000000000000] & Fork_71=0.000000000000000]] & Fork_64=0.000000000000000] & Fork_88=0.000000000000000] & Fork_90=0.000000000000000] & Fork_82=0.000000000000000]] & Fork_18=0.000000000000000] & Fork_3=0.000000000000000] & Fork_78=0.000000000000000] & Fork_42=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_95=0.000000000000000] & Fork_97=0.000000000000000] & Fork_59=0.000000000000000] & Fork_9=0.000000000000000]] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000] & Fork_36=0.000000000000000]] | [[[[[[[[[[Catch1_76=0.000000000000000 & [[[[[[Catch1_44=0.000000000000000 & [[[[[[[[[[Catch1_2=0.000000000000000 & [[[[[[Catch1_1=0.000000000000000 & [Catch1_49=0.000000000000000 & [[[[[[[[[[[[[[Catch1_86=0.000000000000000 & [[[[[[[Catch1_68=0.000000000000000 & [[[[[Catch1_92=0.000000000000000 & [[[[[[[[[[[[Catch1_59=0.000000000000000 & [[[Catch1_22=0.000000000000000 & [[[[[Catch1_37=0.000000000000000 & [[Catch1_12=0.000000000000000 & [[[[[[[[[[[[[[[[[[[true & 1.000000000000000=Catch1_84] & 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_87=0.000000000000000]] & Catch1_69=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_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_75=0.000000000000000] & Catch1_88=0.000000000000000] & Catch1_27=0.000000000000000] & Catch1_65=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_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_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_39=0.000000000000000] & Catch1_24=0.000000000000000] & Catch1_72=0.000000000000000] & Catch1_23=0.000000000000000] & Catch1_51=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: ~ [E [true U ~ [[[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_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_87=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_84 & 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_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_75=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_99 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_30_markingcomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[Fork_9=0.000000000000000 & [[[[[[[[[[[Fork_60=0.000000000000000 & [[[[Fork_3=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[Fork_62=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[Fork_72=0.000000000000000 & [[[[Fork_73=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=Fork_99] & 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_54=0.000000000000000] & Fork_24=0.000000000000000] & Fork_1=0.000000000000000] & Fork_29=0.000000000000000] & Fork_47=0.000000000000000] & Fork_34=0.000000000000000] & Fork_94=0.000000000000000] & Fork_2=0.000000000000000] & Fork_57=0.000000000000000] & Fork_75=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_28=0.000000000000000] & Fork_35=0.000000000000000] & Fork_17=0.000000000000000]] & Fork_50=0.000000000000000] & Fork_85=0.000000000000000] & Fork_65=0.000000000000000] & Fork_26=0.000000000000000] & Fork_25=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_100=0.000000000000000] & Fork_58=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_90=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_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_55=0.000000000000000] & Fork_13=0.000000000000000] & Fork_91=0.000000000000000] & Fork_36=0.000000000000000] <-> [Catch1_30=0.000000000000000 & [[[[[[[[[[[Catch1_23=0.000000000000000 & [[[[[[[[[Catch1_67=0.000000000000000 & [[[[Catch1_18=0.000000000000000 & [[[[[[[[[Catch1_62=0.000000000000000 & [[Catch1_16=0.000000000000000 & [[[[[[[Catch1_97=0.000000000000000 & [[[[[[Catch1_40=0.000000000000000 & [[[[[[[[[Catch1_75=0.000000000000000 & [[[[[[[Catch1_81=0.000000000000000 & [[[[Catch1_45=0.000000000000000 & [[[[[[[[[[[[[Catch1_87=0.000000000000000 & [[[[[[[Catch1_55=0.000000000000000 & [[[[Catch1_26=0.000000000000000 & [[[[[[[true & 1.000000000000000=Catch1_84] & 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_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_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_46=0.000000000000000] & Catch1_78=0.000000000000000] & Catch1_36=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_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_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_34=0.000000000000000] & Catch1_31=0.000000000000000]] & Catch1_21=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_54=0.000000000000000] & Catch1_57=0.000000000000000] & Catch1_43=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_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]]]]
normalized: ~ [E [true U ~ [[[~ [[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_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_87=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_84 & 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_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_75=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_99 & 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_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_75=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_99 & 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_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_87=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_84 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_31_markingcomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[1.000000000000000<=Catch2_58 & true] & true] & [[[[[[Catch2_69!=0.000000000000000 | [[[[[[[[[[[[[Catch2_57!=0.000000000000000 | [[[Catch2_41!=0.000000000000000 | [[[[[[[[[[[[[[[[[[Catch2_54!=0.000000000000000 | [[[[[[[[[[Catch2_20!=0.000000000000000 | [[[Catch2_42!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[[[[Catch2_97!=0.000000000000000 | [[[[[[[Catch2_26!=0.000000000000000 | [[[[[[[[[[[Catch2_56!=0.000000000000000 | [[Catch2_96!=0.000000000000000 | [[[[[false | Catch2_66!=0.000000000000000] | Catch2_99!=0.000000000000000] | Catch2_67!=0.000000000000000] | Catch2_95!=0.000000000000000] | Catch2_37!=0.000000000000000]] | Catch2_45!=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_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_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_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_6!=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_82!=0.000000000000000] | Catch2_23!=0.000000000000000]] | Catch2_51!=0.000000000000000] | Catch2_76!=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_61!=0.000000000000000] | Catch2_77!=0.000000000000000] | Catch2_25!=0.000000000000000] | Catch2_24!=0.000000000000000] | [false | 1.000000000000000Catch2_41]]]]
normalized: ~ [E [true U ~ [[[[1.000000000000000>Catch2_41 & true] & [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_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 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[[1.000000000000000
-> the formula is FALSE

FORMULA p_32_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Catch2_24=0.000000000000000 & [[[[[[[[[[[[[[[[Catch2_100=0.000000000000000 & [[[Catch2_51=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[Catch2_15=0.000000000000000 & [[[Catch2_55=0.000000000000000 & [[[Catch2_75=0.000000000000000 & [[[Catch2_20=0.000000000000000 & [[[[[[[[[[[[[[Catch2_48=0.000000000000000 & [[[[[[[[Catch2_79=0.000000000000000 & [[[Catch2_97=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[Catch2_37=0.000000000000000 & [[[[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_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_87=0.000000000000000] & Catch2_49=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_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_1=0.000000000000000] & Catch2_22=0.000000000000000]] & Catch2_35=0.000000000000000] & Catch2_72=0.000000000000000]] & Catch2_36=0.000000000000000] & Catch2_73=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_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_23=0.000000000000000]] & Catch2_76=0.000000000000000] & Catch2_57=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]] & [true & 1.000000000000000>Catch2_41]] | [[[true & 1.000000000000000<=Catch2_58] & true] & [[[[[[[[[[[[[[Catch2_59!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_30!=0.000000000000000 | [[[[Catch2_17!=0.000000000000000 | [[[[[[[[Catch2_84!=0.000000000000000 | [[[[[[[[[[[[[[[[[[[[[Catch2_66!=0.000000000000000 | false] | 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_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_52!=0.000000000000000] | Catch2_16!=0.000000000000000] | Catch2_10!=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_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_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_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] | [false | 1.000000000000000 normalized: ~ [E [true U ~ [[[[[1.000000000000000Catch2_41 & true] & [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_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 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_33_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 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_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_23=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>Catch2_41]] & [[true & [true & 1.000000000000000<=Catch2_58]] & [[false | 1.000000000000000 normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | 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_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_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] | [false | 1.000000000000000Catch2_41] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[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 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & 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_40=0.000000000000000] & Catch2_89=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_82=0.000000000000000] & Catch2_23=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]]]]]]

-> the formula is FALSE

FORMULA p_34_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m9sec

STOP 1369702602

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


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

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

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

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

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

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

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