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=ReachabilityPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
export BIN_DIR=/home/mcc/BenchKit/bin
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 ReachabilityPlaceComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo 'START 1369696059'

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=136968524700090_n_2)
=====================================================================
runnning marcie on Philosophers-PT-000100 (ReachabilityPlaceComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Philosophers-PT-000100, examination is ReachabilityPlaceComparison
=====================================================================

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

START 1369696059

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 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 [[[[[Catch1_39!=Eat_39 & [[Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [[[Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [[[[[[[[Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [[Catch1_17!=Eat_17 & [[[[[Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [[[Catch1_46!=Eat_46 & [[[[Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [[[[[[[Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [[Catch1_56!=Eat_56 & [[[[Catch1_58!=Eat_58 & [[[Catch1_63!=Eat_63 & [[[[Catch1_89!=Eat_89 & [[Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [[[[Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [[Catch1_86!=Eat_86 & [[[[[Catch1_20!=Eat_20 & [[Catch1_30!=Eat_30 & [[Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [[[Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [[Catch1_45!=Eat_45 & [[Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [[[Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [[Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [[Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [[true & Catch1_11!=Eat_11] & Catch1_7!=Eat_7]]] & Catch1_97!=Eat_97]]] & Catch1_55!=Eat_55]]] & Catch1_62!=Eat_62] & Catch1_18!=Eat_18]]]] & Catch1_87!=Eat_87]] & Catch1_6!=Eat_6]]] & Catch1_50!=Eat_50] & Catch1_57!=Eat_57]]] & Catch1_96!=Eat_96]] & Catch1_35!=Eat_35]] & Catch1_73!=Eat_73] & Catch1_81!=Eat_81] & Catch1_22!=Eat_22] & Catch1_78!=Eat_78]] & Catch1_19!=Eat_19]]] & Catch1_5!=Eat_5] & Catch1_3!=Eat_3] & Catch1_28!=Eat_28]]]] & Catch1_31!=Eat_31]] & Catch1_90!=Eat_90] & Catch1_61!=Eat_61] & Catch1_99!=Eat_99]] & Catch1_65!=Eat_65] & Catch1_4!=Eat_4]] & Catch1_53!=Eat_53] & Catch1_54!=Eat_54] & Catch1_9!=Eat_9]] & Catch1_26!=Eat_26]]]] & Catch1_44!=Eat_44] & Catch1_27!=Eat_27] & Catch1_100!=Eat_100] & Catch1_48!=Eat_48] & Catch1_13!=Eat_13] & Catch1_66!=Eat_66]]] & Catch1_74!=Eat_74] & Catch1_80!=Eat_80] & Catch1_33!=Eat_33]] & Catch1_88!=Eat_88] & Catch1_60!=Eat_60]]] & Catch1_75!=Eat_75] & Catch1_15!=Eat_15] & Catch1_77!=Eat_77] & Catch1_42!=Eat_42]] & Catch1_67!=Eat_67]]] & Catch1_25!=Eat_25] & Catch1_83!=Eat_83] & Catch1_34!=Eat_34] & Catch1_14!=Eat_14] & Catch1_84!=Eat_84] & Catch1_21!=Eat_21] & Catch1_43!=Eat_43]]] & Catch1_69!=Eat_69] & Catch1_64!=Eat_64]]] & Catch1_41!=Eat_41]] & Catch1_16!=Eat_16] & Catch1_82!=Eat_82] & [[[Catch2_62=Fork_62 & [[Catch2_80=Fork_80 & [[[[Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [[[[[[[[[[[[Catch2_49=Fork_49 & [[[[[Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [[[Catch2_77=Fork_77 & [[Catch2_92=Fork_92 & [[Catch2_44=Fork_44 & [[[Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [[[Catch2_1=Fork_1 & [[[[[[Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [[Catch2_55=Fork_55 & [[[Catch2_52=Fork_52 & [[[Catch2_25=Fork_25 & [[[[Catch2_7=Fork_7 & [[Catch2_16=Fork_16 & [[[Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [[Catch2_89=Fork_89 & [[[[[[[Catch2_35=Fork_35 & [[[Catch2_63=Fork_63 & [[[[[[Catch2_85=Fork_85 & [[Catch2_84=Fork_84 & [[Catch2_99=Fork_99 & [[Catch2_27=Fork_27 & [[[Catch2_86=Fork_86 & [[Catch2_46=Fork_46 & [[true & Catch2_50=Fork_50] & Catch2_40=Fork_40]] & Catch2_54=Fork_54]] & Catch2_42=Fork_42] & Catch2_6=Fork_6]] & Catch2_33=Fork_33]] & Catch2_68=Fork_68]] & Catch2_4=Fork_4]] & Catch2_81=Fork_81] & Catch2_43=Fork_43] & Catch2_36=Fork_36] & Catch2_37=Fork_37] & Catch2_100=Fork_100]] & Catch2_64=Fork_64] & Catch2_41=Fork_41]] & Catch2_59=Fork_59] & Catch2_93=Fork_93] & Catch2_2=Fork_2] & Catch2_70=Fork_70] & Catch2_8=Fork_8] & Catch2_22=Fork_22]] & Catch2_96=Fork_96]]] & Catch2_28=Fork_28] & Catch2_5=Fork_5]] & Catch2_12=Fork_12]] & Catch2_87=Fork_87] & Catch2_17=Fork_17] & Catch2_32=Fork_32]] & Catch2_66=Fork_66] & Catch2_10=Fork_10]] & Catch2_61=Fork_61] & Catch2_56=Fork_56]] & Catch2_90=Fork_90]]]] & Catch2_39=Fork_39] & Catch2_53=Fork_53] & Catch2_3=Fork_3] & Catch2_91=Fork_91] & Catch2_79=Fork_79]] & Catch2_58=Fork_58] & Catch2_95=Fork_95]]] & Catch2_14=Fork_14] & Catch2_74=Fork_74]] & Catch2_45=Fork_45]] & Catch2_29=Fork_29]] & Catch2_69=Fork_69] & Catch2_11=Fork_11]]] & Catch2_31=Fork_31] & Catch2_15=Fork_15] & Catch2_75=Fork_75] & Catch2_38=Fork_38]] & Catch2_60=Fork_60] & Catch2_26=Fork_26] & Catch2_67=Fork_67] & Catch2_82=Fork_82] & Catch2_76=Fork_76] & Catch2_9=Fork_9] & Catch2_71=Fork_71] & Catch2_18=Fork_18] & Catch2_19=Fork_19] & Catch2_88=Fork_88] & Catch2_65=Fork_65]]]] & Catch2_21=Fork_21] & Catch2_24=Fork_24] & Catch2_20=Fork_20]] & Catch2_48=Fork_48]] & Catch2_47=Fork_47] & Catch2_73=Fork_73]]]
normalized: ~ [E [true U ~ [[[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_7_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [[[[[Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [[[[[Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [[[[[Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [[[[[Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [[[[[Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [[[[[Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [[[[[[Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [[[[[[Catch1_35!=Eat_35 & [[[[[[[Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [[Catch1_45!=Eat_45 & [[[[[Catch1_18!=Eat_18 & [[[[[[Catch1_95!=Eat_95 & [[[[[Catch1_11!=Eat_11 & true] & Catch1_7!=Eat_7] & Catch1_72!=Eat_72] & Catch1_52!=Eat_52] & Catch1_97!=Eat_97]] & Catch1_29!=Eat_29] & Catch1_55!=Eat_55] & Catch1_36!=Eat_36] & Catch1_49!=Eat_49] & Catch1_62!=Eat_62]] & Catch1_98!=Eat_98] & Catch1_47!=Eat_47] & Catch1_51!=Eat_51] & Catch1_87!=Eat_87]] & Catch1_6!=Eat_6]]] & Catch1_50!=Eat_50] & Catch1_57!=Eat_57] & Catch1_12!=Eat_12] & Catch1_85!=Eat_85] & Catch1_96!=Eat_96] & Catch1_30!=Eat_30]] & Catch1_20!=Eat_20] & Catch1_73!=Eat_73] & Catch1_81!=Eat_81] & Catch1_22!=Eat_22] & Catch1_78!=Eat_78]]] & Catch1_70!=Eat_70] & Catch1_71!=Eat_71] & Catch1_5!=Eat_5] & Catch1_3!=Eat_3] & Catch1_28!=Eat_28]]]]] & Catch1_89!=Eat_89] & Catch1_90!=Eat_90] & Catch1_61!=Eat_61] & Catch1_99!=Eat_99]]]]]]] & Catch1_9!=Eat_9] & Catch1_56!=Eat_56] & Catch1_26!=Eat_26] & Catch1_92!=Eat_92]]]]]]] & Catch1_13!=Eat_13] & Catch1_66!=Eat_66] & Catch1_91!=Eat_91] & Catch1_79!=Eat_79]]]]]]] & Catch1_2!=Eat_2] & Catch1_1!=Eat_1] & Catch1_75!=Eat_75] & Catch1_15!=Eat_15]]]]]]] & Catch1_25!=Eat_25] & Catch1_83!=Eat_83] & Catch1_34!=Eat_34] & Catch1_14!=Eat_14]]]]]]] & Catch1_64!=Eat_64] & Catch1_24!=Eat_24] & Catch1_93!=Eat_93] & Catch1_41!=Eat_41]]]] | [Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [[[[[[Catch2_19=Fork_19 & [[[[[Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [[[[[[[[[[Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [[Catch2_79=Fork_79 & [[Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [[[[[[Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [[[[[[[Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [[[[[Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [[[[[Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [[[[[Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [[true & Catch2_50=Fork_50] & Catch2_40=Fork_40]]]]]]] & Catch2_33=Fork_33] & Catch2_99=Fork_99] & Catch2_68=Fork_68] & Catch2_84=Fork_84]]]]]]] & Catch2_100=Fork_100] & Catch2_63=Fork_63] & Catch2_64=Fork_64] & Catch2_41=Fork_41]]]]]]] & Catch2_22=Fork_22] & Catch2_89=Fork_89] & Catch2_96=Fork_96] & Catch2_97=Fork_97]]]]]]] & Catch2_87=Fork_87] & Catch2_17=Fork_17] & Catch2_32=Fork_32] & Catch2_25=Fork_25] & Catch2_66=Fork_66] & Catch2_10=Fork_10]]]]] & Catch2_90=Fork_90] & Catch2_94=Fork_94] & Catch2_78=Fork_78] & Catch2_57=Fork_57] & Catch2_39=Fork_39]]] & Catch2_91=Fork_91]] & Catch2_1=Fork_1]]] & Catch2_98=Fork_98] & Catch2_23=Fork_23] & Catch2_14=Fork_14] & Catch2_74=Fork_74] & Catch2_44=Fork_44] & Catch2_45=Fork_45] & Catch2_92=Fork_92] & Catch2_29=Fork_29] & Catch2_77=Fork_77]]]]]]]]]]]]]] & Catch2_76=Fork_76] & Catch2_9=Fork_9] & Catch2_71=Fork_71] & Catch2_18=Fork_18]] & Catch2_88=Fork_88] & Catch2_65=Fork_65] & Catch2_51=Fork_51] & Catch2_83=Fork_83] & Catch2_72=Fork_72]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_8_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[Catch2_47=Fork_47 & [[[Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [[[Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [[[Catch2_88=Fork_88 & [[[[Catch2_9=Fork_9 & [[[Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [[[Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [[[Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [[[Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [[[Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [[[Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [[[Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [[[Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [[[Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [[[Catch2_52=Fork_52 & [[[[Catch2_32=Fork_32 & [[[[[[[[[Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [[[Catch2_8=Fork_8 & [[[[[[Catch2_41=Fork_41 & [[[[Catch2_37=Fork_37 & [[[[Catch2_85=Fork_85 & [[Catch2_84=Fork_84 & [[[[[[[[[Catch2_46=Fork_46 & [[Catch2_50=Fork_50 & true] & Catch2_40=Fork_40]] & Catch2_54=Fork_54] & Catch2_86=Fork_86] & Catch2_42=Fork_42] & Catch2_6=Fork_6] & Catch2_27=Fork_27] & Catch2_33=Fork_33] & Catch2_99=Fork_99] & Catch2_68=Fork_68]] & Catch2_4=Fork_4]] & Catch2_81=Fork_81] & Catch2_43=Fork_43] & Catch2_36=Fork_36]] & Catch2_100=Fork_100] & Catch2_63=Fork_63] & Catch2_64=Fork_64]] & Catch2_35=Fork_35] & Catch2_59=Fork_59] & Catch2_93=Fork_93] & Catch2_2=Fork_2] & Catch2_70=Fork_70]] & Catch2_22=Fork_22] & Catch2_89=Fork_89]]] & Catch2_30=Fork_30] & Catch2_28=Fork_28] & Catch2_5=Fork_5] & Catch2_16=Fork_16] & Catch2_12=Fork_12] & Catch2_7=Fork_7] & Catch2_87=Fork_87] & Catch2_17=Fork_17]] & Catch2_25=Fork_25] & Catch2_66=Fork_66] & Catch2_10=Fork_10]] & Catch2_61=Fork_61] & Catch2_56=Fork_56]]] & Catch2_94=Fork_94] & Catch2_78=Fork_78]]] & Catch2_53=Fork_53] & Catch2_3=Fork_3]]] & Catch2_1=Fork_1] & Catch2_58=Fork_58]]] & Catch2_23=Fork_23] & Catch2_14=Fork_14]]] & Catch2_45=Fork_45] & Catch2_92=Fork_92]]] & Catch2_69=Fork_69] & Catch2_11=Fork_11]]] & Catch2_31=Fork_31] & Catch2_15=Fork_15]]] & Catch2_49=Fork_49] & Catch2_60=Fork_60]]] & Catch2_82=Fork_82] & Catch2_76=Fork_76]] & Catch2_71=Fork_71] & Catch2_18=Fork_18] & Catch2_19=Fork_19]] & Catch2_65=Fork_65] & Catch2_51=Fork_51]]] & Catch2_21=Fork_21] & Catch2_24=Fork_24]]] & Catch2_48=Fork_48] & Catch2_62=Fork_62]] & Catch2_73=Fork_73] & [Catch1_82!=Eat_82 & [[[[[[[[[[Catch1_43!=Eat_43 & [[Catch1_84!=Eat_84 & [[[[Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [[[[[[[[[Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [[[Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [[[[Catch1_48!=Eat_48 & [[[[[[[[[[[[[[[[Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [[[[[[Catch1_73!=Eat_73 & [[[[[Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [[[[[[Catch1_95!=Eat_95 & [[[[[Catch1_11!=Eat_11 & true] & Catch1_7!=Eat_7] & Catch1_72!=Eat_72] & Catch1_52!=Eat_52] & Catch1_97!=Eat_97]] & Catch1_29!=Eat_29] & Catch1_55!=Eat_55] & Catch1_36!=Eat_36] & Catch1_49!=Eat_49] & Catch1_62!=Eat_62]]]]]]]]]]]]]] & Catch1_96!=Eat_96] & Catch1_30!=Eat_30] & Catch1_35!=Eat_35] & Catch1_20!=Eat_20]] & Catch1_81!=Eat_81] & Catch1_22!=Eat_22] & Catch1_78!=Eat_78] & Catch1_86!=Eat_86] & Catch1_19!=Eat_19]]]]]]]]]]]]]] & Catch1_63!=Eat_63] & Catch1_65!=Eat_65] & Catch1_4!=Eat_4] & Catch1_58!=Eat_58] & Catch1_53!=Eat_53] & Catch1_54!=Eat_54] & Catch1_9!=Eat_9] & Catch1_56!=Eat_56] & Catch1_26!=Eat_26] & Catch1_92!=Eat_92] & Catch1_38!=Eat_38] & Catch1_68!=Eat_68] & Catch1_44!=Eat_44] & Catch1_27!=Eat_27] & Catch1_100!=Eat_100]] & Catch1_13!=Eat_13] & Catch1_66!=Eat_66] & Catch1_91!=Eat_91]]] & Catch1_80!=Eat_80] & Catch1_33!=Eat_33]]] & Catch1_60!=Eat_60] & Catch1_2!=Eat_2] & Catch1_1!=Eat_1] & Catch1_75!=Eat_75] & Catch1_15!=Eat_15] & Catch1_77!=Eat_77] & Catch1_42!=Eat_42] & Catch1_17!=Eat_17]]]]] & Catch1_83!=Eat_83] & Catch1_34!=Eat_34] & Catch1_14!=Eat_14]] & Catch1_21!=Eat_21]] & Catch1_37!=Eat_37] & Catch1_40!=Eat_40] & Catch1_69!=Eat_69] & Catch1_64!=Eat_64] & Catch1_24!=Eat_24] & Catch1_93!=Eat_93] & Catch1_41!=Eat_41] & Catch1_39!=Eat_39] & Catch1_16!=Eat_16]]]]
normalized: ~ [E [true U ~ [[[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_9_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[Catch1_64!=Eat_64 & [[Catch1_40!=Eat_40 & [[[[[[[[[[[[[[[[[Catch1_1!=Eat_1 & [[[[[Catch1_33!=Eat_33 & [[[[[[Catch1_13!=Eat_13 & [[[Catch1_27!=Eat_27 & [[[[[[Catch1_56!=Eat_56 & [[[Catch1_53!=Eat_53 & [[[[[[[[[[[[Catch1_94!=Eat_94 & [[[Catch1_5!=Eat_5 & [[[[Catch1_86!=Eat_86 & [[[[[[Catch1_35!=Eat_35 & [[[Catch1_85!=Eat_85 & [[[[[Catch1_32!=Eat_32 & [[[Catch1_87!=Eat_87 & [[[Catch1_98!=Eat_98 & [[[[Catch1_36!=Eat_36 & [[[Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [[[Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]] & Catch1_72!=Eat_72] & Catch1_52!=Eat_52]]] & Catch1_29!=Eat_29] & Catch1_55!=Eat_55]] & Catch1_49!=Eat_49] & Catch1_62!=Eat_62] & Catch1_18!=Eat_18]] & Catch1_47!=Eat_47] & Catch1_51!=Eat_51]] & Catch1_45!=Eat_45] & Catch1_6!=Eat_6]] & Catch1_59!=Eat_59] & Catch1_50!=Eat_50] & Catch1_57!=Eat_57] & Catch1_12!=Eat_12]] & Catch1_96!=Eat_96] & Catch1_30!=Eat_30]] & Catch1_20!=Eat_20] & Catch1_73!=Eat_73] & Catch1_81!=Eat_81] & Catch1_22!=Eat_22] & Catch1_78!=Eat_78]] & Catch1_19!=Eat_19] & Catch1_70!=Eat_70] & Catch1_71!=Eat_71]] & Catch1_3!=Eat_3] & Catch1_28!=Eat_28]] & Catch1_8!=Eat_8] & Catch1_76!=Eat_76] & Catch1_31!=Eat_31] & Catch1_89!=Eat_89] & Catch1_90!=Eat_90] & Catch1_61!=Eat_61] & Catch1_99!=Eat_99] & Catch1_63!=Eat_63] & Catch1_65!=Eat_65] & Catch1_4!=Eat_4] & Catch1_58!=Eat_58]] & Catch1_54!=Eat_54] & Catch1_9!=Eat_9]] & Catch1_26!=Eat_26] & Catch1_92!=Eat_92] & Catch1_38!=Eat_38] & Catch1_68!=Eat_68] & Catch1_44!=Eat_44]] & Catch1_100!=Eat_100] & Catch1_48!=Eat_48]] & Catch1_66!=Eat_66] & Catch1_91!=Eat_91] & Catch1_79!=Eat_79] & Catch1_74!=Eat_74] & Catch1_80!=Eat_80]] & Catch1_46!=Eat_46] & Catch1_88!=Eat_88] & Catch1_60!=Eat_60] & Catch1_2!=Eat_2]] & Catch1_75!=Eat_75] & Catch1_15!=Eat_15] & Catch1_77!=Eat_77] & Catch1_42!=Eat_42] & Catch1_17!=Eat_17] & Catch1_67!=Eat_67] & Catch1_10!=Eat_10] & Catch1_23!=Eat_23] & Catch1_25!=Eat_25] & Catch1_83!=Eat_83] & Catch1_34!=Eat_34] & Catch1_14!=Eat_14] & Catch1_84!=Eat_84] & Catch1_21!=Eat_21] & Catch1_43!=Eat_43] & Catch1_37!=Eat_37]] & Catch1_69!=Eat_69]] & Catch1_24!=Eat_24] & Catch1_93!=Eat_93] & Catch1_41!=Eat_41] & Catch1_39!=Eat_39] & Catch1_16!=Eat_16] & Catch1_82!=Eat_82] | [[[[Catch2_48=Fork_48 & [[[[[[[[[Catch2_88=Fork_88 & [[[[[Catch2_76=Fork_76 & [[[Catch2_26=Fork_26 & [[Catch2_49=Fork_49 & [[Catch2_75=Fork_75 & [[[[[[[Catch2_77=Fork_77 & [[[[[[[[[[Catch2_58=Fork_58 & [[[[[[[[[[Catch2_90=Fork_90 & [[[[[Catch2_10=Fork_10 & [[Catch2_25=Fork_25 & [[[Catch2_87=Fork_87 & [[Catch2_12=Fork_12 & [[[[[Catch2_97=Fork_97 & [[[[[[[[[[[[[[[Catch2_36=Fork_36 & [[[[[Catch2_84=Fork_84 & [[Catch2_99=Fork_99 & [[[Catch2_6=Fork_6 & [[Catch2_86=Fork_86 & [[[[true & Catch2_50=Fork_50] & Catch2_40=Fork_40] & Catch2_46=Fork_46] & Catch2_54=Fork_54]] & Catch2_42=Fork_42]] & Catch2_27=Fork_27] & Catch2_33=Fork_33]] & Catch2_68=Fork_68]] & Catch2_4=Fork_4] & Catch2_85=Fork_85] & Catch2_81=Fork_81] & Catch2_43=Fork_43]] & Catch2_37=Fork_37] & Catch2_100=Fork_100] & Catch2_63=Fork_63] & Catch2_64=Fork_64] & Catch2_41=Fork_41] & Catch2_35=Fork_35] & Catch2_59=Fork_59] & Catch2_93=Fork_93] & Catch2_2=Fork_2] & Catch2_70=Fork_70] & Catch2_8=Fork_8] & Catch2_22=Fork_22] & Catch2_89=Fork_89] & Catch2_96=Fork_96]] & Catch2_30=Fork_30] & Catch2_28=Fork_28] & Catch2_5=Fork_5] & Catch2_16=Fork_16]] & Catch2_7=Fork_7]] & Catch2_17=Fork_17] & Catch2_32=Fork_32]] & Catch2_66=Fork_66]] & Catch2_52=Fork_52] & Catch2_61=Fork_61] & Catch2_56=Fork_56] & Catch2_55=Fork_55]] & Catch2_94=Fork_94] & Catch2_78=Fork_78] & Catch2_57=Fork_57] & Catch2_39=Fork_39] & Catch2_53=Fork_53] & Catch2_3=Fork_3] & Catch2_91=Fork_91] & Catch2_79=Fork_79] & Catch2_1=Fork_1]] & Catch2_95=Fork_95] & Catch2_98=Fork_98] & Catch2_23=Fork_23] & Catch2_14=Fork_14] & Catch2_74=Fork_74] & Catch2_44=Fork_44] & Catch2_45=Fork_45] & Catch2_92=Fork_92] & Catch2_29=Fork_29]] & Catch2_69=Fork_69] & Catch2_11=Fork_11] & Catch2_13=Fork_13] & Catch2_34=Fork_34] & Catch2_31=Fork_31] & Catch2_15=Fork_15]] & Catch2_38=Fork_38]] & Catch2_60=Fork_60]] & Catch2_67=Fork_67] & Catch2_82=Fork_82]] & Catch2_9=Fork_9] & Catch2_71=Fork_71] & Catch2_18=Fork_18] & Catch2_19=Fork_19]] & Catch2_65=Fork_65] & Catch2_51=Fork_51] & Catch2_83=Fork_83] & Catch2_72=Fork_72] & Catch2_21=Fork_21] & Catch2_24=Fork_24] & Catch2_20=Fork_20] & Catch2_80=Fork_80]] & Catch2_62=Fork_62] & Catch2_47=Fork_47] & Catch2_73=Fork_73]]]
normalized: ~ [E [true U ~ [[[Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_10_placecomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[[[[[[[Catch1_69!=Eat_69 & [[[[[[[[[[[[[Catch1_17!=Eat_17 & [[[[[Catch1_1!=Eat_1 & [[[[[[[[[[[[[[[[[[[[[[Catch1_54!=Eat_54 & [[[[[[[[[[[Catch1_76!=Eat_76 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch1_97!=Eat_97 & [[[[true & Catch1_11!=Eat_11] & Catch1_7!=Eat_7] & Catch1_72!=Eat_72] & Catch1_52!=Eat_52]] & Catch1_95!=Eat_95] & Catch1_29!=Eat_29] & Catch1_55!=Eat_55] & Catch1_36!=Eat_36] & Catch1_49!=Eat_49] & Catch1_62!=Eat_62] & Catch1_18!=Eat_18] & Catch1_98!=Eat_98] & Catch1_47!=Eat_47] & Catch1_51!=Eat_51] & Catch1_87!=Eat_87] & Catch1_45!=Eat_45] & Catch1_6!=Eat_6] & Catch1_32!=Eat_32] & Catch1_59!=Eat_59] & Catch1_50!=Eat_50] & Catch1_57!=Eat_57] & Catch1_12!=Eat_12] & Catch1_85!=Eat_85] & Catch1_96!=Eat_96] & Catch1_30!=Eat_30] & Catch1_35!=Eat_35] & Catch1_20!=Eat_20] & Catch1_73!=Eat_73] & Catch1_81!=Eat_81] & Catch1_22!=Eat_22] & Catch1_78!=Eat_78] & Catch1_86!=Eat_86] & Catch1_19!=Eat_19] & Catch1_70!=Eat_70] & Catch1_71!=Eat_71] & Catch1_5!=Eat_5] & Catch1_3!=Eat_3] & Catch1_28!=Eat_28] & Catch1_94!=Eat_94] & Catch1_8!=Eat_8]] & Catch1_31!=Eat_31] & Catch1_89!=Eat_89] & Catch1_90!=Eat_90] & Catch1_61!=Eat_61] & Catch1_99!=Eat_99] & Catch1_63!=Eat_63] & Catch1_65!=Eat_65] & Catch1_4!=Eat_4] & Catch1_58!=Eat_58] & Catch1_53!=Eat_53]] & Catch1_9!=Eat_9] & Catch1_56!=Eat_56] & Catch1_26!=Eat_26] & Catch1_92!=Eat_92] & Catch1_38!=Eat_38] & Catch1_68!=Eat_68] & Catch1_44!=Eat_44] & Catch1_27!=Eat_27] & Catch1_100!=Eat_100] & Catch1_48!=Eat_48] & Catch1_13!=Eat_13] & Catch1_66!=Eat_66] & Catch1_91!=Eat_91] & Catch1_79!=Eat_79] & Catch1_74!=Eat_74] & Catch1_80!=Eat_80] & Catch1_33!=Eat_33] & Catch1_46!=Eat_46] & Catch1_88!=Eat_88] & Catch1_60!=Eat_60] & Catch1_2!=Eat_2]] & Catch1_75!=Eat_75] & Catch1_15!=Eat_15] & Catch1_77!=Eat_77] & Catch1_42!=Eat_42]] & Catch1_67!=Eat_67] & Catch1_10!=Eat_10] & Catch1_23!=Eat_23] & Catch1_25!=Eat_25] & Catch1_83!=Eat_83] & Catch1_34!=Eat_34] & Catch1_14!=Eat_14] & Catch1_84!=Eat_84] & Catch1_21!=Eat_21] & Catch1_43!=Eat_43] & Catch1_37!=Eat_37] & Catch1_40!=Eat_40]] & Catch1_64!=Eat_64] & Catch1_24!=Eat_24] & Catch1_93!=Eat_93] & Catch1_41!=Eat_41] & Catch1_39!=Eat_39] & Catch1_16!=Eat_16] & Catch1_82!=Eat_82]] <-> [[[[[[Catch2_20=Fork_20 & [[[[[[[Catch2_88=Fork_88 & [[[[[[[[[[[[[[[[[[[[[[Catch2_45=Fork_45 & [[[[Catch2_23=Fork_23 & [[[[[[[[[[[Catch2_78=Fork_78 & [[[[[[[Catch2_10=Fork_10 & [[[[[[[[[[[[[[[Catch2_22=Fork_22 & [[[[[[[[[[[Catch2_37=Fork_37 & [[[[[[[[[[[[[Catch2_86=Fork_86 & [[[[true & Catch2_50=Fork_50] & Catch2_40=Fork_40] & Catch2_46=Fork_46] & Catch2_54=Fork_54]] & Catch2_42=Fork_42] & Catch2_6=Fork_6] & Catch2_27=Fork_27] & Catch2_33=Fork_33] & Catch2_99=Fork_99] & Catch2_68=Fork_68] & Catch2_84=Fork_84] & Catch2_4=Fork_4] & Catch2_85=Fork_85] & Catch2_81=Fork_81] & Catch2_43=Fork_43] & Catch2_36=Fork_36]] & Catch2_100=Fork_100] & Catch2_63=Fork_63] & Catch2_64=Fork_64] & Catch2_41=Fork_41] & Catch2_35=Fork_35] & Catch2_59=Fork_59] & Catch2_93=Fork_93] & Catch2_2=Fork_2] & Catch2_70=Fork_70] & Catch2_8=Fork_8]] & Catch2_89=Fork_89] & Catch2_96=Fork_96] & Catch2_97=Fork_97] & Catch2_30=Fork_30] & Catch2_28=Fork_28] & Catch2_5=Fork_5] & Catch2_16=Fork_16] & Catch2_12=Fork_12] & Catch2_7=Fork_7] & Catch2_87=Fork_87] & Catch2_17=Fork_17] & Catch2_32=Fork_32] & Catch2_25=Fork_25] & Catch2_66=Fork_66]] & Catch2_52=Fork_52] & Catch2_61=Fork_61] & Catch2_56=Fork_56] & Catch2_55=Fork_55] & Catch2_90=Fork_90] & Catch2_94=Fork_94]] & Catch2_57=Fork_57] & Catch2_39=Fork_39] & Catch2_53=Fork_53] & Catch2_3=Fork_3] & Catch2_91=Fork_91] & Catch2_79=Fork_79] & Catch2_1=Fork_1] & Catch2_58=Fork_58] & Catch2_95=Fork_95] & Catch2_98=Fork_98]] & Catch2_14=Fork_14] & Catch2_74=Fork_74] & Catch2_44=Fork_44]] & Catch2_92=Fork_92] & Catch2_29=Fork_29] & Catch2_77=Fork_77] & Catch2_69=Fork_69] & Catch2_11=Fork_11] & Catch2_13=Fork_13] & Catch2_34=Fork_34] & Catch2_31=Fork_31] & Catch2_15=Fork_15] & Catch2_75=Fork_75] & Catch2_38=Fork_38] & Catch2_49=Fork_49] & Catch2_60=Fork_60] & Catch2_26=Fork_26] & Catch2_67=Fork_67] & Catch2_82=Fork_82] & Catch2_76=Fork_76] & Catch2_9=Fork_9] & Catch2_71=Fork_71] & Catch2_18=Fork_18] & Catch2_19=Fork_19]] & Catch2_65=Fork_65] & Catch2_51=Fork_51] & Catch2_83=Fork_83] & Catch2_72=Fork_72] & Catch2_21=Fork_21] & Catch2_24=Fork_24]] & Catch2_80=Fork_80] & Catch2_48=Fork_48] & Catch2_62=Fork_62] & Catch2_47=Fork_47] & Catch2_73=Fork_73]]]
normalized: ~ [E [true U ~ [[[[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & ~ [[Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [~ [[Catch1_82!=Eat_82 & [Catch1_16!=Eat_16 & [Catch1_39!=Eat_39 & [Catch1_41!=Eat_41 & [Catch1_93!=Eat_93 & [Catch1_24!=Eat_24 & [Catch1_64!=Eat_64 & [Catch1_69!=Eat_69 & [Catch1_40!=Eat_40 & [Catch1_37!=Eat_37 & [Catch1_43!=Eat_43 & [Catch1_21!=Eat_21 & [Catch1_84!=Eat_84 & [Catch1_14!=Eat_14 & [Catch1_34!=Eat_34 & [Catch1_83!=Eat_83 & [Catch1_25!=Eat_25 & [Catch1_23!=Eat_23 & [Catch1_10!=Eat_10 & [Catch1_67!=Eat_67 & [Catch1_17!=Eat_17 & [Catch1_42!=Eat_42 & [Catch1_77!=Eat_77 & [Catch1_15!=Eat_15 & [Catch1_75!=Eat_75 & [Catch1_1!=Eat_1 & [Catch1_2!=Eat_2 & [Catch1_60!=Eat_60 & [Catch1_88!=Eat_88 & [Catch1_46!=Eat_46 & [Catch1_33!=Eat_33 & [Catch1_80!=Eat_80 & [Catch1_74!=Eat_74 & [Catch1_79!=Eat_79 & [Catch1_91!=Eat_91 & [Catch1_66!=Eat_66 & [Catch1_13!=Eat_13 & [Catch1_48!=Eat_48 & [Catch1_100!=Eat_100 & [Catch1_27!=Eat_27 & [Catch1_44!=Eat_44 & [Catch1_68!=Eat_68 & [Catch1_38!=Eat_38 & [Catch1_92!=Eat_92 & [Catch1_26!=Eat_26 & [Catch1_56!=Eat_56 & [Catch1_9!=Eat_9 & [Catch1_54!=Eat_54 & [Catch1_53!=Eat_53 & [Catch1_58!=Eat_58 & [Catch1_4!=Eat_4 & [Catch1_65!=Eat_65 & [Catch1_63!=Eat_63 & [Catch1_99!=Eat_99 & [Catch1_61!=Eat_61 & [Catch1_90!=Eat_90 & [Catch1_89!=Eat_89 & [Catch1_31!=Eat_31 & [Catch1_76!=Eat_76 & [Catch1_8!=Eat_8 & [Catch1_94!=Eat_94 & [Catch1_28!=Eat_28 & [Catch1_3!=Eat_3 & [Catch1_5!=Eat_5 & [Catch1_71!=Eat_71 & [Catch1_70!=Eat_70 & [Catch1_19!=Eat_19 & [Catch1_86!=Eat_86 & [Catch1_78!=Eat_78 & [Catch1_22!=Eat_22 & [Catch1_81!=Eat_81 & [Catch1_73!=Eat_73 & [Catch1_20!=Eat_20 & [Catch1_35!=Eat_35 & [Catch1_30!=Eat_30 & [Catch1_96!=Eat_96 & [Catch1_85!=Eat_85 & [Catch1_12!=Eat_12 & [Catch1_57!=Eat_57 & [Catch1_50!=Eat_50 & [Catch1_59!=Eat_59 & [Catch1_32!=Eat_32 & [Catch1_6!=Eat_6 & [Catch1_45!=Eat_45 & [Catch1_87!=Eat_87 & [Catch1_51!=Eat_51 & [Catch1_47!=Eat_47 & [Catch1_98!=Eat_98 & [Catch1_18!=Eat_18 & [Catch1_62!=Eat_62 & [Catch1_49!=Eat_49 & [Catch1_36!=Eat_36 & [Catch1_55!=Eat_55 & [Catch1_29!=Eat_29 & [Catch1_95!=Eat_95 & [Catch1_97!=Eat_97 & [Catch1_52!=Eat_52 & [Catch1_72!=Eat_72 & [Catch1_7!=Eat_7 & [Catch1_11!=Eat_11 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [Catch2_80=Fork_80 & [Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [Catch2_21=Fork_21 & [Catch2_72=Fork_72 & [Catch2_83=Fork_83 & [Catch2_51=Fork_51 & [Catch2_65=Fork_65 & [Catch2_88=Fork_88 & [Catch2_19=Fork_19 & [Catch2_18=Fork_18 & [Catch2_71=Fork_71 & [Catch2_9=Fork_9 & [Catch2_76=Fork_76 & [Catch2_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [Catch2_75=Fork_75 & [Catch2_15=Fork_15 & [Catch2_31=Fork_31 & [Catch2_34=Fork_34 & [Catch2_13=Fork_13 & [Catch2_11=Fork_11 & [Catch2_69=Fork_69 & [Catch2_77=Fork_77 & [Catch2_29=Fork_29 & [Catch2_92=Fork_92 & [Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [Catch2_14=Fork_14 & [Catch2_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [Catch2_91=Fork_91 & [Catch2_3=Fork_3 & [Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [Catch2_94=Fork_94 & [Catch2_90=Fork_90 & [Catch2_55=Fork_55 & [Catch2_56=Fork_56 & [Catch2_61=Fork_61 & [Catch2_52=Fork_52 & [Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [Catch2_87=Fork_87 & [Catch2_7=Fork_7 & [Catch2_12=Fork_12 & [Catch2_16=Fork_16 & [Catch2_5=Fork_5 & [Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [Catch2_89=Fork_89 & [Catch2_22=Fork_22 & [Catch2_8=Fork_8 & [Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [Catch2_35=Fork_35 & [Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [Catch2_63=Fork_63 & [Catch2_100=Fork_100 & [Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [Catch2_81=Fork_81 & [Catch2_85=Fork_85 & [Catch2_4=Fork_4 & [Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [Catch2_42=Fork_42 & [Catch2_86=Fork_86 & [Catch2_54=Fork_54 & [Catch2_46=Fork_46 & [Catch2_40=Fork_40 & [Catch2_50=Fork_50 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_11_placecomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[Eat_42>Catch2_42 | [[[[[[[[Eat_8>Catch2_8 | [[[[[[[[[[[[[Eat_61>Catch2_61 | [[[[[Eat_48>Catch2_48 | [[[[[Eat_39>Catch2_39 | [[Eat_31>Catch2_31 | [[[[[Eat_44>Catch2_44 | [[[[[[[[[[[[[[[[[[[[[[Eat_40>Catch2_40 | [[Eat_24>Catch2_24 | [[Eat_29>Catch2_29 | [[[[[Eat_32>Catch2_32 | [[Eat_9>Catch2_9 | [[Eat_73>Catch2_73 | [[[[[[[[[[[Eat_46>Catch2_46 | [[[[[[Eat_92>Catch2_92 | [[Eat_59>Catch2_59 | [[[false | Eat_85>Catch2_85] | Eat_16>Catch2_16] | Eat_67>Catch2_67]] | Eat_51>Catch2_51]] | Eat_65>Catch2_65] | Eat_23>Catch2_23] | Eat_22>Catch2_22] | Eat_97>Catch2_97] | Eat_89>Catch2_89]] | Eat_37>Catch2_37] | Eat_81>Catch2_81] | Eat_87>Catch2_87] | Eat_19>Catch2_19] | Eat_50>Catch2_50] | Eat_26>Catch2_26] | Eat_3>Catch2_3] | Eat_13>Catch2_13] | Eat_93>Catch2_93] | Eat_1>Catch2_1]] | Eat_28>Catch2_28]] | Eat_53>Catch2_53]] | Eat_69>Catch2_69] | Eat_2>Catch2_2] | Eat_5>Catch2_5] | Eat_77>Catch2_77]] | Eat_82>Catch2_82]] | Eat_70>Catch2_70]] | Eat_78>Catch2_78] | Eat_4>Catch2_4] | Eat_27>Catch2_27] | Eat_84>Catch2_84] | Eat_95>Catch2_95] | Eat_35>Catch2_35] | Eat_20>Catch2_20] | Eat_79>Catch2_79] | Eat_91>Catch2_91] | Eat_14>Catch2_14] | Eat_98>Catch2_98] | Eat_99>Catch2_99] | Eat_86>Catch2_86] | Eat_38>Catch2_38] | Eat_62>Catch2_62] | Eat_43>Catch2_43] | Eat_94>Catch2_94] | Eat_64>Catch2_64] | Eat_25>Catch2_25] | Eat_10>Catch2_10] | Eat_18>Catch2_18]] | Eat_76>Catch2_76] | Eat_71>Catch2_71] | Eat_74>Catch2_74] | Eat_55>Catch2_55]] | Eat_7>Catch2_7]] | Eat_21>Catch2_21] | Eat_11>Catch2_11] | Eat_47>Catch2_47] | Eat_80>Catch2_80]] | Eat_45>Catch2_45] | Eat_66>Catch2_66] | Eat_49>Catch2_49] | Eat_72>Catch2_72]] | Eat_90>Catch2_90] | Eat_83>Catch2_83] | Eat_96>Catch2_96] | Eat_56>Catch2_56] | Eat_54>Catch2_54] | Eat_57>Catch2_57] | Eat_12>Catch2_12] | Eat_63>Catch2_63] | Eat_36>Catch2_36] | Eat_68>Catch2_68] | Eat_100>Catch2_100] | Eat_33>Catch2_33]] | Eat_41>Catch2_41] | Eat_30>Catch2_30] | Eat_58>Catch2_58] | Eat_15>Catch2_15] | Eat_75>Catch2_75] | Eat_6>Catch2_6] | Eat_52>Catch2_52]] | Eat_60>Catch2_60] | Eat_34>Catch2_34] | Eat_88>Catch2_88] | Eat_17>Catch2_17] | false] & [[[[[[[[[[[[[[[[[[[Eat_63>Catch2_63 & [[[[[[Eat_83>Catch2_83 & [[[[Eat_49>Catch2_49 & [[Eat_45>Catch2_45 & [[[[Eat_11>Catch2_11 & [[Eat_39>Catch2_39 & [[[[[[[[[Eat_10>Catch2_10 & [[[[Eat_43>Catch2_43 & [[[[[[[[[Eat_20>Catch2_20 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Eat_85>Catch2_85] & Eat_16>Catch2_16] & Eat_67>Catch2_67] & Eat_59>Catch2_59] & Eat_51>Catch2_51] & Eat_92>Catch2_92] & Eat_65>Catch2_65] & Eat_23>Catch2_23] & Eat_22>Catch2_22] & Eat_97>Catch2_97] & Eat_89>Catch2_89] & Eat_46>Catch2_46] & Eat_37>Catch2_37] & Eat_81>Catch2_81] & Eat_87>Catch2_87] & Eat_19>Catch2_19] & Eat_50>Catch2_50] & Eat_26>Catch2_26] & Eat_3>Catch2_3] & Eat_13>Catch2_13] & Eat_93>Catch2_93] & Eat_1>Catch2_1] & Eat_73>Catch2_73] & Eat_28>Catch2_28] & Eat_9>Catch2_9] & Eat_53>Catch2_53] & Eat_32>Catch2_32] & Eat_69>Catch2_69] & Eat_2>Catch2_2] & Eat_5>Catch2_5] & Eat_77>Catch2_77] & Eat_29>Catch2_29] & Eat_82>Catch2_82] & Eat_24>Catch2_24] & Eat_70>Catch2_70] & Eat_40>Catch2_40] & Eat_78>Catch2_78] & Eat_4>Catch2_4] & Eat_27>Catch2_27] & Eat_84>Catch2_84] & Eat_95>Catch2_95] & Eat_35>Catch2_35]] & Eat_79>Catch2_79] & Eat_91>Catch2_91] & Eat_14>Catch2_14] & Eat_98>Catch2_98] & Eat_99>Catch2_99] & Eat_86>Catch2_86] & Eat_38>Catch2_38] & Eat_62>Catch2_62]] & Eat_94>Catch2_94] & Eat_64>Catch2_64] & Eat_25>Catch2_25]] & Eat_18>Catch2_18] & Eat_44>Catch2_44] & Eat_76>Catch2_76] & Eat_71>Catch2_71] & Eat_74>Catch2_74] & Eat_55>Catch2_55] & Eat_31>Catch2_31] & Eat_7>Catch2_7]] & Eat_21>Catch2_21]] & Eat_47>Catch2_47] & Eat_80>Catch2_80] & Eat_48>Catch2_48]] & Eat_66>Catch2_66]] & Eat_72>Catch2_72] & Eat_61>Catch2_61] & Eat_90>Catch2_90]] & Eat_96>Catch2_96] & Eat_56>Catch2_56] & Eat_54>Catch2_54] & Eat_57>Catch2_57] & Eat_12>Catch2_12]] & Eat_36>Catch2_36] & Eat_68>Catch2_68] & Eat_100>Catch2_100] & Eat_33>Catch2_33] & Eat_8>Catch2_8] & Eat_41>Catch2_41] & Eat_30>Catch2_30] & Eat_58>Catch2_58] & Eat_15>Catch2_15] & Eat_75>Catch2_75] & Eat_6>Catch2_6] & Eat_52>Catch2_52] & Eat_42>Catch2_42] & Eat_60>Catch2_60] & Eat_34>Catch2_34] & Eat_88>Catch2_88] & Eat_17>Catch2_17] & true]] & [true & [[[[[[[[Eat_75<=Catch2_75 & [[[[[[[[[Eat_36<=Catch2_36 & [[[Eat_57<=Catch2_57 & [[[Eat_96<=Catch2_96 & [[[[[[Eat_66<=Catch2_66 & [[[[[[[[[[[Eat_74<=Catch2_74 & [[[[[[[[[[[[[[[[[[[[[[[[[Eat_40<=Catch2_40 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_65<=Catch2_65 & [[[[[[true & Eat_85<=Catch2_85] & Eat_16<=Catch2_16] & Eat_67<=Catch2_67] & Eat_59<=Catch2_59] & Eat_51<=Catch2_51] & Eat_92<=Catch2_92]] & Eat_23<=Catch2_23] & Eat_22<=Catch2_22] & Eat_97<=Catch2_97] & Eat_89<=Catch2_89] & Eat_46<=Catch2_46] & Eat_37<=Catch2_37] & Eat_81<=Catch2_81] & Eat_87<=Catch2_87] & Eat_19<=Catch2_19] & Eat_50<=Catch2_50] & Eat_26<=Catch2_26] & Eat_3<=Catch2_3] & Eat_13<=Catch2_13] & Eat_93<=Catch2_93] & Eat_1<=Catch2_1] & Eat_73<=Catch2_73] & Eat_28<=Catch2_28] & Eat_9<=Catch2_9] & Eat_53<=Catch2_53] & Eat_32<=Catch2_32] & Eat_69<=Catch2_69] & Eat_2<=Catch2_2] & Eat_5<=Catch2_5] & Eat_77<=Catch2_77] & Eat_29<=Catch2_29] & Eat_82<=Catch2_82] & Eat_24<=Catch2_24] & Eat_70<=Catch2_70]] & Eat_78<=Catch2_78] & Eat_4<=Catch2_4] & Eat_27<=Catch2_27] & Eat_84<=Catch2_84] & Eat_95<=Catch2_95] & Eat_35<=Catch2_35] & Eat_20<=Catch2_20] & Eat_79<=Catch2_79] & Eat_91<=Catch2_91] & Eat_14<=Catch2_14] & Eat_98<=Catch2_98] & Eat_99<=Catch2_99] & Eat_86<=Catch2_86] & Eat_38<=Catch2_38] & Eat_62<=Catch2_62] & Eat_43<=Catch2_43] & Eat_94<=Catch2_94] & Eat_64<=Catch2_64] & Eat_25<=Catch2_25] & Eat_10<=Catch2_10] & Eat_18<=Catch2_18] & Eat_44<=Catch2_44] & Eat_76<=Catch2_76] & Eat_71<=Catch2_71]] & Eat_55<=Catch2_55] & Eat_31<=Catch2_31] & Eat_7<=Catch2_7] & Eat_39<=Catch2_39] & Eat_21<=Catch2_21] & Eat_11<=Catch2_11] & Eat_47<=Catch2_47] & Eat_80<=Catch2_80] & Eat_48<=Catch2_48] & Eat_45<=Catch2_45]] & Eat_49<=Catch2_49] & Eat_72<=Catch2_72] & Eat_61<=Catch2_61] & Eat_90<=Catch2_90] & Eat_83<=Catch2_83]] & Eat_56<=Catch2_56] & Eat_54<=Catch2_54]] & Eat_12<=Catch2_12] & Eat_63<=Catch2_63]] & Eat_68<=Catch2_68] & Eat_100<=Catch2_100] & Eat_33<=Catch2_33] & Eat_8<=Catch2_8] & Eat_41<=Catch2_41] & Eat_30<=Catch2_30] & Eat_58<=Catch2_58] & Eat_15<=Catch2_15]] & Eat_6<=Catch2_6] & Eat_52<=Catch2_52] & Eat_42<=Catch2_42] & Eat_60<=Catch2_60] & Eat_34<=Catch2_34] & Eat_88<=Catch2_88] & Eat_17<=Catch2_17]]]]
normalized: ~ [E [true U ~ [[[[Eat_17<=Catch2_17 & [Eat_88<=Catch2_88 & [Eat_34<=Catch2_34 & [Eat_60<=Catch2_60 & [Eat_42<=Catch2_42 & [Eat_52<=Catch2_52 & [Eat_6<=Catch2_6 & [Eat_75<=Catch2_75 & [Eat_15<=Catch2_15 & [Eat_58<=Catch2_58 & [Eat_30<=Catch2_30 & [Eat_41<=Catch2_41 & [Eat_8<=Catch2_8 & [Eat_33<=Catch2_33 & [Eat_100<=Catch2_100 & [Eat_68<=Catch2_68 & [Eat_36<=Catch2_36 & [Eat_63<=Catch2_63 & [Eat_12<=Catch2_12 & [Eat_57<=Catch2_57 & [Eat_54<=Catch2_54 & [Eat_56<=Catch2_56 & [Eat_96<=Catch2_96 & [Eat_83<=Catch2_83 & [Eat_90<=Catch2_90 & [Eat_61<=Catch2_61 & [Eat_72<=Catch2_72 & [Eat_49<=Catch2_49 & [Eat_66<=Catch2_66 & [Eat_45<=Catch2_45 & [Eat_48<=Catch2_48 & [Eat_80<=Catch2_80 & [Eat_47<=Catch2_47 & [Eat_11<=Catch2_11 & [Eat_21<=Catch2_21 & [Eat_39<=Catch2_39 & [Eat_7<=Catch2_7 & [Eat_31<=Catch2_31 & [Eat_55<=Catch2_55 & [Eat_74<=Catch2_74 & [Eat_71<=Catch2_71 & [Eat_76<=Catch2_76 & [Eat_44<=Catch2_44 & [Eat_18<=Catch2_18 & [Eat_10<=Catch2_10 & [Eat_25<=Catch2_25 & [Eat_64<=Catch2_64 & [Eat_94<=Catch2_94 & [Eat_43<=Catch2_43 & [Eat_62<=Catch2_62 & [Eat_38<=Catch2_38 & [Eat_86<=Catch2_86 & [Eat_99<=Catch2_99 & [Eat_98<=Catch2_98 & [Eat_14<=Catch2_14 & [Eat_91<=Catch2_91 & [Eat_79<=Catch2_79 & [Eat_20<=Catch2_20 & [Eat_35<=Catch2_35 & [Eat_95<=Catch2_95 & [Eat_84<=Catch2_84 & [Eat_27<=Catch2_27 & [Eat_4<=Catch2_4 & [Eat_78<=Catch2_78 & [Eat_40<=Catch2_40 & [Eat_70<=Catch2_70 & [Eat_24<=Catch2_24 & [Eat_82<=Catch2_82 & [Eat_29<=Catch2_29 & [Eat_77<=Catch2_77 & [Eat_5<=Catch2_5 & [Eat_2<=Catch2_2 & [Eat_69<=Catch2_69 & [Eat_32<=Catch2_32 & [Eat_53<=Catch2_53 & [Eat_9<=Catch2_9 & [Eat_28<=Catch2_28 & [Eat_73<=Catch2_73 & [Eat_1<=Catch2_1 & [Eat_93<=Catch2_93 & [Eat_13<=Catch2_13 & [Eat_3<=Catch2_3 & [Eat_26<=Catch2_26 & [Eat_50<=Catch2_50 & [Eat_19<=Catch2_19 & [Eat_87<=Catch2_87 & [Eat_81<=Catch2_81 & [Eat_37<=Catch2_37 & [Eat_46<=Catch2_46 & [Eat_89<=Catch2_89 & [Eat_97<=Catch2_97 & [Eat_22<=Catch2_22 & [Eat_23<=Catch2_23 & [Eat_65<=Catch2_65 & [Eat_92<=Catch2_92 & [Eat_51<=Catch2_51 & [Eat_59<=Catch2_59 & [Eat_67<=Catch2_67 & [Eat_16<=Catch2_16 & [Eat_85<=Catch2_85 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & true] & [[true & [Eat_17>Catch2_17 & [Eat_88>Catch2_88 & [Eat_34>Catch2_34 & [Eat_60>Catch2_60 & [Eat_42>Catch2_42 & [Eat_52>Catch2_52 & [Eat_6>Catch2_6 & [Eat_75>Catch2_75 & [Eat_15>Catch2_15 & [Eat_58>Catch2_58 & [Eat_30>Catch2_30 & [Eat_41>Catch2_41 & [Eat_8>Catch2_8 & [Eat_33>Catch2_33 & [Eat_100>Catch2_100 & [Eat_68>Catch2_68 & [Eat_36>Catch2_36 & [Eat_63>Catch2_63 & [Eat_12>Catch2_12 & [Eat_57>Catch2_57 & [Eat_54>Catch2_54 & [Eat_56>Catch2_56 & [Eat_96>Catch2_96 & [Eat_83>Catch2_83 & [Eat_90>Catch2_90 & [Eat_61>Catch2_61 & [Eat_72>Catch2_72 & [Eat_49>Catch2_49 & [Eat_66>Catch2_66 & [Eat_45>Catch2_45 & [Eat_48>Catch2_48 & [Eat_80>Catch2_80 & [Eat_47>Catch2_47 & [Eat_11>Catch2_11 & [Eat_21>Catch2_21 & [Eat_39>Catch2_39 & [Eat_7>Catch2_7 & [Eat_31>Catch2_31 & [Eat_55>Catch2_55 & [Eat_74>Catch2_74 & [Eat_71>Catch2_71 & [Eat_76>Catch2_76 & [Eat_44>Catch2_44 & [Eat_18>Catch2_18 & [Eat_10>Catch2_10 & [Eat_25>Catch2_25 & [Eat_64>Catch2_64 & [Eat_94>Catch2_94 & [Eat_43>Catch2_43 & [Eat_62>Catch2_62 & [Eat_38>Catch2_38 & [Eat_86>Catch2_86 & [Eat_99>Catch2_99 & [Eat_98>Catch2_98 & [Eat_14>Catch2_14 & [Eat_91>Catch2_91 & [Eat_79>Catch2_79 & [Eat_20>Catch2_20 & [Eat_35>Catch2_35 & [Eat_95>Catch2_95 & [Eat_84>Catch2_84 & [Eat_27>Catch2_27 & [Eat_4>Catch2_4 & [Eat_78>Catch2_78 & [Eat_40>Catch2_40 & [Eat_70>Catch2_70 & [Eat_24>Catch2_24 & [Eat_82>Catch2_82 & [Eat_29>Catch2_29 & [Eat_77>Catch2_77 & [Eat_5>Catch2_5 & [Eat_2>Catch2_2 & [Eat_69>Catch2_69 & [Eat_32>Catch2_32 & [Eat_53>Catch2_53 & [Eat_9>Catch2_9 & [Eat_28>Catch2_28 & [Eat_73>Catch2_73 & [Eat_1>Catch2_1 & [Eat_93>Catch2_93 & [Eat_13>Catch2_13 & [Eat_3>Catch2_3 & [Eat_26>Catch2_26 & [Eat_50>Catch2_50 & [Eat_19>Catch2_19 & [Eat_87>Catch2_87 & [Eat_81>Catch2_81 & [Eat_37>Catch2_37 & [Eat_46>Catch2_46 & [Eat_89>Catch2_89 & [Eat_97>Catch2_97 & [Eat_22>Catch2_22 & [Eat_23>Catch2_23 & [Eat_65>Catch2_65 & [Eat_92>Catch2_92 & [Eat_51>Catch2_51 & [Eat_59>Catch2_59 & [Eat_67>Catch2_67 & [Eat_16>Catch2_16 & [Eat_85>Catch2_85 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [false | [Eat_17>Catch2_17 | [Eat_88>Catch2_88 | [Eat_34>Catch2_34 | [Eat_60>Catch2_60 | [Eat_42>Catch2_42 | [Eat_52>Catch2_52 | [Eat_6>Catch2_6 | [Eat_75>Catch2_75 | [Eat_15>Catch2_15 | [Eat_58>Catch2_58 | [Eat_30>Catch2_30 | [Eat_41>Catch2_41 | [Eat_8>Catch2_8 | [Eat_33>Catch2_33 | [Eat_100>Catch2_100 | [Eat_68>Catch2_68 | [Eat_36>Catch2_36 | [Eat_63>Catch2_63 | [Eat_12>Catch2_12 | [Eat_57>Catch2_57 | [Eat_54>Catch2_54 | [Eat_56>Catch2_56 | [Eat_96>Catch2_96 | [Eat_83>Catch2_83 | [Eat_90>Catch2_90 | [Eat_61>Catch2_61 | [Eat_72>Catch2_72 | [Eat_49>Catch2_49 | [Eat_66>Catch2_66 | [Eat_45>Catch2_45 | [Eat_48>Catch2_48 | [Eat_80>Catch2_80 | [Eat_47>Catch2_47 | [Eat_11>Catch2_11 | [Eat_21>Catch2_21 | [Eat_39>Catch2_39 | [Eat_7>Catch2_7 | [Eat_31>Catch2_31 | [Eat_55>Catch2_55 | [Eat_74>Catch2_74 | [Eat_71>Catch2_71 | [Eat_76>Catch2_76 | [Eat_44>Catch2_44 | [Eat_18>Catch2_18 | [Eat_10>Catch2_10 | [Eat_25>Catch2_25 | [Eat_64>Catch2_64 | [Eat_94>Catch2_94 | [Eat_43>Catch2_43 | [Eat_62>Catch2_62 | [Eat_38>Catch2_38 | [Eat_86>Catch2_86 | [Eat_99>Catch2_99 | [Eat_98>Catch2_98 | [Eat_14>Catch2_14 | [Eat_91>Catch2_91 | [Eat_79>Catch2_79 | [Eat_20>Catch2_20 | [Eat_35>Catch2_35 | [Eat_95>Catch2_95 | [Eat_84>Catch2_84 | [Eat_27>Catch2_27 | [Eat_4>Catch2_4 | [Eat_78>Catch2_78 | [Eat_40>Catch2_40 | [Eat_70>Catch2_70 | [Eat_24>Catch2_24 | [Eat_82>Catch2_82 | [Eat_29>Catch2_29 | [Eat_77>Catch2_77 | [Eat_5>Catch2_5 | [Eat_2>Catch2_2 | [Eat_69>Catch2_69 | [Eat_32>Catch2_32 | [Eat_53>Catch2_53 | [Eat_9>Catch2_9 | [Eat_28>Catch2_28 | [Eat_73>Catch2_73 | [Eat_1>Catch2_1 | [Eat_93>Catch2_93 | [Eat_13>Catch2_13 | [Eat_3>Catch2_3 | [Eat_26>Catch2_26 | [Eat_50>Catch2_50 | [Eat_19>Catch2_19 | [Eat_87>Catch2_87 | [Eat_81>Catch2_81 | [Eat_37>Catch2_37 | [Eat_46>Catch2_46 | [Eat_89>Catch2_89 | [Eat_97>Catch2_97 | [Eat_22>Catch2_22 | [Eat_23>Catch2_23 | [Eat_65>Catch2_65 | [Eat_92>Catch2_92 | [Eat_51>Catch2_51 | [Eat_59>Catch2_59 | [Eat_67>Catch2_67 | [Eat_16>Catch2_16 | [Eat_85>Catch2_85 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_12_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Eat_85<=Catch2_85] & Eat_16<=Catch2_16] & Eat_67<=Catch2_67] & Eat_59<=Catch2_59] & Eat_51<=Catch2_51] & Eat_92<=Catch2_92] & Eat_65<=Catch2_65] & Eat_23<=Catch2_23] & Eat_22<=Catch2_22] & Eat_97<=Catch2_97] & Eat_89<=Catch2_89] & Eat_46<=Catch2_46] & Eat_37<=Catch2_37] & Eat_81<=Catch2_81] & Eat_87<=Catch2_87] & Eat_19<=Catch2_19] & Eat_50<=Catch2_50] & Eat_26<=Catch2_26] & Eat_3<=Catch2_3] & Eat_13<=Catch2_13] & Eat_93<=Catch2_93] & Eat_1<=Catch2_1] & Eat_73<=Catch2_73] & Eat_28<=Catch2_28] & Eat_9<=Catch2_9] & Eat_53<=Catch2_53] & Eat_32<=Catch2_32] & Eat_69<=Catch2_69] & Eat_2<=Catch2_2] & Eat_5<=Catch2_5] & Eat_77<=Catch2_77] & Eat_29<=Catch2_29] & Eat_82<=Catch2_82] & Eat_24<=Catch2_24] & Eat_70<=Catch2_70] & Eat_40<=Catch2_40] & Eat_78<=Catch2_78] & Eat_4<=Catch2_4] & Eat_27<=Catch2_27] & Eat_84<=Catch2_84] & Eat_95<=Catch2_95] & Eat_35<=Catch2_35] & Eat_20<=Catch2_20] & Eat_79<=Catch2_79] & Eat_91<=Catch2_91] & Eat_14<=Catch2_14] & Eat_98<=Catch2_98] & Eat_99<=Catch2_99] & Eat_86<=Catch2_86] & Eat_38<=Catch2_38] & Eat_62<=Catch2_62] & Eat_43<=Catch2_43] & Eat_94<=Catch2_94] & Eat_64<=Catch2_64] & Eat_25<=Catch2_25] & Eat_10<=Catch2_10] & Eat_18<=Catch2_18] & Eat_44<=Catch2_44] & Eat_76<=Catch2_76] & Eat_71<=Catch2_71] & Eat_74<=Catch2_74] & Eat_55<=Catch2_55] & Eat_31<=Catch2_31] & Eat_7<=Catch2_7] & Eat_39<=Catch2_39] & Eat_21<=Catch2_21] & Eat_11<=Catch2_11] & Eat_47<=Catch2_47] & Eat_80<=Catch2_80] & Eat_48<=Catch2_48] & Eat_45<=Catch2_45] & Eat_66<=Catch2_66] & Eat_49<=Catch2_49] & Eat_72<=Catch2_72] & Eat_61<=Catch2_61] & Eat_90<=Catch2_90] & Eat_83<=Catch2_83] & Eat_96<=Catch2_96] & Eat_56<=Catch2_56] & Eat_54<=Catch2_54] & Eat_57<=Catch2_57] & Eat_12<=Catch2_12] & Eat_63<=Catch2_63] & Eat_36<=Catch2_36] & Eat_68<=Catch2_68] & Eat_100<=Catch2_100] & Eat_33<=Catch2_33] & Eat_8<=Catch2_8] & Eat_41<=Catch2_41] & Eat_30<=Catch2_30] & Eat_58<=Catch2_58] & Eat_15<=Catch2_15] & Eat_75<=Catch2_75] & Eat_6<=Catch2_6] & Eat_52<=Catch2_52] & Eat_42<=Catch2_42] & Eat_60<=Catch2_60] & Eat_34<=Catch2_34] & Eat_88<=Catch2_88] & Eat_17<=Catch2_17] & true] | [[[[[[[[[[[Eat_15>Catch2_15 & [[[[[[[[[[[[[[[[[[[Eat_49>Catch2_49 & [[[[[Eat_47>Catch2_47 & [[[[Eat_7>Catch2_7 & [[[[[[[[[Eat_25>Catch2_25 & [[[[Eat_62>Catch2_62 & [[[[[[[[[[[[[[[[Eat_70>Catch2_70 & [[[[Eat_77>Catch2_77 & [[[[[[[[[[[[[[[[[[[[[Eat_97>Catch2_97 & [[[[[[[[[true & Eat_85>Catch2_85] & Eat_16>Catch2_16] & Eat_67>Catch2_67] & Eat_59>Catch2_59] & Eat_51>Catch2_51] & Eat_92>Catch2_92] & Eat_65>Catch2_65] & Eat_23>Catch2_23] & Eat_22>Catch2_22]] & Eat_89>Catch2_89] & Eat_46>Catch2_46] & Eat_37>Catch2_37] & Eat_81>Catch2_81] & Eat_87>Catch2_87] & Eat_19>Catch2_19] & Eat_50>Catch2_50] & Eat_26>Catch2_26] & Eat_3>Catch2_3] & Eat_13>Catch2_13] & Eat_93>Catch2_93] & Eat_1>Catch2_1] & Eat_73>Catch2_73] & Eat_28>Catch2_28] & Eat_9>Catch2_9] & Eat_53>Catch2_53] & Eat_32>Catch2_32] & Eat_69>Catch2_69] & Eat_2>Catch2_2] & Eat_5>Catch2_5]] & Eat_29>Catch2_29] & Eat_82>Catch2_82] & Eat_24>Catch2_24]] & Eat_40>Catch2_40] & Eat_78>Catch2_78] & Eat_4>Catch2_4] & Eat_27>Catch2_27] & Eat_84>Catch2_84] & Eat_95>Catch2_95] & Eat_35>Catch2_35] & Eat_20>Catch2_20] & Eat_79>Catch2_79] & Eat_91>Catch2_91] & Eat_14>Catch2_14] & Eat_98>Catch2_98] & Eat_99>Catch2_99] & Eat_86>Catch2_86] & Eat_38>Catch2_38]] & Eat_43>Catch2_43] & Eat_94>Catch2_94] & Eat_64>Catch2_64]] & Eat_10>Catch2_10] & Eat_18>Catch2_18] & Eat_44>Catch2_44] & Eat_76>Catch2_76] & Eat_71>Catch2_71] & Eat_74>Catch2_74] & Eat_55>Catch2_55] & Eat_31>Catch2_31]] & Eat_39>Catch2_39] & Eat_21>Catch2_21] & Eat_11>Catch2_11]] & Eat_80>Catch2_80] & Eat_48>Catch2_48] & Eat_45>Catch2_45] & Eat_66>Catch2_66]] & Eat_72>Catch2_72] & Eat_61>Catch2_61] & Eat_90>Catch2_90] & Eat_83>Catch2_83] & Eat_96>Catch2_96] & Eat_56>Catch2_56] & Eat_54>Catch2_54] & Eat_57>Catch2_57] & Eat_12>Catch2_12] & Eat_63>Catch2_63] & Eat_36>Catch2_36] & Eat_68>Catch2_68] & Eat_100>Catch2_100] & Eat_33>Catch2_33] & Eat_8>Catch2_8] & Eat_41>Catch2_41] & Eat_30>Catch2_30] & Eat_58>Catch2_58]] & Eat_75>Catch2_75] & Eat_6>Catch2_6] & Eat_52>Catch2_52] & Eat_42>Catch2_42] & Eat_60>Catch2_60] & Eat_34>Catch2_34] & Eat_88>Catch2_88] & Eat_17>Catch2_17] & true] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Eat_85>Catch2_85] | Eat_16>Catch2_16] | Eat_67>Catch2_67] | Eat_59>Catch2_59] | Eat_51>Catch2_51] | Eat_92>Catch2_92] | Eat_65>Catch2_65] | Eat_23>Catch2_23] | Eat_22>Catch2_22] | Eat_97>Catch2_97] | Eat_89>Catch2_89] | Eat_46>Catch2_46] | Eat_37>Catch2_37] | Eat_81>Catch2_81] | Eat_87>Catch2_87] | Eat_19>Catch2_19] | Eat_50>Catch2_50] | Eat_26>Catch2_26] | Eat_3>Catch2_3] | Eat_13>Catch2_13] | Eat_93>Catch2_93] | Eat_1>Catch2_1] | Eat_73>Catch2_73] | Eat_28>Catch2_28] | Eat_9>Catch2_9] | Eat_53>Catch2_53] | Eat_32>Catch2_32] | Eat_69>Catch2_69] | Eat_2>Catch2_2] | Eat_5>Catch2_5] | Eat_77>Catch2_77] | Eat_29>Catch2_29] | Eat_82>Catch2_82] | Eat_24>Catch2_24] | Eat_70>Catch2_70] | Eat_40>Catch2_40] | Eat_78>Catch2_78] | Eat_4>Catch2_4] | Eat_27>Catch2_27] | Eat_84>Catch2_84] | Eat_95>Catch2_95] | Eat_35>Catch2_35] | Eat_20>Catch2_20] | Eat_79>Catch2_79] | Eat_91>Catch2_91] | Eat_14>Catch2_14] | Eat_98>Catch2_98] | Eat_99>Catch2_99] | Eat_86>Catch2_86] | Eat_38>Catch2_38] | Eat_62>Catch2_62] | Eat_43>Catch2_43] | Eat_94>Catch2_94] | Eat_64>Catch2_64] | Eat_25>Catch2_25] | Eat_10>Catch2_10] | Eat_18>Catch2_18] | Eat_44>Catch2_44] | Eat_76>Catch2_76] | Eat_71>Catch2_71] | Eat_74>Catch2_74] | Eat_55>Catch2_55] | Eat_31>Catch2_31] | Eat_7>Catch2_7] | Eat_39>Catch2_39] | Eat_21>Catch2_21] | Eat_11>Catch2_11] | Eat_47>Catch2_47] | Eat_80>Catch2_80] | Eat_48>Catch2_48] | Eat_45>Catch2_45] | Eat_66>Catch2_66] | Eat_49>Catch2_49] | Eat_72>Catch2_72] | Eat_61>Catch2_61] | Eat_90>Catch2_90] | Eat_83>Catch2_83] | Eat_96>Catch2_96] | Eat_56>Catch2_56] | Eat_54>Catch2_54] | Eat_57>Catch2_57] | Eat_12>Catch2_12] | Eat_63>Catch2_63] | Eat_36>Catch2_36] | Eat_68>Catch2_68] | Eat_100>Catch2_100] | Eat_33>Catch2_33] | Eat_8>Catch2_8] | Eat_41>Catch2_41] | Eat_30>Catch2_30] | Eat_58>Catch2_58] | Eat_15>Catch2_15] | Eat_75>Catch2_75] | Eat_6>Catch2_6] | Eat_52>Catch2_52] | Eat_42>Catch2_42] | Eat_60>Catch2_60] | Eat_34>Catch2_34] | Eat_88>Catch2_88] | Eat_17>Catch2_17] | false]]]]
normalized: ~ [E [true U ~ [[[[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_44>Catch2_44 | [Eat_18>Catch2_18 | [Eat_10>Catch2_10 | [Eat_25>Catch2_25 | [Eat_64>Catch2_64 | [Eat_94>Catch2_94 | [Eat_43>Catch2_43 | [Eat_62>Catch2_62 | [Eat_38>Catch2_38 | [Eat_86>Catch2_86 | [Eat_99>Catch2_99 | [Eat_98>Catch2_98 | [Eat_14>Catch2_14 | [Eat_91>Catch2_91 | [Eat_79>Catch2_79 | [Eat_20>Catch2_20 | [Eat_35>Catch2_35 | [Eat_95>Catch2_95 | [Eat_84>Catch2_84 | [Eat_27>Catch2_27 | [Eat_4>Catch2_4 | [Eat_78>Catch2_78 | [Eat_40>Catch2_40 | [Eat_70>Catch2_70 | [Eat_24>Catch2_24 | [Eat_82>Catch2_82 | [Eat_29>Catch2_29 | [Eat_77>Catch2_77 | [Eat_5>Catch2_5 | [Eat_2>Catch2_2 | [Eat_69>Catch2_69 | [Eat_32>Catch2_32 | [Eat_53>Catch2_53 | [Eat_9>Catch2_9 | [Eat_28>Catch2_28 | [Eat_73>Catch2_73 | [Eat_1>Catch2_1 | [Eat_93>Catch2_93 | [Eat_13>Catch2_13 | [Eat_3>Catch2_3 | [Eat_26>Catch2_26 | [Eat_50>Catch2_50 | [Eat_19>Catch2_19 | [Eat_87>Catch2_87 | [Eat_81>Catch2_81 | [Eat_37>Catch2_37 | [Eat_46>Catch2_46 | [Eat_89>Catch2_89 | [Eat_97>Catch2_97 | [Eat_22>Catch2_22 | [Eat_23>Catch2_23 | [Eat_65>Catch2_65 | [Eat_92>Catch2_92 | [Eat_51>Catch2_51 | [Eat_59>Catch2_59 | [Eat_67>Catch2_67 | [Eat_16>Catch2_16 | [Eat_85>Catch2_85 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | Eat_76>Catch2_76] | Eat_71>Catch2_71] | Eat_74>Catch2_74] | Eat_55>Catch2_55] | Eat_31>Catch2_31] | Eat_7>Catch2_7] | Eat_39>Catch2_39] | Eat_21>Catch2_21] | Eat_11>Catch2_11] | Eat_47>Catch2_47] | Eat_80>Catch2_80] | Eat_48>Catch2_48] | Eat_45>Catch2_45] | Eat_66>Catch2_66] | Eat_49>Catch2_49] | Eat_72>Catch2_72] | Eat_61>Catch2_61] | Eat_90>Catch2_90] | Eat_83>Catch2_83] | Eat_96>Catch2_96] | Eat_56>Catch2_56] | Eat_54>Catch2_54] | Eat_57>Catch2_57] | Eat_12>Catch2_12] | Eat_63>Catch2_63] | Eat_36>Catch2_36] | Eat_68>Catch2_68] | Eat_100>Catch2_100] | Eat_33>Catch2_33] | Eat_8>Catch2_8] | Eat_41>Catch2_41] | Eat_30>Catch2_30] | Eat_58>Catch2_58] | Eat_15>Catch2_15] | Eat_75>Catch2_75] | Eat_6>Catch2_6] | Eat_52>Catch2_52] | Eat_42>Catch2_42] | Eat_60>Catch2_60] | Eat_34>Catch2_34] | Eat_88>Catch2_88] | Eat_17>Catch2_17]] & [true & [Eat_17>Catch2_17 & [Eat_88>Catch2_88 & [Eat_34>Catch2_34 & [Eat_60>Catch2_60 & [Eat_42>Catch2_42 & [Eat_52>Catch2_52 & [Eat_6>Catch2_6 & [Eat_75>Catch2_75 & [Eat_15>Catch2_15 & [Eat_58>Catch2_58 & [Eat_30>Catch2_30 & [Eat_41>Catch2_41 & [Eat_8>Catch2_8 & [Eat_33>Catch2_33 & [Eat_100>Catch2_100 & [Eat_68>Catch2_68 & [Eat_36>Catch2_36 & [Eat_63>Catch2_63 & [Eat_12>Catch2_12 & [Eat_57>Catch2_57 & [Eat_54>Catch2_54 & [Eat_56>Catch2_56 & [Eat_96>Catch2_96 & [Eat_83>Catch2_83 & [Eat_90>Catch2_90 & [Eat_61>Catch2_61 & [Eat_72>Catch2_72 & [Eat_49>Catch2_49 & [Eat_66>Catch2_66 & [Eat_45>Catch2_45 & [Eat_48>Catch2_48 & [Eat_80>Catch2_80 & [Eat_47>Catch2_47 & [Eat_11>Catch2_11 & [Eat_21>Catch2_21 & [Eat_39>Catch2_39 & [Eat_7>Catch2_7 & [Eat_31>Catch2_31 & [Eat_55>Catch2_55 & [Eat_74>Catch2_74 & [Eat_71>Catch2_71 & [Eat_76>Catch2_76 & [Eat_44>Catch2_44 & [Eat_18>Catch2_18 & [Eat_10>Catch2_10 & [Eat_25>Catch2_25 & [Eat_64>Catch2_64 & [Eat_94>Catch2_94 & [Eat_43>Catch2_43 & [Eat_62>Catch2_62 & [Eat_38>Catch2_38 & [Eat_86>Catch2_86 & [Eat_99>Catch2_99 & [Eat_98>Catch2_98 & [Eat_14>Catch2_14 & [Eat_91>Catch2_91 & [Eat_79>Catch2_79 & [Eat_20>Catch2_20 & [Eat_35>Catch2_35 & [Eat_95>Catch2_95 & [Eat_84>Catch2_84 & [Eat_27>Catch2_27 & [Eat_4>Catch2_4 & [Eat_78>Catch2_78 & [Eat_40>Catch2_40 & [Eat_70>Catch2_70 & [Eat_24>Catch2_24 & [Eat_82>Catch2_82 & [Eat_29>Catch2_29 & [Eat_77>Catch2_77 & [Eat_5>Catch2_5 & [Eat_2>Catch2_2 & [Eat_69>Catch2_69 & [Eat_32>Catch2_32 & [Eat_53>Catch2_53 & [Eat_9>Catch2_9 & [Eat_28>Catch2_28 & [Eat_73>Catch2_73 & [Eat_1>Catch2_1 & [Eat_93>Catch2_93 & [Eat_13>Catch2_13 & [Eat_3>Catch2_3 & [Eat_26>Catch2_26 & [Eat_50>Catch2_50 & [Eat_19>Catch2_19 & [Eat_87>Catch2_87 & [Eat_81>Catch2_81 & [Eat_37>Catch2_37 & [Eat_46>Catch2_46 & [Eat_89>Catch2_89 & [Eat_97>Catch2_97 & [Eat_22>Catch2_22 & [Eat_23>Catch2_23 & [Eat_65>Catch2_65 & [Eat_92>Catch2_92 & [Eat_51>Catch2_51 & [Eat_59>Catch2_59 & [Eat_67>Catch2_67 & [Eat_16>Catch2_16 & [Eat_85>Catch2_85 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [true & [Eat_17<=Catch2_17 & [Eat_88<=Catch2_88 & [Eat_34<=Catch2_34 & [Eat_60<=Catch2_60 & [Eat_42<=Catch2_42 & [Eat_52<=Catch2_52 & [Eat_6<=Catch2_6 & [Eat_75<=Catch2_75 & [Eat_15<=Catch2_15 & [Eat_58<=Catch2_58 & [Eat_30<=Catch2_30 & [Eat_41<=Catch2_41 & [Eat_8<=Catch2_8 & [Eat_33<=Catch2_33 & [Eat_100<=Catch2_100 & [Eat_68<=Catch2_68 & [Eat_36<=Catch2_36 & [Eat_63<=Catch2_63 & [Eat_12<=Catch2_12 & [Eat_57<=Catch2_57 & [Eat_54<=Catch2_54 & [Eat_56<=Catch2_56 & [Eat_96<=Catch2_96 & [Eat_83<=Catch2_83 & [Eat_90<=Catch2_90 & [Eat_61<=Catch2_61 & [Eat_72<=Catch2_72 & [Eat_49<=Catch2_49 & [Eat_66<=Catch2_66 & [Eat_45<=Catch2_45 & [Eat_48<=Catch2_48 & [Eat_80<=Catch2_80 & [Eat_47<=Catch2_47 & [Eat_11<=Catch2_11 & [Eat_21<=Catch2_21 & [Eat_39<=Catch2_39 & [Eat_7<=Catch2_7 & [Eat_31<=Catch2_31 & [Eat_55<=Catch2_55 & [Eat_74<=Catch2_74 & [Eat_71<=Catch2_71 & [Eat_76<=Catch2_76 & [Eat_44<=Catch2_44 & [Eat_18<=Catch2_18 & [Eat_10<=Catch2_10 & [Eat_25<=Catch2_25 & [Eat_64<=Catch2_64 & [Eat_94<=Catch2_94 & [Eat_43<=Catch2_43 & [Eat_62<=Catch2_62 & [Eat_38<=Catch2_38 & [Eat_86<=Catch2_86 & [Eat_99<=Catch2_99 & [Eat_98<=Catch2_98 & [Eat_14<=Catch2_14 & [Eat_91<=Catch2_91 & [Eat_79<=Catch2_79 & [Eat_20<=Catch2_20 & [Eat_35<=Catch2_35 & [Eat_95<=Catch2_95 & [Eat_84<=Catch2_84 & [Eat_27<=Catch2_27 & [Eat_4<=Catch2_4 & [Eat_78<=Catch2_78 & [Eat_40<=Catch2_40 & [Eat_70<=Catch2_70 & [Eat_24<=Catch2_24 & [Eat_82<=Catch2_82 & [Eat_29<=Catch2_29 & [Eat_77<=Catch2_77 & [Eat_5<=Catch2_5 & [Eat_2<=Catch2_2 & [Eat_69<=Catch2_69 & [Eat_32<=Catch2_32 & [Eat_53<=Catch2_53 & [Eat_9<=Catch2_9 & [Eat_28<=Catch2_28 & [Eat_73<=Catch2_73 & [Eat_1<=Catch2_1 & [Eat_93<=Catch2_93 & [Eat_13<=Catch2_13 & [Eat_3<=Catch2_3 & [Eat_26<=Catch2_26 & [Eat_50<=Catch2_50 & [Eat_19<=Catch2_19 & [Eat_87<=Catch2_87 & [Eat_81<=Catch2_81 & [Eat_37<=Catch2_37 & [Eat_46<=Catch2_46 & [Eat_89<=Catch2_89 & [Eat_97<=Catch2_97 & [Eat_22<=Catch2_22 & [Eat_23<=Catch2_23 & [Eat_65<=Catch2_65 & [Eat_92<=Catch2_92 & [Eat_51<=Catch2_51 & [Eat_59<=Catch2_59 & [Eat_67<=Catch2_67 & [Eat_16<=Catch2_16 & [Eat_85<=Catch2_85 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_13_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Eat_85>Catch2_85] & Eat_16>Catch2_16] & Eat_67>Catch2_67] & Eat_59>Catch2_59] & Eat_51>Catch2_51] & Eat_92>Catch2_92] & Eat_65>Catch2_65] & Eat_23>Catch2_23] & Eat_22>Catch2_22] & Eat_97>Catch2_97] & Eat_89>Catch2_89] & Eat_46>Catch2_46] & Eat_37>Catch2_37] & Eat_81>Catch2_81] & Eat_87>Catch2_87] & Eat_19>Catch2_19] & Eat_50>Catch2_50] & Eat_26>Catch2_26] & Eat_3>Catch2_3] & Eat_13>Catch2_13] & Eat_93>Catch2_93] & Eat_1>Catch2_1] & Eat_73>Catch2_73] & Eat_28>Catch2_28] & Eat_9>Catch2_9] & Eat_53>Catch2_53] & Eat_32>Catch2_32] & Eat_69>Catch2_69] & Eat_2>Catch2_2] & Eat_5>Catch2_5] & Eat_77>Catch2_77] & Eat_29>Catch2_29] & Eat_82>Catch2_82] & Eat_24>Catch2_24] & Eat_70>Catch2_70] & Eat_40>Catch2_40] & Eat_78>Catch2_78] & Eat_4>Catch2_4] & Eat_27>Catch2_27] & Eat_84>Catch2_84] & Eat_95>Catch2_95] & Eat_35>Catch2_35] & Eat_20>Catch2_20] & Eat_79>Catch2_79] & Eat_91>Catch2_91] & Eat_14>Catch2_14] & Eat_98>Catch2_98] & Eat_99>Catch2_99] & Eat_86>Catch2_86] & Eat_38>Catch2_38] & Eat_62>Catch2_62] & Eat_43>Catch2_43] & Eat_94>Catch2_94] & Eat_64>Catch2_64] & Eat_25>Catch2_25] & Eat_10>Catch2_10] & Eat_18>Catch2_18] & Eat_44>Catch2_44] & Eat_76>Catch2_76] & Eat_71>Catch2_71] & Eat_74>Catch2_74] & Eat_55>Catch2_55] & Eat_31>Catch2_31] & Eat_7>Catch2_7] & Eat_39>Catch2_39] & Eat_21>Catch2_21] & Eat_11>Catch2_11] & Eat_47>Catch2_47] & Eat_80>Catch2_80] & Eat_48>Catch2_48] & Eat_45>Catch2_45] & Eat_66>Catch2_66] & Eat_49>Catch2_49] & Eat_72>Catch2_72] & Eat_61>Catch2_61] & Eat_90>Catch2_90] & Eat_83>Catch2_83] & Eat_96>Catch2_96] & Eat_56>Catch2_56] & Eat_54>Catch2_54] & Eat_57>Catch2_57] & Eat_12>Catch2_12] & Eat_63>Catch2_63] & Eat_36>Catch2_36] & Eat_68>Catch2_68] & Eat_100>Catch2_100] & Eat_33>Catch2_33] & Eat_8>Catch2_8] & Eat_41>Catch2_41] & Eat_30>Catch2_30] & Eat_58>Catch2_58] & Eat_15>Catch2_15] & Eat_75>Catch2_75] & Eat_6>Catch2_6] & Eat_52>Catch2_52] & Eat_42>Catch2_42] & Eat_60>Catch2_60] & Eat_34>Catch2_34] & Eat_88>Catch2_88] & Eat_17>Catch2_17]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Eat_85>Catch2_85] | Eat_16>Catch2_16] | Eat_67>Catch2_67] | Eat_59>Catch2_59] | Eat_51>Catch2_51] | Eat_92>Catch2_92] | Eat_65>Catch2_65] | Eat_23>Catch2_23] | Eat_22>Catch2_22] | Eat_97>Catch2_97] | Eat_89>Catch2_89] | Eat_46>Catch2_46] | Eat_37>Catch2_37] | Eat_81>Catch2_81] | Eat_87>Catch2_87] | Eat_19>Catch2_19] | Eat_50>Catch2_50] | Eat_26>Catch2_26] | Eat_3>Catch2_3] | Eat_13>Catch2_13] | Eat_93>Catch2_93] | Eat_1>Catch2_1] | Eat_73>Catch2_73] | Eat_28>Catch2_28] | Eat_9>Catch2_9] | Eat_53>Catch2_53] | Eat_32>Catch2_32] | Eat_69>Catch2_69] | Eat_2>Catch2_2] | Eat_5>Catch2_5] | Eat_77>Catch2_77] | Eat_29>Catch2_29] | Eat_82>Catch2_82] | Eat_24>Catch2_24] | Eat_70>Catch2_70] | Eat_40>Catch2_40] | Eat_78>Catch2_78] | Eat_4>Catch2_4] | Eat_27>Catch2_27] | Eat_84>Catch2_84] | Eat_95>Catch2_95] | Eat_35>Catch2_35] | Eat_20>Catch2_20] | Eat_79>Catch2_79] | Eat_91>Catch2_91] | Eat_14>Catch2_14] | Eat_98>Catch2_98] | Eat_99>Catch2_99] | Eat_86>Catch2_86] | Eat_38>Catch2_38] | Eat_62>Catch2_62] | Eat_43>Catch2_43] | Eat_94>Catch2_94] | Eat_64>Catch2_64] | Eat_25>Catch2_25] | Eat_10>Catch2_10] | Eat_18>Catch2_18] | Eat_44>Catch2_44] | Eat_76>Catch2_76] | Eat_71>Catch2_71] | Eat_74>Catch2_74] | Eat_55>Catch2_55] | Eat_31>Catch2_31] | Eat_7>Catch2_7] | Eat_39>Catch2_39] | Eat_21>Catch2_21] | Eat_11>Catch2_11] | Eat_47>Catch2_47] | Eat_80>Catch2_80] | Eat_48>Catch2_48] | Eat_45>Catch2_45] | Eat_66>Catch2_66] | Eat_49>Catch2_49] | Eat_72>Catch2_72] | Eat_61>Catch2_61] | Eat_90>Catch2_90] | Eat_83>Catch2_83] | Eat_96>Catch2_96] | Eat_56>Catch2_56] | Eat_54>Catch2_54] | Eat_57>Catch2_57] | Eat_12>Catch2_12] | Eat_63>Catch2_63] | Eat_36>Catch2_36] | Eat_68>Catch2_68] | Eat_100>Catch2_100] | Eat_33>Catch2_33] | Eat_8>Catch2_8] | Eat_41>Catch2_41] | Eat_30>Catch2_30] | Eat_58>Catch2_58] | Eat_15>Catch2_15] | Eat_75>Catch2_75] | Eat_6>Catch2_6] | Eat_52>Catch2_52] | Eat_42>Catch2_42] | Eat_60>Catch2_60] | Eat_34>Catch2_34] | Eat_88>Catch2_88] | Eat_17>Catch2_17] | false]] & [true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Eat_85<=Catch2_85] & Eat_16<=Catch2_16] & Eat_67<=Catch2_67] & Eat_59<=Catch2_59] & Eat_51<=Catch2_51] & Eat_92<=Catch2_92] & Eat_65<=Catch2_65] & Eat_23<=Catch2_23] & Eat_22<=Catch2_22] & Eat_97<=Catch2_97] & Eat_89<=Catch2_89] & Eat_46<=Catch2_46] & Eat_37<=Catch2_37] & Eat_81<=Catch2_81] & Eat_87<=Catch2_87] & Eat_19<=Catch2_19] & Eat_50<=Catch2_50] & Eat_26<=Catch2_26] & Eat_3<=Catch2_3] & Eat_13<=Catch2_13] & Eat_93<=Catch2_93] & Eat_1<=Catch2_1] & Eat_73<=Catch2_73] & Eat_28<=Catch2_28] & Eat_9<=Catch2_9] & Eat_53<=Catch2_53] & Eat_32<=Catch2_32] & Eat_69<=Catch2_69] & Eat_2<=Catch2_2] & Eat_5<=Catch2_5] & Eat_77<=Catch2_77] & Eat_29<=Catch2_29] & Eat_82<=Catch2_82] & Eat_24<=Catch2_24] & Eat_70<=Catch2_70] & Eat_40<=Catch2_40] & Eat_78<=Catch2_78] & Eat_4<=Catch2_4] & Eat_27<=Catch2_27] & Eat_84<=Catch2_84] & Eat_95<=Catch2_95] & Eat_35<=Catch2_35] & Eat_20<=Catch2_20] & Eat_79<=Catch2_79] & Eat_91<=Catch2_91] & Eat_14<=Catch2_14] & Eat_98<=Catch2_98] & Eat_99<=Catch2_99] & Eat_86<=Catch2_86] & Eat_38<=Catch2_38] & Eat_62<=Catch2_62] & Eat_43<=Catch2_43] & Eat_94<=Catch2_94] & Eat_64<=Catch2_64] & Eat_25<=Catch2_25] & Eat_10<=Catch2_10] & Eat_18<=Catch2_18] & Eat_44<=Catch2_44] & Eat_76<=Catch2_76] & Eat_71<=Catch2_71] & Eat_74<=Catch2_74] & Eat_55<=Catch2_55] & Eat_31<=Catch2_31] & Eat_7<=Catch2_7] & Eat_39<=Catch2_39] & Eat_21<=Catch2_21] & Eat_11<=Catch2_11] & Eat_47<=Catch2_47] & Eat_80<=Catch2_80] & Eat_48<=Catch2_48] & Eat_45<=Catch2_45] & Eat_66<=Catch2_66] & Eat_49<=Catch2_49] & Eat_72<=Catch2_72] & Eat_61<=Catch2_61] & Eat_90<=Catch2_90] & Eat_83<=Catch2_83] & Eat_96<=Catch2_96] & Eat_56<=Catch2_56] & Eat_54<=Catch2_54] & Eat_57<=Catch2_57] & Eat_12<=Catch2_12] & Eat_63<=Catch2_63] & Eat_36<=Catch2_36] & Eat_68<=Catch2_68] & Eat_100<=Catch2_100] & Eat_33<=Catch2_33] & Eat_8<=Catch2_8] & Eat_41<=Catch2_41] & Eat_30<=Catch2_30] & Eat_58<=Catch2_58] & Eat_15<=Catch2_15] & Eat_75<=Catch2_75] & Eat_6<=Catch2_6] & Eat_52<=Catch2_52] & Eat_42<=Catch2_42] & Eat_60<=Catch2_60] & Eat_34<=Catch2_34] & Eat_88<=Catch2_88] & Eat_17<=Catch2_17]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Eat_85<=Catch2_85] & Eat_16<=Catch2_16] & Eat_67<=Catch2_67] & Eat_59<=Catch2_59] & Eat_51<=Catch2_51] & Eat_92<=Catch2_92] & Eat_65<=Catch2_65] & Eat_23<=Catch2_23] & Eat_22<=Catch2_22] & Eat_97<=Catch2_97] & Eat_89<=Catch2_89] & Eat_46<=Catch2_46] & Eat_37<=Catch2_37] & Eat_81<=Catch2_81] & Eat_87<=Catch2_87] & Eat_19<=Catch2_19] & Eat_50<=Catch2_50] & Eat_26<=Catch2_26] & Eat_3<=Catch2_3] & Eat_13<=Catch2_13] & Eat_93<=Catch2_93] & Eat_1<=Catch2_1] & Eat_73<=Catch2_73] & Eat_28<=Catch2_28] & Eat_9<=Catch2_9] & Eat_53<=Catch2_53] & Eat_32<=Catch2_32] & Eat_69<=Catch2_69] & Eat_2<=Catch2_2] & Eat_5<=Catch2_5] & Eat_77<=Catch2_77] & Eat_29<=Catch2_29] & Eat_82<=Catch2_82] & Eat_24<=Catch2_24] & Eat_70<=Catch2_70] & Eat_40<=Catch2_40] & Eat_78<=Catch2_78] & Eat_4<=Catch2_4] & Eat_27<=Catch2_27] & Eat_84<=Catch2_84] & Eat_95<=Catch2_95] & Eat_35<=Catch2_35] & Eat_20<=Catch2_20] & Eat_79<=Catch2_79] & Eat_91<=Catch2_91] & Eat_14<=Catch2_14] & Eat_98<=Catch2_98] & Eat_99<=Catch2_99] & Eat_86<=Catch2_86] & Eat_38<=Catch2_38] & Eat_62<=Catch2_62] & Eat_43<=Catch2_43] & Eat_94<=Catch2_94] & Eat_64<=Catch2_64] & Eat_25<=Catch2_25] & Eat_10<=Catch2_10] & Eat_18<=Catch2_18] & Eat_44<=Catch2_44] & Eat_76<=Catch2_76] & Eat_71<=Catch2_71] & Eat_74<=Catch2_74] & Eat_55<=Catch2_55] & Eat_31<=Catch2_31] & Eat_7<=Catch2_7] & Eat_39<=Catch2_39] & Eat_21<=Catch2_21] & Eat_11<=Catch2_11] & Eat_47<=Catch2_47] & Eat_80<=Catch2_80] & Eat_48<=Catch2_48] & Eat_45<=Catch2_45] & Eat_66<=Catch2_66] & Eat_49<=Catch2_49] & Eat_72<=Catch2_72] & Eat_61<=Catch2_61] & Eat_90<=Catch2_90] & Eat_83<=Catch2_83] & Eat_96<=Catch2_96] & Eat_56<=Catch2_56] & Eat_54<=Catch2_54] & Eat_57<=Catch2_57] & Eat_12<=Catch2_12] & Eat_63<=Catch2_63] & Eat_36<=Catch2_36] & Eat_68<=Catch2_68] & Eat_100<=Catch2_100] & Eat_33<=Catch2_33] & Eat_8<=Catch2_8] & Eat_41<=Catch2_41] & Eat_30<=Catch2_30] & Eat_58<=Catch2_58] & Eat_15<=Catch2_15] & Eat_75<=Catch2_75] & Eat_6<=Catch2_6] & Eat_52<=Catch2_52] & Eat_42<=Catch2_42] & Eat_60<=Catch2_60] & Eat_34<=Catch2_34] & Eat_88<=Catch2_88] & Eat_17<=Catch2_17] & true] & [[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Eat_85>Catch2_85] | Eat_16>Catch2_16] | Eat_67>Catch2_67] | Eat_59>Catch2_59] | Eat_51>Catch2_51] | Eat_92>Catch2_92] | Eat_65>Catch2_65] | Eat_23>Catch2_23] | Eat_22>Catch2_22] | Eat_97>Catch2_97] | Eat_89>Catch2_89] | Eat_46>Catch2_46] | Eat_37>Catch2_37] | Eat_81>Catch2_81] | Eat_87>Catch2_87] | Eat_19>Catch2_19] | Eat_50>Catch2_50] | Eat_26>Catch2_26] | Eat_3>Catch2_3] | Eat_13>Catch2_13] | Eat_93>Catch2_93] | Eat_1>Catch2_1] | Eat_73>Catch2_73] | Eat_28>Catch2_28] | Eat_9>Catch2_9] | Eat_53>Catch2_53] | Eat_32>Catch2_32] | Eat_69>Catch2_69] | Eat_2>Catch2_2] | Eat_5>Catch2_5] | Eat_77>Catch2_77] | Eat_29>Catch2_29] | Eat_82>Catch2_82] | Eat_24>Catch2_24] | Eat_70>Catch2_70] | Eat_40>Catch2_40] | Eat_78>Catch2_78] | Eat_4>Catch2_4] | Eat_27>Catch2_27] | Eat_84>Catch2_84] | Eat_95>Catch2_95] | Eat_35>Catch2_35] | Eat_20>Catch2_20] | Eat_79>Catch2_79] | Eat_91>Catch2_91] | Eat_14>Catch2_14] | Eat_98>Catch2_98] | Eat_99>Catch2_99] | Eat_86>Catch2_86] | Eat_38>Catch2_38] | Eat_62>Catch2_62] | Eat_43>Catch2_43] | Eat_94>Catch2_94] | Eat_64>Catch2_64] | Eat_25>Catch2_25] | Eat_10>Catch2_10] | Eat_18>Catch2_18] | Eat_44>Catch2_44] | Eat_76>Catch2_76] | Eat_71>Catch2_71] | Eat_74>Catch2_74] | Eat_55>Catch2_55] | Eat_31>Catch2_31] | Eat_7>Catch2_7] | Eat_39>Catch2_39] | Eat_21>Catch2_21] | Eat_11>Catch2_11] | Eat_47>Catch2_47] | Eat_80>Catch2_80] | Eat_48>Catch2_48] | Eat_45>Catch2_45] | Eat_66>Catch2_66] | Eat_49>Catch2_49] | Eat_72>Catch2_72] | Eat_61>Catch2_61] | Eat_90>Catch2_90] | Eat_83>Catch2_83] | Eat_96>Catch2_96] | Eat_56>Catch2_56] | Eat_54>Catch2_54] | Eat_57>Catch2_57] | Eat_12>Catch2_12] | Eat_63>Catch2_63] | Eat_36>Catch2_36] | Eat_68>Catch2_68] | Eat_100>Catch2_100] | Eat_33>Catch2_33] | Eat_8>Catch2_8] | Eat_41>Catch2_41] | Eat_30>Catch2_30] | Eat_58>Catch2_58] | Eat_15>Catch2_15] | Eat_75>Catch2_75] | Eat_6>Catch2_6] | Eat_52>Catch2_52] | Eat_42>Catch2_42] | Eat_60>Catch2_60] | Eat_34>Catch2_34] | Eat_88>Catch2_88] | Eat_17>Catch2_17]] & [[[[[[[[[[[[[[[[[[[[[[[[[Eat_83>Catch2_83 & [Eat_90>Catch2_90 & [Eat_61>Catch2_61 & [Eat_72>Catch2_72 & [Eat_49>Catch2_49 & [Eat_66>Catch2_66 & [Eat_45>Catch2_45 & [Eat_48>Catch2_48 & [Eat_80>Catch2_80 & [Eat_47>Catch2_47 & [Eat_11>Catch2_11 & [Eat_21>Catch2_21 & [Eat_39>Catch2_39 & [Eat_7>Catch2_7 & [Eat_31>Catch2_31 & [Eat_55>Catch2_55 & [Eat_74>Catch2_74 & [Eat_71>Catch2_71 & [Eat_76>Catch2_76 & [Eat_44>Catch2_44 & [Eat_18>Catch2_18 & [Eat_10>Catch2_10 & [Eat_25>Catch2_25 & [Eat_64>Catch2_64 & [Eat_94>Catch2_94 & [Eat_43>Catch2_43 & [Eat_62>Catch2_62 & [Eat_38>Catch2_38 & [Eat_86>Catch2_86 & [Eat_99>Catch2_99 & [Eat_98>Catch2_98 & [Eat_14>Catch2_14 & [Eat_91>Catch2_91 & [Eat_79>Catch2_79 & [Eat_20>Catch2_20 & [Eat_35>Catch2_35 & [Eat_95>Catch2_95 & [Eat_84>Catch2_84 & [Eat_27>Catch2_27 & [Eat_4>Catch2_4 & [Eat_78>Catch2_78 & [Eat_40>Catch2_40 & [Eat_70>Catch2_70 & [Eat_24>Catch2_24 & [Eat_82>Catch2_82 & [Eat_29>Catch2_29 & [Eat_77>Catch2_77 & [Eat_5>Catch2_5 & [Eat_2>Catch2_2 & [Eat_69>Catch2_69 & [Eat_32>Catch2_32 & [Eat_53>Catch2_53 & [Eat_9>Catch2_9 & [Eat_28>Catch2_28 & [Eat_73>Catch2_73 & [Eat_1>Catch2_1 & [Eat_93>Catch2_93 & [Eat_13>Catch2_13 & [Eat_3>Catch2_3 & [Eat_26>Catch2_26 & [Eat_50>Catch2_50 & [Eat_19>Catch2_19 & [Eat_87>Catch2_87 & [Eat_81>Catch2_81 & [Eat_37>Catch2_37 & [Eat_46>Catch2_46 & [Eat_89>Catch2_89 & [Eat_97>Catch2_97 & [Eat_22>Catch2_22 & [Eat_23>Catch2_23 & [Eat_65>Catch2_65 & [Eat_92>Catch2_92 & [Eat_51>Catch2_51 & [Eat_59>Catch2_59 & [Eat_67>Catch2_67 & [Eat_16>Catch2_16 & [Eat_85>Catch2_85 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Eat_96>Catch2_96] & Eat_56>Catch2_56] & Eat_54>Catch2_54] & Eat_57>Catch2_57] & Eat_12>Catch2_12] & Eat_63>Catch2_63] & Eat_36>Catch2_36] & Eat_68>Catch2_68] & Eat_100>Catch2_100] & Eat_33>Catch2_33] & Eat_8>Catch2_8] & Eat_41>Catch2_41] & Eat_30>Catch2_30] & Eat_58>Catch2_58] & Eat_15>Catch2_15] & Eat_75>Catch2_75] & Eat_6>Catch2_6] & Eat_52>Catch2_52] & Eat_42>Catch2_42] & Eat_60>Catch2_60] & Eat_34>Catch2_34] & Eat_88>Catch2_88] & Eat_17>Catch2_17] & true]]]]]]

-> the formula is FALSE

FORMULA p_14_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m9sec

STOP 1369696069

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

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

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

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