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

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

START 1369712424

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=CTLPlaceComparison.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: EG [[[[Catch2_30=Catch1_30 & [[Catch2_78=Catch1_78 & [[[[[[[[[[Catch2_33=Catch1_33 & [[[[[[[Catch2_19=Catch1_19 & [Catch2_88=Catch1_88 & [[[Catch2_8=Catch1_8 & [[Catch2_31=Catch1_31 & [[[[Catch2_62=Catch1_62 & [Catch2_52=Catch1_52 & [Catch2_87=Catch1_87 & [[[[Catch2_29=Catch1_29 & [[Catch2_57=Catch1_57 & [[[[[Catch2_84=Catch1_84 & [Catch2_68=Catch1_68 & [Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [[Catch2_54=Catch1_54 & [[[[[[[[[Catch2_23=Catch1_23 & [[Catch2_53=Catch1_53 & [Catch2_34=Catch1_34 & [[[Catch2_39=Catch1_39 & [[Catch2_22=Catch1_22 & [[[[Catch2_45=Catch1_45 & [[[[[[[[[[[Catch2_42=Catch1_42 & [Catch2_94=Catch1_94 & [[[Catch2_91=Catch1_91 & [[Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [[Catch2_9=Catch1_9 & [[[[[Catch2_28=Catch1_28 & [[[[[true & Catch2_92=Catch1_92] & Catch2_97=Catch1_97] & Catch2_67=Catch1_67] & Catch2_5=Catch1_5] & Catch2_49=Catch1_49]] & Catch2_66=Catch1_66] & Catch2_79=Catch1_79] & Catch2_77=Catch1_77] & Catch2_73=Catch1_73]] & Catch2_35=Catch1_35]]] & Catch2_13=Catch1_13]] & Catch2_37=Catch1_37] & Catch2_86=Catch1_86]]] & Catch2_85=Catch1_85] & Catch2_100=Catch1_100] & Catch2_89=Catch1_89] & Catch2_26=Catch1_26] & Catch2_93=Catch1_93] & Catch2_17=Catch1_17] & Catch2_61=Catch1_61] & Catch2_56=Catch1_56] & Catch2_60=Catch1_60] & Catch2_64=Catch1_64]] & Catch2_90=Catch1_90] & Catch2_7=Catch1_7] & Catch2_75=Catch1_75]] & Catch2_27=Catch1_27]] & Catch2_59=Catch1_59] & Catch2_24=Catch1_24]]] & Catch2_95=Catch1_95]] & Catch2_38=Catch1_38] & Catch2_70=Catch1_70] & Catch2_55=Catch1_55] & Catch2_36=Catch1_36] & Catch2_1=Catch1_1] & Catch2_47=Catch1_47] & Catch2_41=Catch1_41] & Catch2_98=Catch1_98]] & Catch2_63=Catch1_63]]]]] & Catch2_6=Catch1_6] & Catch2_10=Catch1_10] & Catch2_76=Catch1_76] & Catch2_65=Catch1_65]] & Catch2_51=Catch1_51]] & Catch2_25=Catch1_25] & Catch2_50=Catch1_50] & Catch2_43=Catch1_43]]]] & Catch2_11=Catch1_11] & Catch2_4=Catch1_4] & Catch2_20=Catch1_20]] & Catch2_16=Catch1_16]] & Catch2_2=Catch1_2] & Catch2_83=Catch1_83]]] & Catch2_32=Catch1_32] & Catch2_21=Catch1_21] & Catch2_14=Catch1_14] & Catch2_82=Catch1_82] & Catch2_46=Catch1_46] & Catch2_80=Catch1_80]] & Catch2_48=Catch1_48] & Catch2_3=Catch1_3] & Catch2_15=Catch1_15] & Catch2_81=Catch1_81] & Catch2_99=Catch1_99] & Catch2_12=Catch1_12] & Catch2_69=Catch1_69] & Catch2_74=Catch1_74] & Catch2_44=Catch1_44]] & Catch2_18=Catch1_18]] & Catch2_71=Catch1_71] & [[[Catch2_62=Fork_62 & [[[Catch2_20=Fork_20 & [Catch2_24=Fork_24 & [[[[[Catch2_65=Fork_65 & [[[Catch2_18=Fork_18 & [[[[[Catch2_67=Fork_67 & [[[[Catch2_38=Fork_38 & [[[[Catch2_34=Fork_34 & [[Catch2_11=Fork_11 & [[[[[Catch2_45=Fork_45 & [Catch2_44=Fork_44 & [Catch2_74=Fork_74 & [[[Catch2_98=Fork_98 & [[Catch2_58=Fork_58 & [[[[[Catch2_53=Fork_53 & [[Catch2_57=Fork_57 & [[[[[Catch2_56=Fork_56 & [[[Catch2_10=Fork_10 & [Catch2_66=Fork_66 & [Catch2_25=Fork_25 & [Catch2_32=Fork_32 & [Catch2_17=Fork_17 & [[[[Catch2_16=Fork_16 & [[Catch2_28=Fork_28 & [Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [[Catch2_89=Fork_89 & [[[Catch2_70=Fork_70 & [[[[[Catch2_41=Fork_41 & [[[[Catch2_37=Fork_37 & [Catch2_36=Fork_36 & [Catch2_43=Fork_43 & [[[[Catch2_84=Fork_84 & [Catch2_68=Fork_68 & [Catch2_99=Fork_99 & [Catch2_33=Fork_33 & [[[Catch2_42=Fork_42 & [[Catch2_54=Fork_54 & [[[Catch2_50=Fork_50 & true] & Catch2_40=Fork_40] & Catch2_46=Fork_46]] & Catch2_86=Fork_86]] & Catch2_6=Fork_6] & Catch2_27=Fork_27]]]]] & Catch2_4=Fork_4] & Catch2_85=Fork_85] & Catch2_81=Fork_81]]]] & 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_8=Fork_8] & Catch2_22=Fork_22]] & Catch2_96=Fork_96]]]] & Catch2_5=Fork_5]] & Catch2_12=Fork_12] & Catch2_7=Fork_7] & Catch2_87=Fork_87]]]]]] & Catch2_52=Fork_52] & Catch2_61=Fork_61]] & Catch2_55=Fork_55] & Catch2_90=Fork_90] & Catch2_94=Fork_94] & Catch2_78=Fork_78]] & Catch2_39=Fork_39]] & Catch2_3=Fork_3] & Catch2_91=Fork_91] & Catch2_79=Fork_79] & Catch2_1=Fork_1]] & Catch2_95=Fork_95]] & Catch2_23=Fork_23] & Catch2_14=Fork_14]]]] & Catch2_92=Fork_92] & Catch2_29=Fork_29] & Catch2_77=Fork_77] & Catch2_69=Fork_69]] & Catch2_13=Fork_13]] & Catch2_31=Fork_31] & Catch2_15=Fork_15] & Catch2_75=Fork_75]] & Catch2_49=Fork_49] & Catch2_60=Fork_60] & Catch2_26=Fork_26]] & Catch2_82=Fork_82] & Catch2_76=Fork_76] & Catch2_9=Fork_9] & Catch2_71=Fork_71]] & Catch2_19=Fork_19] & Catch2_88=Fork_88]] & Catch2_51=Fork_51] & Catch2_83=Fork_83] & Catch2_72=Fork_72] & Catch2_21=Fork_21]]] & Catch2_80=Fork_80] & Catch2_48=Fork_48]] & Catch2_47=Fork_47] & Catch2_73=Fork_73]]]
normalized: EG [[[Catch2_71=Catch1_71 & [Catch2_30=Catch1_30 & [Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [Catch2_44=Catch1_44 & [Catch2_74=Catch1_74 & [Catch2_69=Catch1_69 & [Catch2_12=Catch1_12 & [Catch2_99=Catch1_99 & [Catch2_81=Catch1_81 & [Catch2_15=Catch1_15 & [Catch2_3=Catch1_3 & [Catch2_48=Catch1_48 & [Catch2_33=Catch1_33 & [Catch2_80=Catch1_80 & [Catch2_46=Catch1_46 & [Catch2_82=Catch1_82 & [Catch2_14=Catch1_14 & [Catch2_21=Catch1_21 & [Catch2_32=Catch1_32 & [Catch2_19=Catch1_19 & [Catch2_88=Catch1_88 & [Catch2_83=Catch1_83 & [Catch2_2=Catch1_2 & [Catch2_8=Catch1_8 & [Catch2_16=Catch1_16 & [Catch2_31=Catch1_31 & [Catch2_20=Catch1_20 & [Catch2_4=Catch1_4 & [Catch2_11=Catch1_11 & [Catch2_62=Catch1_62 & [Catch2_52=Catch1_52 & [Catch2_87=Catch1_87 & [Catch2_43=Catch1_43 & [Catch2_50=Catch1_50 & [Catch2_25=Catch1_25 & [Catch2_29=Catch1_29 & [Catch2_51=Catch1_51 & [Catch2_57=Catch1_57 & [Catch2_65=Catch1_65 & [Catch2_76=Catch1_76 & [Catch2_10=Catch1_10 & [Catch2_6=Catch1_6 & [Catch2_84=Catch1_84 & [Catch2_68=Catch1_68 & [Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [Catch2_63=Catch1_63 & [Catch2_54=Catch1_54 & [Catch2_98=Catch1_98 & [Catch2_41=Catch1_41 & [Catch2_47=Catch1_47 & [Catch2_1=Catch1_1 & [Catch2_36=Catch1_36 & [Catch2_55=Catch1_55 & [Catch2_70=Catch1_70 & [Catch2_38=Catch1_38 & [Catch2_23=Catch1_23 & [Catch2_95=Catch1_95 & [Catch2_53=Catch1_53 & [Catch2_34=Catch1_34 & [Catch2_24=Catch1_24 & [Catch2_59=Catch1_59 & [Catch2_39=Catch1_39 & [Catch2_27=Catch1_27 & [Catch2_22=Catch1_22 & [Catch2_75=Catch1_75 & [Catch2_7=Catch1_7 & [Catch2_90=Catch1_90 & [Catch2_45=Catch1_45 & [Catch2_64=Catch1_64 & [Catch2_60=Catch1_60 & [Catch2_56=Catch1_56 & [Catch2_61=Catch1_61 & [Catch2_17=Catch1_17 & [Catch2_93=Catch1_93 & [Catch2_26=Catch1_26 & [Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [Catch2_85=Catch1_85 & [Catch2_42=Catch1_42 & [Catch2_94=Catch1_94 & [Catch2_86=Catch1_86 & [Catch2_37=Catch1_37 & [Catch2_91=Catch1_91 & [Catch2_13=Catch1_13 & [Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [Catch2_35=Catch1_35 & [Catch2_9=Catch1_9 & [Catch2_73=Catch1_73 & [Catch2_77=Catch1_77 & [Catch2_79=Catch1_79 & [Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [Catch2_49=Catch1_49 & [Catch2_5=Catch1_5 & [Catch2_67=Catch1_67 & [Catch2_97=Catch1_97 & [Catch2_92=Catch1_92 & 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]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1846_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch2_73=Fork_73 & [Catch2_47=Fork_47 & [Catch2_62=Fork_62 & [Catch2_48=Fork_48 & [[[[[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_82=Fork_82 & [Catch2_67=Fork_67 & [Catch2_26=Fork_26 & [Catch2_60=Fork_60 & [Catch2_49=Fork_49 & [Catch2_38=Fork_38 & [[[[[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_23=Fork_23 & [Catch2_98=Fork_98 & [Catch2_95=Fork_95 & [Catch2_58=Fork_58 & [Catch2_1=Fork_1 & [Catch2_79=Fork_79 & [[[[[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_32=Fork_32 & [Catch2_17=Fork_17 & [[[[[[[Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [Catch2_96=Fork_96 & [[[[Catch2_70=Fork_70 & [Catch2_2=Fork_2 & [Catch2_93=Fork_93 & [Catch2_59=Fork_59 & [[[[Catch2_63=Fork_63 & [[[[[[Catch2_85=Fork_85 & [[[[Catch2_99=Fork_99 & [[[Catch2_6=Fork_6 & [[[[[[Catch2_50=Fork_50 & true] & Catch2_40=Fork_40] & Catch2_46=Fork_46] & Catch2_54=Fork_54] & Catch2_86=Fork_86] & Catch2_42=Fork_42]] & Catch2_27=Fork_27] & Catch2_33=Fork_33]] & Catch2_68=Fork_68] & Catch2_84=Fork_84] & 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_35=Fork_35]]]]] & Catch2_8=Fork_8] & Catch2_22=Fork_22] & Catch2_89=Fork_89]]]] & 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_25=Fork_25] & Catch2_66=Fork_66] & Catch2_10=Fork_10] & Catch2_52=Fork_52] & Catch2_61=Fork_61]]]]]]] & Catch2_39=Fork_39] & Catch2_53=Fork_53] & Catch2_3=Fork_3] & Catch2_91=Fork_91]]]]]]] & Catch2_14=Fork_14] & Catch2_74=Fork_74] & Catch2_44=Fork_44] & Catch2_45=Fork_45]]]]]]] & Catch2_34=Fork_34] & Catch2_31=Fork_31] & Catch2_15=Fork_15] & Catch2_75=Fork_75]]]]]]] & Catch2_76=Fork_76] & Catch2_9=Fork_9] & Catch2_71=Fork_71] & Catch2_18=Fork_18]]]]]]] & Catch2_21=Fork_21] & Catch2_24=Fork_24] & Catch2_20=Fork_20] & Catch2_80=Fork_80]]]]] | [Catch2_71=Catch1_71 & [Catch2_30=Catch1_30 & [Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [Catch2_44=Catch1_44 & [Catch2_74=Catch1_74 & [Catch2_69=Catch1_69 & [Catch2_12=Catch1_12 & [Catch2_99=Catch1_99 & [Catch2_81=Catch1_81 & [Catch2_15=Catch1_15 & [Catch2_3=Catch1_3 & [Catch2_48=Catch1_48 & [[[[[[Catch2_21=Catch1_21 & [[[[[Catch2_2=Catch1_2 & [Catch2_8=Catch1_8 & [Catch2_16=Catch1_16 & [Catch2_31=Catch1_31 & [Catch2_20=Catch1_20 & [Catch2_4=Catch1_4 & [Catch2_11=Catch1_11 & [Catch2_62=Catch1_62 & [[Catch2_87=Catch1_87 & [Catch2_43=Catch1_43 & [[[[[[[[[[Catch2_84=Catch1_84 & [[Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [[[[[[Catch2_1=Catch1_1 & [[[Catch2_70=Catch1_70 & [Catch2_38=Catch1_38 & [[Catch2_95=Catch1_95 & [[Catch2_34=Catch1_34 & [[Catch2_59=Catch1_59 & [Catch2_39=Catch1_39 & [Catch2_27=Catch1_27 & [Catch2_22=Catch1_22 & [Catch2_75=Catch1_75 & [Catch2_7=Catch1_7 & [Catch2_90=Catch1_90 & [[Catch2_64=Catch1_64 & [[Catch2_56=Catch1_56 & [Catch2_61=Catch1_61 & [Catch2_17=Catch1_17 & [Catch2_93=Catch1_93 & [Catch2_26=Catch1_26 & [Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [[Catch2_42=Catch1_42 & [[Catch2_86=Catch1_86 & [Catch2_37=Catch1_37 & [Catch2_91=Catch1_91 & [Catch2_13=Catch1_13 & [Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [Catch2_35=Catch1_35 & [[Catch2_73=Catch1_73 & [[Catch2_79=Catch1_79 & [Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [Catch2_49=Catch1_49 & [Catch2_5=Catch1_5 & [Catch2_67=Catch1_67 & [Catch2_97=Catch1_97 & [true & Catch2_92=Catch1_92]]]]]]]] & Catch2_77=Catch1_77]] & Catch2_9=Catch1_9]]]]]]]] & Catch2_94=Catch1_94]] & Catch2_85=Catch1_85]]]]]]]] & Catch2_60=Catch1_60]] & Catch2_45=Catch1_45]]]]]]]] & Catch2_24=Catch1_24]] & Catch2_53=Catch1_53]] & Catch2_23=Catch1_23]]] & Catch2_55=Catch1_55] & Catch2_36=Catch1_36]] & Catch2_47=Catch1_47] & Catch2_41=Catch1_41] & Catch2_98=Catch1_98] & Catch2_54=Catch1_54] & Catch2_63=Catch1_63]]] & Catch2_68=Catch1_68]] & Catch2_6=Catch1_6] & Catch2_10=Catch1_10] & Catch2_76=Catch1_76] & Catch2_65=Catch1_65] & Catch2_57=Catch1_57] & Catch2_51=Catch1_51] & Catch2_29=Catch1_29] & Catch2_25=Catch1_25] & Catch2_50=Catch1_50]]] & Catch2_52=Catch1_52]]]]]]]]] & Catch2_83=Catch1_83] & Catch2_88=Catch1_88] & Catch2_19=Catch1_19] & Catch2_32=Catch1_32]] & Catch2_14=Catch1_14] & Catch2_82=Catch1_82] & Catch2_46=Catch1_46] & Catch2_80=Catch1_80] & Catch2_33=Catch1_33]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[Catch2_71=Catch1_71 & [Catch2_30=Catch1_30 & [Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [Catch2_44=Catch1_44 & [Catch2_74=Catch1_74 & [Catch2_69=Catch1_69 & [Catch2_12=Catch1_12 & [Catch2_99=Catch1_99 & [Catch2_81=Catch1_81 & [Catch2_15=Catch1_15 & [Catch2_3=Catch1_3 & [Catch2_48=Catch1_48 & [Catch2_33=Catch1_33 & [Catch2_80=Catch1_80 & [Catch2_46=Catch1_46 & [Catch2_82=Catch1_82 & [Catch2_14=Catch1_14 & [Catch2_21=Catch1_21 & [Catch2_32=Catch1_32 & [Catch2_19=Catch1_19 & [Catch2_88=Catch1_88 & [Catch2_83=Catch1_83 & [Catch2_2=Catch1_2 & [Catch2_8=Catch1_8 & [Catch2_16=Catch1_16 & [Catch2_31=Catch1_31 & [Catch2_20=Catch1_20 & [Catch2_4=Catch1_4 & [Catch2_11=Catch1_11 & [Catch2_62=Catch1_62 & [Catch2_52=Catch1_52 & [Catch2_87=Catch1_87 & [Catch2_43=Catch1_43 & [Catch2_50=Catch1_50 & [Catch2_25=Catch1_25 & [Catch2_29=Catch1_29 & [Catch2_51=Catch1_51 & [Catch2_57=Catch1_57 & [Catch2_65=Catch1_65 & [Catch2_76=Catch1_76 & [Catch2_10=Catch1_10 & [Catch2_6=Catch1_6 & [Catch2_84=Catch1_84 & [Catch2_68=Catch1_68 & [Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [Catch2_63=Catch1_63 & [Catch2_54=Catch1_54 & [Catch2_98=Catch1_98 & [Catch2_41=Catch1_41 & [Catch2_47=Catch1_47 & [Catch2_1=Catch1_1 & [Catch2_36=Catch1_36 & [Catch2_55=Catch1_55 & [Catch2_70=Catch1_70 & [Catch2_38=Catch1_38 & [Catch2_23=Catch1_23 & [Catch2_95=Catch1_95 & [Catch2_53=Catch1_53 & [Catch2_34=Catch1_34 & [Catch2_24=Catch1_24 & [Catch2_59=Catch1_59 & [Catch2_39=Catch1_39 & [Catch2_27=Catch1_27 & [Catch2_22=Catch1_22 & [Catch2_75=Catch1_75 & [Catch2_7=Catch1_7 & [Catch2_90=Catch1_90 & [Catch2_45=Catch1_45 & [Catch2_64=Catch1_64 & [Catch2_60=Catch1_60 & [Catch2_56=Catch1_56 & [Catch2_61=Catch1_61 & [Catch2_17=Catch1_17 & [Catch2_93=Catch1_93 & [Catch2_26=Catch1_26 & [Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [Catch2_85=Catch1_85 & [Catch2_42=Catch1_42 & [Catch2_94=Catch1_94 & [Catch2_86=Catch1_86 & [Catch2_37=Catch1_37 & [Catch2_91=Catch1_91 & [Catch2_13=Catch1_13 & [Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [Catch2_35=Catch1_35 & [Catch2_9=Catch1_9 & [Catch2_73=Catch1_73 & [Catch2_77=Catch1_77 & [Catch2_79=Catch1_79 & [Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [Catch2_49=Catch1_49 & [Catch2_5=Catch1_5 & [Catch2_67=Catch1_67 & [Catch2_97=Catch1_97 & [Catch2_92=Catch1_92 & 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_1847_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[[[[Catch2_80=Fork_80 & [[[[[[[[Catch2_88=Fork_88 & [[[[[[Catch2_82=Fork_82 & [[Catch2_26=Fork_26 & [[[[[[[[[[[[[Catch2_92=Fork_92 & [[Catch2_44=Fork_44 & [[Catch2_14=Fork_14 & [[Catch2_98=Fork_98 & [[Catch2_58=Fork_58 & [[[Catch2_91=Fork_91 & [[Catch2_53=Fork_53 & [Catch2_39=Fork_39 & [Catch2_57=Fork_57 & [Catch2_78=Fork_78 & [[[[[[Catch2_52=Fork_52 & [[[[[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_41=Fork_41 & [[[[[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 & [[[[true & Catch2_50=Fork_50] & Catch2_40=Fork_40] & Catch2_46=Fork_46] & Catch2_54=Fork_54]]]]]]]]]]]]]] & Catch2_37=Fork_37] & 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_32=Fork_32] & Catch2_25=Fork_25] & Catch2_66=Fork_66] & Catch2_10=Fork_10]] & Catch2_61=Fork_61] & Catch2_56=Fork_56] & Catch2_55=Fork_55] & Catch2_90=Fork_90] & Catch2_94=Fork_94]]]]] & Catch2_3=Fork_3]] & Catch2_79=Fork_79] & Catch2_1=Fork_1]] & Catch2_95=Fork_95]] & Catch2_23=Fork_23]] & Catch2_74=Fork_74]] & Catch2_45=Fork_45]] & 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_67=Fork_67]] & 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_20=Fork_20]] & Catch2_48=Fork_48] & Catch2_62=Fork_62] & Catch2_47=Fork_47] & Catch2_73=Fork_73] & [[[Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [[[Catch2_69=Catch1_69 & [[[[[Catch2_3=Catch1_3 & [[[[Catch2_46=Catch1_46 & [[[[Catch2_32=Catch1_32 & [[[[Catch2_2=Catch1_2 & [[[[Catch2_20=Catch1_20 & [[[[Catch2_52=Catch1_52 & [[[[Catch2_25=Catch1_25 & [[[[Catch2_65=Catch1_65 & [[[[Catch2_84=Catch1_84 & [[[Catch2_72=Catch1_72 & [[[[Catch2_41=Catch1_41 & [Catch2_47=Catch1_47 & [[[[Catch2_70=Catch1_70 & [[[Catch2_95=Catch1_95 & [Catch2_53=Catch1_53 & [[[[[[[[[[[[[[[[[[Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [[[[[Catch2_37=Catch1_37 & [[[[[[[[[[Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [[[[[Catch2_92=Catch1_92 & true] & Catch2_97=Catch1_97] & Catch2_67=Catch1_67] & Catch2_5=Catch1_5] & Catch2_49=Catch1_49]]] & Catch2_79=Catch1_79] & Catch2_77=Catch1_77] & Catch2_73=Catch1_73] & Catch2_9=Catch1_9] & Catch2_35=Catch1_35] & Catch2_96=Catch1_96] & Catch2_58=Catch1_58] & Catch2_13=Catch1_13] & Catch2_91=Catch1_91]] & Catch2_86=Catch1_86] & Catch2_94=Catch1_94] & Catch2_42=Catch1_42] & Catch2_85=Catch1_85]]] & Catch2_26=Catch1_26] & Catch2_93=Catch1_93] & Catch2_17=Catch1_17] & Catch2_61=Catch1_61] & Catch2_56=Catch1_56] & Catch2_60=Catch1_60] & Catch2_64=Catch1_64] & Catch2_45=Catch1_45] & Catch2_90=Catch1_90] & Catch2_7=Catch1_7] & Catch2_75=Catch1_75] & Catch2_22=Catch1_22] & Catch2_27=Catch1_27] & Catch2_39=Catch1_39] & Catch2_59=Catch1_59] & Catch2_24=Catch1_24] & Catch2_34=Catch1_34]]] & Catch2_23=Catch1_23] & Catch2_38=Catch1_38]] & Catch2_55=Catch1_55] & Catch2_36=Catch1_36] & Catch2_1=Catch1_1]]] & Catch2_98=Catch1_98] & Catch2_54=Catch1_54] & Catch2_63=Catch1_63]] & Catch2_40=Catch1_40] & Catch2_68=Catch1_68]] & Catch2_6=Catch1_6] & Catch2_10=Catch1_10] & Catch2_76=Catch1_76]] & Catch2_57=Catch1_57] & Catch2_51=Catch1_51] & Catch2_29=Catch1_29]] & Catch2_50=Catch1_50] & Catch2_43=Catch1_43] & Catch2_87=Catch1_87]] & Catch2_62=Catch1_62] & Catch2_11=Catch1_11] & Catch2_4=Catch1_4]] & Catch2_31=Catch1_31] & Catch2_16=Catch1_16] & Catch2_8=Catch1_8]] & Catch2_83=Catch1_83] & Catch2_88=Catch1_88] & Catch2_19=Catch1_19]] & Catch2_21=Catch1_21] & Catch2_14=Catch1_14] & Catch2_82=Catch1_82]] & Catch2_80=Catch1_80] & Catch2_33=Catch1_33] & Catch2_48=Catch1_48]] & Catch2_15=Catch1_15] & Catch2_81=Catch1_81] & Catch2_99=Catch1_99] & Catch2_12=Catch1_12]] & Catch2_74=Catch1_74] & Catch2_44=Catch1_44]]] & Catch2_30=Catch1_30] & Catch2_71=Catch1_71]]]
normalized: E [true U [[Catch2_71=Catch1_71 & [Catch2_30=Catch1_30 & [Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [Catch2_44=Catch1_44 & [Catch2_74=Catch1_74 & [Catch2_69=Catch1_69 & [Catch2_12=Catch1_12 & [Catch2_99=Catch1_99 & [Catch2_81=Catch1_81 & [Catch2_15=Catch1_15 & [Catch2_3=Catch1_3 & [Catch2_48=Catch1_48 & [Catch2_33=Catch1_33 & [Catch2_80=Catch1_80 & [Catch2_46=Catch1_46 & [Catch2_82=Catch1_82 & [Catch2_14=Catch1_14 & [Catch2_21=Catch1_21 & [Catch2_32=Catch1_32 & [Catch2_19=Catch1_19 & [Catch2_88=Catch1_88 & [Catch2_83=Catch1_83 & [Catch2_2=Catch1_2 & [Catch2_8=Catch1_8 & [Catch2_16=Catch1_16 & [Catch2_31=Catch1_31 & [Catch2_20=Catch1_20 & [Catch2_4=Catch1_4 & [Catch2_11=Catch1_11 & [Catch2_62=Catch1_62 & [Catch2_52=Catch1_52 & [Catch2_87=Catch1_87 & [Catch2_43=Catch1_43 & [Catch2_50=Catch1_50 & [Catch2_25=Catch1_25 & [Catch2_29=Catch1_29 & [Catch2_51=Catch1_51 & [Catch2_57=Catch1_57 & [Catch2_65=Catch1_65 & [Catch2_76=Catch1_76 & [Catch2_10=Catch1_10 & [Catch2_6=Catch1_6 & [Catch2_84=Catch1_84 & [Catch2_68=Catch1_68 & [Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [Catch2_63=Catch1_63 & [Catch2_54=Catch1_54 & [Catch2_98=Catch1_98 & [Catch2_41=Catch1_41 & [Catch2_47=Catch1_47 & [Catch2_1=Catch1_1 & [Catch2_36=Catch1_36 & [Catch2_55=Catch1_55 & [Catch2_70=Catch1_70 & [Catch2_38=Catch1_38 & [Catch2_23=Catch1_23 & [Catch2_95=Catch1_95 & [Catch2_53=Catch1_53 & [Catch2_34=Catch1_34 & [Catch2_24=Catch1_24 & [Catch2_59=Catch1_59 & [Catch2_39=Catch1_39 & [Catch2_27=Catch1_27 & [Catch2_22=Catch1_22 & [Catch2_75=Catch1_75 & [Catch2_7=Catch1_7 & [Catch2_90=Catch1_90 & [Catch2_45=Catch1_45 & [Catch2_64=Catch1_64 & [Catch2_60=Catch1_60 & [Catch2_56=Catch1_56 & [Catch2_61=Catch1_61 & [Catch2_17=Catch1_17 & [Catch2_93=Catch1_93 & [Catch2_26=Catch1_26 & [Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [Catch2_85=Catch1_85 & [Catch2_42=Catch1_42 & [Catch2_94=Catch1_94 & [Catch2_86=Catch1_86 & [Catch2_37=Catch1_37 & [Catch2_91=Catch1_91 & [Catch2_13=Catch1_13 & [Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [Catch2_35=Catch1_35 & [Catch2_9=Catch1_9 & [Catch2_73=Catch1_73 & [Catch2_77=Catch1_77 & [Catch2_79=Catch1_79 & [Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [Catch2_49=Catch1_49 & [Catch2_5=Catch1_5 & [Catch2_67=Catch1_67 & [Catch2_97=Catch1_97 & [Catch2_92=Catch1_92 & 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_1848_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[Catch2_71=Catch1_71 & [[Catch2_18=Catch1_18 & [[[[[Catch2_12=Catch1_12 & [[[[[[[Catch2_80=Catch1_80 & [[[[[[[Catch2_88=Catch1_88 & [[Catch2_2=Catch1_2 & [[[[[Catch2_4=Catch1_4 & [[Catch2_62=Catch1_62 & [[[[[[[[[[[[[[[[[[[[[[Catch2_1=Catch1_1 & [[[Catch2_70=Catch1_70 & [[[[[[[Catch2_59=Catch1_59 & [[[[[Catch2_7=Catch1_7 & [[Catch2_45=Catch1_45 & [[[[[[[[[[[[[[[Catch2_91=Catch1_91 & [[[[[Catch2_9=Catch1_9 & [[[[[Catch2_28=Catch1_28 & [[[[[Catch2_92=Catch1_92 & true] & Catch2_97=Catch1_97] & Catch2_67=Catch1_67] & Catch2_5=Catch1_5] & Catch2_49=Catch1_49]] & Catch2_66=Catch1_66] & Catch2_79=Catch1_79] & Catch2_77=Catch1_77] & Catch2_73=Catch1_73]] & Catch2_35=Catch1_35] & Catch2_96=Catch1_96] & Catch2_58=Catch1_58] & Catch2_13=Catch1_13]] & Catch2_37=Catch1_37] & Catch2_86=Catch1_86] & Catch2_94=Catch1_94] & Catch2_42=Catch1_42] & Catch2_85=Catch1_85] & Catch2_100=Catch1_100] & Catch2_89=Catch1_89] & Catch2_26=Catch1_26] & Catch2_93=Catch1_93] & Catch2_17=Catch1_17] & Catch2_61=Catch1_61] & Catch2_56=Catch1_56] & Catch2_60=Catch1_60] & Catch2_64=Catch1_64]] & Catch2_90=Catch1_90]] & Catch2_75=Catch1_75] & Catch2_22=Catch1_22] & Catch2_27=Catch1_27] & Catch2_39=Catch1_39]] & Catch2_24=Catch1_24] & Catch2_34=Catch1_34] & Catch2_53=Catch1_53] & Catch2_95=Catch1_95] & Catch2_23=Catch1_23] & Catch2_38=Catch1_38]] & Catch2_55=Catch1_55] & Catch2_36=Catch1_36]] & Catch2_47=Catch1_47] & Catch2_41=Catch1_41] & Catch2_98=Catch1_98] & Catch2_54=Catch1_54] & Catch2_63=Catch1_63] & Catch2_72=Catch1_72] & Catch2_40=Catch1_40] & Catch2_68=Catch1_68] & Catch2_84=Catch1_84] & Catch2_6=Catch1_6] & Catch2_10=Catch1_10] & Catch2_76=Catch1_76] & Catch2_65=Catch1_65] & Catch2_57=Catch1_57] & Catch2_51=Catch1_51] & Catch2_29=Catch1_29] & Catch2_25=Catch1_25] & Catch2_50=Catch1_50] & Catch2_43=Catch1_43] & Catch2_87=Catch1_87] & Catch2_52=Catch1_52]] & Catch2_11=Catch1_11]] & Catch2_20=Catch1_20] & Catch2_31=Catch1_31] & Catch2_16=Catch1_16] & Catch2_8=Catch1_8]] & Catch2_83=Catch1_83]] & Catch2_19=Catch1_19] & Catch2_32=Catch1_32] & Catch2_21=Catch1_21] & Catch2_14=Catch1_14] & Catch2_82=Catch1_82] & Catch2_46=Catch1_46]] & Catch2_33=Catch1_33] & Catch2_48=Catch1_48] & Catch2_3=Catch1_3] & Catch2_15=Catch1_15] & Catch2_81=Catch1_81] & Catch2_99=Catch1_99]] & Catch2_69=Catch1_69] & Catch2_74=Catch1_74] & Catch2_44=Catch1_44] & Catch2_78=Catch1_78]] & Catch2_30=Catch1_30]] | [[[[[[Catch2_20=Fork_20 & [[[[[Catch2_51=Fork_51 & [[[[[[[[Catch2_82=Fork_82 & [[[Catch2_60=Fork_60 & [[[[[Catch2_31=Fork_31 & [[[Catch2_11=Fork_11 & [[[[[Catch2_45=Fork_45 & [[[[[[Catch2_95=Fork_95 & [[[[Catch2_91=Fork_91 & [[Catch2_53=Fork_53 & [[[Catch2_78=Fork_78 & [[[[[[[[[[[[[[[Catch2_16=Fork_16 & [[[Catch2_30=Fork_30 & [Catch2_97=Fork_97 & [[[[[[[Catch2_93=Fork_93 & [[[Catch2_41=Fork_41 & [Catch2_64=Fork_64 & [[[Catch2_37=Fork_37 & [[[Catch2_81=Fork_81 & [[[[Catch2_68=Fork_68 & [[[Catch2_27=Fork_27 & [Catch2_6=Fork_6 & [[[Catch2_54=Fork_54 & [[[Catch2_50=Fork_50 & true] & Catch2_40=Fork_40] & Catch2_46=Fork_46]] & Catch2_86=Fork_86] & Catch2_42=Fork_42]]] & Catch2_33=Fork_33] & Catch2_99=Fork_99]] & Catch2_84=Fork_84] & Catch2_4=Fork_4] & Catch2_85=Fork_85]] & Catch2_43=Fork_43] & Catch2_36=Fork_36]] & Catch2_100=Fork_100] & Catch2_63=Fork_63]]] & Catch2_35=Fork_35] & Catch2_59=Fork_59]] & 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_28=Fork_28] & Catch2_5=Fork_5]] & 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_10=Fork_10] & 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_3=Fork_3]] & Catch2_79=Fork_79] & Catch2_1=Fork_1] & Catch2_58=Fork_58]] & Catch2_98=Fork_98] & Catch2_23=Fork_23] & 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_13=Fork_13] & Catch2_34=Fork_34]] & Catch2_15=Fork_15] & Catch2_75=Fork_75] & Catch2_38=Fork_38] & Catch2_49=Fork_49]] & Catch2_26=Fork_26] & Catch2_67=Fork_67]] & 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_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 ~ [[[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]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [Catch2_71=Catch1_71 & [Catch2_30=Catch1_30 & [Catch2_18=Catch1_18 & [Catch2_78=Catch1_78 & [Catch2_44=Catch1_44 & [Catch2_74=Catch1_74 & [Catch2_69=Catch1_69 & [Catch2_12=Catch1_12 & [Catch2_99=Catch1_99 & [Catch2_81=Catch1_81 & [Catch2_15=Catch1_15 & [Catch2_3=Catch1_3 & [Catch2_48=Catch1_48 & [Catch2_33=Catch1_33 & [Catch2_80=Catch1_80 & [Catch2_46=Catch1_46 & [Catch2_82=Catch1_82 & [Catch2_14=Catch1_14 & [Catch2_21=Catch1_21 & [Catch2_32=Catch1_32 & [Catch2_19=Catch1_19 & [Catch2_88=Catch1_88 & [Catch2_83=Catch1_83 & [Catch2_2=Catch1_2 & [Catch2_8=Catch1_8 & [Catch2_16=Catch1_16 & [Catch2_31=Catch1_31 & [Catch2_20=Catch1_20 & [Catch2_4=Catch1_4 & [Catch2_11=Catch1_11 & [Catch2_62=Catch1_62 & [Catch2_52=Catch1_52 & [Catch2_87=Catch1_87 & [Catch2_43=Catch1_43 & [Catch2_50=Catch1_50 & [Catch2_25=Catch1_25 & [Catch2_29=Catch1_29 & [Catch2_51=Catch1_51 & [Catch2_57=Catch1_57 & [Catch2_65=Catch1_65 & [Catch2_76=Catch1_76 & [Catch2_10=Catch1_10 & [Catch2_6=Catch1_6 & [Catch2_84=Catch1_84 & [Catch2_68=Catch1_68 & [Catch2_40=Catch1_40 & [Catch2_72=Catch1_72 & [Catch2_63=Catch1_63 & [Catch2_54=Catch1_54 & [Catch2_98=Catch1_98 & [Catch2_41=Catch1_41 & [Catch2_47=Catch1_47 & [Catch2_1=Catch1_1 & [Catch2_36=Catch1_36 & [Catch2_55=Catch1_55 & [Catch2_70=Catch1_70 & [Catch2_38=Catch1_38 & [Catch2_23=Catch1_23 & [Catch2_95=Catch1_95 & [Catch2_53=Catch1_53 & [Catch2_34=Catch1_34 & [Catch2_24=Catch1_24 & [Catch2_59=Catch1_59 & [Catch2_39=Catch1_39 & [Catch2_27=Catch1_27 & [Catch2_22=Catch1_22 & [Catch2_75=Catch1_75 & [Catch2_7=Catch1_7 & [Catch2_90=Catch1_90 & [Catch2_45=Catch1_45 & [Catch2_64=Catch1_64 & [Catch2_60=Catch1_60 & [Catch2_56=Catch1_56 & [Catch2_61=Catch1_61 & [Catch2_17=Catch1_17 & [Catch2_93=Catch1_93 & [Catch2_26=Catch1_26 & [Catch2_89=Catch1_89 & [Catch2_100=Catch1_100 & [Catch2_85=Catch1_85 & [Catch2_42=Catch1_42 & [Catch2_94=Catch1_94 & [Catch2_86=Catch1_86 & [Catch2_37=Catch1_37 & [Catch2_91=Catch1_91 & [Catch2_13=Catch1_13 & [Catch2_58=Catch1_58 & [Catch2_96=Catch1_96 & [Catch2_35=Catch1_35 & [Catch2_9=Catch1_9 & [Catch2_73=Catch1_73 & [Catch2_77=Catch1_77 & [Catch2_79=Catch1_79 & [Catch2_66=Catch1_66 & [Catch2_28=Catch1_28 & [Catch2_49=Catch1_49 & [Catch2_5=Catch1_5 & [Catch2_67=Catch1_67 & [Catch2_97=Catch1_97 & [Catch2_92=Catch1_92 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1849_placecomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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


EG iterations: 0
-> the formula is FALSE

FORMULA p_1850_placecomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[[[Catch2_48>Think_48 & [[[[[[[[[[[[[[[[Catch2_39>Think_39 & [[[[[[[[[[Catch2_7>Think_7 & [[[Catch2_54>Think_54 & [[[[[Catch2_1>Think_1 & [[[[[[[Catch2_26>Think_26 & [[[[[[[[[Catch2_32>Think_32 & [[[[[[[[[[[[Catch2_69>Think_69 & [[[[Catch2_75>Think_75 & [[[[[[[Catch2_13>Think_13 & [[[[[[[[[[[Catch2_56>Think_56 & [[Catch2_4>Think_4 & [[Catch2_28>Think_28 & [[[[[[[[[[[true & Catch2_40>Think_40] & Catch2_88>Think_88] & Catch2_36>Think_36] & Catch2_15>Think_15] & Catch2_16>Think_16] & Catch2_24>Think_24] & Catch2_9>Think_9] & Catch2_92>Think_92] & Catch2_61>Think_61] & Catch2_99>Think_99] & Catch2_57>Think_57]] & Catch2_68>Think_68]] & Catch2_82>Think_82]] & Catch2_42>Think_42] & Catch2_52>Think_52] & Catch2_59>Think_59] & Catch2_98>Think_98] & Catch2_58>Think_58] & Catch2_35>Think_35] & Catch2_30>Think_30] & Catch2_45>Think_45] & Catch2_20>Think_20] & Catch2_79>Think_79]] & Catch2_18>Think_18] & Catch2_83>Think_83] & Catch2_46>Think_46] & Catch2_97>Think_97] & Catch2_51>Think_51] & Catch2_23>Think_23]] & Catch2_81>Think_81] & Catch2_37>Think_37] & Catch2_67>Think_67]] & Catch2_38>Think_38] & Catch2_66>Think_66] & Catch2_100>Think_100] & Catch2_12>Think_12] & Catch2_71>Think_71] & Catch2_96>Think_96] & Catch2_95>Think_95] & Catch2_41>Think_41] & Catch2_21>Think_21] & Catch2_19>Think_19] & Catch2_70>Think_70]] & Catch2_2>Think_2] & Catch2_87>Think_87] & Catch2_31>Think_31] & Catch2_34>Think_34] & Catch2_47>Think_47] & Catch2_29>Think_29] & Catch2_27>Think_27] & Catch2_64>Think_64]] & Catch2_93>Think_93] & Catch2_50>Think_50] & Catch2_94>Think_94] & Catch2_78>Think_78] & Catch2_22>Think_22] & Catch2_76>Think_76]] & Catch2_73>Think_73] & Catch2_85>Think_85] & Catch2_44>Think_44] & Catch2_62>Think_62]] & Catch2_84>Think_84] & Catch2_65>Think_65]] & Catch2_74>Think_74] & Catch2_11>Think_11] & Catch2_14>Think_14] & Catch2_63>Think_63] & Catch2_17>Think_17] & Catch2_25>Think_25] & Catch2_8>Think_8] & Catch2_53>Think_53] & Catch2_86>Think_86]] & Catch2_6>Think_6] & Catch2_55>Think_55] & Catch2_91>Think_91] & Catch2_80>Think_80] & Catch2_10>Think_10] & Catch2_3>Think_3] & Catch2_49>Think_49] & Catch2_33>Think_33] & Catch2_90>Think_90] & Catch2_77>Think_77] & Catch2_89>Think_89] & Catch2_5>Think_5] & Catch2_72>Think_72] & Catch2_43>Think_43] & Catch2_60>Think_60]] & true] & [false | [[[Catch2_43>Think_43 | [[[[[[[Catch2_49>Think_49 | [[[[[[Catch2_6>Think_6 | [[[[[[[[[Catch2_11>Think_11 | [[[Catch2_65>Think_65 | [[[[[[[[[[[[[[[[[Catch2_29>Think_29 | [[[Catch2_31>Think_31 | [[[[[[[[[[[[[[[[[Catch2_37>Think_37 | [[[[[[[[Catch2_18>Think_18 | [[[[[[[[[[[[[[[[Catch2_28>Think_28 | [[[[[[[[Catch2_15>Think_15 | [[[false | Catch2_40>Think_40] | Catch2_88>Think_88] | Catch2_36>Think_36]] | Catch2_16>Think_16] | Catch2_24>Think_24] | Catch2_9>Think_9] | Catch2_92>Think_92] | Catch2_61>Think_61] | Catch2_99>Think_99] | Catch2_57>Think_57]] | Catch2_68>Think_68] | Catch2_4>Think_4] | Catch2_82>Think_82] | Catch2_56>Think_56] | Catch2_42>Think_42] | Catch2_52>Think_52] | Catch2_59>Think_59] | Catch2_98>Think_98] | Catch2_58>Think_58] | Catch2_35>Think_35] | Catch2_30>Think_30] | Catch2_45>Think_45] | Catch2_20>Think_20] | Catch2_79>Think_79] | Catch2_13>Think_13]] | Catch2_83>Think_83] | Catch2_46>Think_46] | Catch2_97>Think_97] | Catch2_51>Think_51] | Catch2_23>Think_23] | Catch2_75>Think_75] | Catch2_81>Think_81]] | Catch2_67>Think_67] | Catch2_69>Think_69] | Catch2_38>Think_38] | Catch2_66>Think_66] | Catch2_100>Think_100] | Catch2_12>Think_12] | Catch2_71>Think_71] | Catch2_96>Think_96] | Catch2_95>Think_95] | Catch2_41>Think_41] | Catch2_21>Think_21] | Catch2_19>Think_19] | Catch2_70>Think_70] | Catch2_32>Think_32] | Catch2_2>Think_2] | Catch2_87>Think_87]] | Catch2_34>Think_34] | Catch2_47>Think_47]] | Catch2_27>Think_27] | Catch2_64>Think_64] | Catch2_26>Think_26] | Catch2_93>Think_93] | Catch2_50>Think_50] | Catch2_94>Think_94] | Catch2_78>Think_78] | Catch2_22>Think_22] | Catch2_76>Think_76] | Catch2_1>Think_1] | Catch2_73>Think_73] | Catch2_85>Think_85] | Catch2_44>Think_44] | Catch2_62>Think_62] | Catch2_54>Think_54] | Catch2_84>Think_84]] | Catch2_7>Think_7] | Catch2_74>Think_74]] | Catch2_14>Think_14] | Catch2_63>Think_63] | Catch2_17>Think_17] | Catch2_25>Think_25] | Catch2_8>Think_8] | Catch2_53>Think_53] | Catch2_86>Think_86] | Catch2_39>Think_39]] | Catch2_55>Think_55] | Catch2_91>Think_91] | Catch2_80>Think_80] | Catch2_10>Think_10] | Catch2_3>Think_3]] | Catch2_33>Think_33] | Catch2_90>Think_90] | Catch2_77>Think_77] | Catch2_89>Think_89] | Catch2_5>Think_5] | Catch2_72>Think_72]] | Catch2_60>Think_60] | Catch2_48>Think_48]]] & [Catch1_27=Catch2_27 & [[[[Catch1_48=Catch2_48 & [[[[Catch1_37=Catch2_37 & [[[[Catch1_44=Catch2_44 & [[Catch1_89=Catch2_89 & [[[[Catch1_36=Catch2_36 & [[Catch1_51=Catch2_51 & [[[[[[[[[[[[[[[Catch1_28=Catch2_28 & [[Catch1_77=Catch2_77 & [[[[Catch1_81=Catch2_81 & [[[[[[[[[[[Catch1_34=Catch2_34 & [[[[[[[[[[[[[[[[[[[[Catch1_25=Catch2_25 & [[[[Catch1_1=Catch2_1 & [[[[[[[[[[[[[[[[[[[[Catch1_11=Catch2_11 & [[[true & Catch1_74=Catch2_74] & Catch1_60=Catch2_60] & Catch1_95=Catch2_95]] & Catch1_62=Catch2_62] & Catch1_90=Catch2_90] & Catch1_100=Catch2_100] & Catch1_2=Catch2_2] & Catch1_46=Catch2_46] & Catch1_26=Catch2_26] & Catch1_52=Catch2_52] & Catch1_22=Catch2_22] & Catch1_99=Catch2_99] & Catch1_3=Catch2_3] & Catch1_19=Catch2_19] & Catch1_83=Catch2_83] & Catch1_24=Catch2_24] & Catch1_18=Catch2_18] & Catch1_43=Catch2_43] & Catch1_88=Catch2_88] & Catch1_54=Catch2_54] & Catch1_58=Catch2_58] & Catch1_68=Catch2_68]] & Catch1_29=Catch2_29] & Catch1_4=Catch2_4] & Catch1_6=Catch2_6]] & Catch1_69=Catch2_69] & Catch1_61=Catch2_61] & Catch1_15=Catch2_15] & Catch1_55=Catch2_55] & Catch1_96=Catch2_96] & Catch1_66=Catch2_66] & Catch1_76=Catch2_76] & Catch1_80=Catch2_80] & Catch1_86=Catch2_86] & Catch1_39=Catch2_39] & Catch1_49=Catch2_49] & Catch1_30=Catch2_30] & Catch1_93=Catch2_93] & Catch1_13=Catch2_13] & Catch1_17=Catch2_17] & Catch1_20=Catch2_20] & Catch1_85=Catch2_85] & Catch1_79=Catch2_79] & Catch1_40=Catch2_40]] & Catch1_65=Catch2_65] & Catch1_57=Catch2_57] & Catch1_82=Catch2_82] & Catch1_42=Catch2_42] & Catch1_14=Catch2_14] & Catch1_73=Catch2_73] & Catch1_67=Catch2_67] & Catch1_9=Catch2_9] & Catch1_91=Catch2_91] & Catch1_8=Catch2_8]] & Catch1_41=Catch2_41] & Catch1_23=Catch2_23] & Catch1_63=Catch2_63]] & Catch1_59=Catch2_59]] & Catch1_10=Catch2_10] & Catch1_56=Catch2_56] & Catch1_21=Catch2_21] & Catch1_78=Catch2_78] & Catch1_47=Catch2_47] & Catch1_75=Catch2_75] & Catch1_31=Catch2_31] & Catch1_87=Catch2_87] & Catch1_71=Catch2_71] & Catch1_12=Catch2_12] & Catch1_97=Catch2_97] & Catch1_16=Catch2_16] & Catch1_53=Catch2_53] & Catch1_84=Catch2_84]] & Catch1_72=Catch2_72]] & Catch1_98=Catch2_98] & Catch1_7=Catch2_7] & Catch1_5=Catch2_5]] & Catch1_35=Catch2_35]] & Catch1_70=Catch2_70] & Catch1_94=Catch2_94] & Catch1_64=Catch2_64]] & Catch1_45=Catch2_45] & Catch1_38=Catch2_38] & Catch1_92=Catch2_92]] & Catch1_33=Catch2_33] & Catch1_32=Catch2_32] & Catch1_50=Catch2_50]]]]
normalized: EG [[[Catch1_27=Catch2_27 & [Catch1_50=Catch2_50 & [Catch1_32=Catch2_32 & [Catch1_33=Catch2_33 & [Catch1_48=Catch2_48 & [Catch1_92=Catch2_92 & [Catch1_38=Catch2_38 & [Catch1_45=Catch2_45 & [Catch1_37=Catch2_37 & [Catch1_64=Catch2_64 & [Catch1_94=Catch2_94 & [Catch1_70=Catch2_70 & [Catch1_44=Catch2_44 & [Catch1_35=Catch2_35 & [Catch1_89=Catch2_89 & [Catch1_5=Catch2_5 & [Catch1_7=Catch2_7 & [Catch1_98=Catch2_98 & [Catch1_36=Catch2_36 & [Catch1_72=Catch2_72 & [Catch1_51=Catch2_51 & [Catch1_84=Catch2_84 & [Catch1_53=Catch2_53 & [Catch1_16=Catch2_16 & [Catch1_97=Catch2_97 & [Catch1_12=Catch2_12 & [Catch1_71=Catch2_71 & [Catch1_87=Catch2_87 & [Catch1_31=Catch2_31 & [Catch1_75=Catch2_75 & [Catch1_47=Catch2_47 & [Catch1_78=Catch2_78 & [Catch1_21=Catch2_21 & [Catch1_56=Catch2_56 & [Catch1_10=Catch2_10 & [Catch1_28=Catch2_28 & [Catch1_59=Catch2_59 & [Catch1_77=Catch2_77 & [Catch1_63=Catch2_63 & [Catch1_23=Catch2_23 & [Catch1_41=Catch2_41 & [Catch1_81=Catch2_81 & [Catch1_8=Catch2_8 & [Catch1_91=Catch2_91 & [Catch1_9=Catch2_9 & [Catch1_67=Catch2_67 & [Catch1_73=Catch2_73 & [Catch1_14=Catch2_14 & [Catch1_42=Catch2_42 & [Catch1_82=Catch2_82 & [Catch1_57=Catch2_57 & [Catch1_65=Catch2_65 & [Catch1_34=Catch2_34 & [Catch1_40=Catch2_40 & [Catch1_79=Catch2_79 & [Catch1_85=Catch2_85 & [Catch1_20=Catch2_20 & [Catch1_17=Catch2_17 & [Catch1_13=Catch2_13 & [Catch1_93=Catch2_93 & [Catch1_30=Catch2_30 & [Catch1_49=Catch2_49 & [Catch1_39=Catch2_39 & [Catch1_86=Catch2_86 & [Catch1_80=Catch2_80 & [Catch1_76=Catch2_76 & [Catch1_66=Catch2_66 & [Catch1_96=Catch2_96 & [Catch1_55=Catch2_55 & [Catch1_15=Catch2_15 & [Catch1_61=Catch2_61 & [Catch1_69=Catch2_69 & [Catch1_25=Catch2_25 & [Catch1_6=Catch2_6 & [Catch1_4=Catch2_4 & [Catch1_29=Catch2_29 & [Catch1_1=Catch2_1 & [Catch1_68=Catch2_68 & [Catch1_58=Catch2_58 & [Catch1_54=Catch2_54 & [Catch1_88=Catch2_88 & [Catch1_43=Catch2_43 & [Catch1_18=Catch2_18 & [Catch1_24=Catch2_24 & [Catch1_83=Catch2_83 & [Catch1_19=Catch2_19 & [Catch1_3=Catch2_3 & [Catch1_99=Catch2_99 & [Catch1_22=Catch2_22 & [Catch1_52=Catch2_52 & [Catch1_26=Catch2_26 & [Catch1_46=Catch2_46 & [Catch1_2=Catch2_2 & [Catch1_100=Catch2_100 & [Catch1_90=Catch2_90 & [Catch1_62=Catch2_62 & [Catch1_11=Catch2_11 & [Catch1_95=Catch2_95 & [Catch1_60=Catch2_60 & [Catch1_74=Catch2_74 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[[Catch2_48>Think_48 | [Catch2_60>Think_60 | [Catch2_43>Think_43 | [Catch2_72>Think_72 | [Catch2_5>Think_5 | [Catch2_89>Think_89 | [Catch2_77>Think_77 | [Catch2_90>Think_90 | [Catch2_33>Think_33 | [Catch2_49>Think_49 | [Catch2_3>Think_3 | [Catch2_10>Think_10 | [Catch2_80>Think_80 | [Catch2_91>Think_91 | [Catch2_55>Think_55 | [Catch2_6>Think_6 | [Catch2_39>Think_39 | [Catch2_86>Think_86 | [Catch2_53>Think_53 | [Catch2_8>Think_8 | [Catch2_25>Think_25 | [Catch2_17>Think_17 | [Catch2_63>Think_63 | [Catch2_14>Think_14 | [Catch2_11>Think_11 | [Catch2_74>Think_74 | [Catch2_7>Think_7 | [Catch2_65>Think_65 | [Catch2_84>Think_84 | [Catch2_54>Think_54 | [Catch2_62>Think_62 | [Catch2_44>Think_44 | [Catch2_85>Think_85 | [Catch2_73>Think_73 | [Catch2_1>Think_1 | [Catch2_76>Think_76 | [Catch2_22>Think_22 | [Catch2_78>Think_78 | [Catch2_94>Think_94 | [Catch2_50>Think_50 | [Catch2_93>Think_93 | [Catch2_26>Think_26 | [Catch2_64>Think_64 | [Catch2_27>Think_27 | [Catch2_29>Think_29 | [Catch2_47>Think_47 | [Catch2_34>Think_34 | [Catch2_31>Think_31 | [Catch2_87>Think_87 | [Catch2_2>Think_2 | [Catch2_32>Think_32 | [Catch2_70>Think_70 | [Catch2_19>Think_19 | [Catch2_21>Think_21 | [Catch2_41>Think_41 | [Catch2_95>Think_95 | [Catch2_96>Think_96 | [Catch2_71>Think_71 | [Catch2_12>Think_12 | [Catch2_100>Think_100 | [Catch2_66>Think_66 | [Catch2_38>Think_38 | [Catch2_69>Think_69 | [Catch2_67>Think_67 | [Catch2_37>Think_37 | [Catch2_81>Think_81 | [Catch2_75>Think_75 | [Catch2_23>Think_23 | [Catch2_51>Think_51 | [Catch2_97>Think_97 | [Catch2_46>Think_46 | [Catch2_83>Think_83 | [Catch2_18>Think_18 | [Catch2_13>Think_13 | [Catch2_79>Think_79 | [Catch2_20>Think_20 | [Catch2_45>Think_45 | [Catch2_30>Think_30 | [Catch2_35>Think_35 | [Catch2_58>Think_58 | [Catch2_98>Think_98 | [Catch2_59>Think_59 | [Catch2_52>Think_52 | [Catch2_42>Think_42 | [Catch2_56>Think_56 | [Catch2_82>Think_82 | [Catch2_4>Think_4 | [Catch2_68>Think_68 | [Catch2_28>Think_28 | [Catch2_57>Think_57 | [Catch2_99>Think_99 | [Catch2_61>Think_61 | [Catch2_92>Think_92 | [Catch2_9>Think_9 | [Catch2_24>Think_24 | [Catch2_16>Think_16 | [Catch2_15>Think_15 | [Catch2_36>Think_36 | [Catch2_88>Think_88 | [Catch2_40>Think_40 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | false] & [true & [Catch2_48>Think_48 & [Catch2_60>Think_60 & [Catch2_43>Think_43 & [Catch2_72>Think_72 & [Catch2_5>Think_5 & [Catch2_89>Think_89 & [Catch2_77>Think_77 & [Catch2_90>Think_90 & [Catch2_33>Think_33 & [Catch2_49>Think_49 & [Catch2_3>Think_3 & [Catch2_10>Think_10 & [Catch2_80>Think_80 & [Catch2_91>Think_91 & [Catch2_55>Think_55 & [Catch2_6>Think_6 & [Catch2_39>Think_39 & [Catch2_86>Think_86 & [Catch2_53>Think_53 & [Catch2_8>Think_8 & [Catch2_25>Think_25 & [Catch2_17>Think_17 & [Catch2_63>Think_63 & [Catch2_14>Think_14 & [Catch2_11>Think_11 & [Catch2_74>Think_74 & [Catch2_7>Think_7 & [Catch2_65>Think_65 & [Catch2_84>Think_84 & [Catch2_54>Think_54 & [Catch2_62>Think_62 & [Catch2_44>Think_44 & [Catch2_85>Think_85 & [Catch2_73>Think_73 & [Catch2_1>Think_1 & [Catch2_76>Think_76 & [Catch2_22>Think_22 & [Catch2_78>Think_78 & [Catch2_94>Think_94 & [Catch2_50>Think_50 & [Catch2_93>Think_93 & [Catch2_26>Think_26 & [Catch2_64>Think_64 & [Catch2_27>Think_27 & [Catch2_29>Think_29 & [Catch2_47>Think_47 & [Catch2_34>Think_34 & [Catch2_31>Think_31 & [Catch2_87>Think_87 & [Catch2_2>Think_2 & [Catch2_32>Think_32 & [Catch2_70>Think_70 & [Catch2_19>Think_19 & [Catch2_21>Think_21 & [Catch2_41>Think_41 & [Catch2_95>Think_95 & [Catch2_96>Think_96 & [Catch2_71>Think_71 & [Catch2_12>Think_12 & [Catch2_100>Think_100 & [Catch2_66>Think_66 & [Catch2_38>Think_38 & [Catch2_69>Think_69 & [Catch2_67>Think_67 & [Catch2_37>Think_37 & [Catch2_81>Think_81 & [Catch2_75>Think_75 & [Catch2_23>Think_23 & [Catch2_51>Think_51 & [Catch2_97>Think_97 & [Catch2_46>Think_46 & [Catch2_83>Think_83 & [Catch2_18>Think_18 & [Catch2_13>Think_13 & [Catch2_79>Think_79 & [Catch2_20>Think_20 & [Catch2_45>Think_45 & [Catch2_30>Think_30 & [Catch2_35>Think_35 & [Catch2_58>Think_58 & [Catch2_98>Think_98 & [Catch2_59>Think_59 & [Catch2_52>Think_52 & [Catch2_42>Think_42 & [Catch2_56>Think_56 & [Catch2_82>Think_82 & [Catch2_4>Think_4 & [Catch2_68>Think_68 & [Catch2_28>Think_28 & [Catch2_57>Think_57 & [Catch2_99>Think_99 & [Catch2_61>Think_61 & [Catch2_92>Think_92 & [Catch2_9>Think_9 & [Catch2_24>Think_24 & [Catch2_16>Think_16 & [Catch2_15>Think_15 & [Catch2_36>Think_36 & [Catch2_88>Think_88 & [Catch2_40>Think_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1851_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[[[[[[[Catch1_38=Catch2_38 & [[[[[[[[Catch1_89=Catch2_89 & [[[[[[[[[[[[[[[[[Catch1_78=Catch2_78 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch1_39=Catch2_39 & [[[[Catch1_66=Catch2_66 & [[[[Catch1_61=Catch2_61 & [[[[[[[[[[[[[[[Catch1_19=Catch2_19 & [[[[[[[Catch1_2=Catch2_2 & [[[[[[[true & Catch1_74=Catch2_74] & Catch1_60=Catch2_60] & Catch1_95=Catch2_95] & Catch1_11=Catch2_11] & Catch1_62=Catch2_62] & Catch1_90=Catch2_90] & Catch1_100=Catch2_100]] & Catch1_46=Catch2_46] & Catch1_26=Catch2_26] & Catch1_52=Catch2_52] & Catch1_22=Catch2_22] & Catch1_99=Catch2_99] & Catch1_3=Catch2_3]] & Catch1_83=Catch2_83] & Catch1_24=Catch2_24] & Catch1_18=Catch2_18] & Catch1_43=Catch2_43] & Catch1_88=Catch2_88] & Catch1_54=Catch2_54] & Catch1_58=Catch2_58] & Catch1_68=Catch2_68] & Catch1_1=Catch2_1] & Catch1_29=Catch2_29] & Catch1_4=Catch2_4] & Catch1_6=Catch2_6] & Catch1_25=Catch2_25] & Catch1_69=Catch2_69]] & Catch1_15=Catch2_15] & Catch1_55=Catch2_55] & Catch1_96=Catch2_96]] & Catch1_76=Catch2_76] & Catch1_80=Catch2_80] & Catch1_86=Catch2_86]] & Catch1_49=Catch2_49] & Catch1_30=Catch2_30] & Catch1_93=Catch2_93] & Catch1_13=Catch2_13] & Catch1_17=Catch2_17] & Catch1_20=Catch2_20] & Catch1_85=Catch2_85] & Catch1_79=Catch2_79] & Catch1_40=Catch2_40] & Catch1_34=Catch2_34] & Catch1_65=Catch2_65] & Catch1_57=Catch2_57] & Catch1_82=Catch2_82] & Catch1_42=Catch2_42] & Catch1_14=Catch2_14] & Catch1_73=Catch2_73] & Catch1_67=Catch2_67] & Catch1_9=Catch2_9] & Catch1_91=Catch2_91] & Catch1_8=Catch2_8] & Catch1_81=Catch2_81] & Catch1_41=Catch2_41] & Catch1_23=Catch2_23] & Catch1_63=Catch2_63] & Catch1_77=Catch2_77] & Catch1_59=Catch2_59] & Catch1_28=Catch2_28] & Catch1_10=Catch2_10] & Catch1_56=Catch2_56] & Catch1_21=Catch2_21]] & Catch1_47=Catch2_47] & Catch1_75=Catch2_75] & Catch1_31=Catch2_31] & Catch1_87=Catch2_87] & Catch1_71=Catch2_71] & Catch1_12=Catch2_12] & Catch1_97=Catch2_97] & Catch1_16=Catch2_16] & Catch1_53=Catch2_53] & Catch1_84=Catch2_84] & Catch1_51=Catch2_51] & Catch1_72=Catch2_72] & Catch1_36=Catch2_36] & Catch1_98=Catch2_98] & Catch1_7=Catch2_7] & Catch1_5=Catch2_5]] & Catch1_35=Catch2_35] & Catch1_44=Catch2_44] & Catch1_70=Catch2_70] & Catch1_94=Catch2_94] & Catch1_64=Catch2_64] & Catch1_37=Catch2_37] & Catch1_45=Catch2_45]] & Catch1_92=Catch2_92] & Catch1_48=Catch2_48] & Catch1_33=Catch2_33] & Catch1_32=Catch2_32] & Catch1_50=Catch2_50] & Catch1_27=Catch2_27] | [[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch2_40>Think_40] & Catch2_88>Think_88] & Catch2_36>Think_36] & Catch2_15>Think_15] & Catch2_16>Think_16] & Catch2_24>Think_24] & Catch2_9>Think_9] & Catch2_92>Think_92] & Catch2_61>Think_61] & Catch2_99>Think_99] & Catch2_57>Think_57] & Catch2_28>Think_28] & Catch2_68>Think_68] & Catch2_4>Think_4] & Catch2_82>Think_82] & Catch2_56>Think_56] & Catch2_42>Think_42] & Catch2_52>Think_52] & Catch2_59>Think_59] & Catch2_98>Think_98] & Catch2_58>Think_58] & Catch2_35>Think_35] & Catch2_30>Think_30] & Catch2_45>Think_45] & Catch2_20>Think_20] & Catch2_79>Think_79] & Catch2_13>Think_13] & Catch2_18>Think_18] & Catch2_83>Think_83] & Catch2_46>Think_46] & Catch2_97>Think_97] & Catch2_51>Think_51] & Catch2_23>Think_23] & Catch2_75>Think_75] & Catch2_81>Think_81] & Catch2_37>Think_37] & Catch2_67>Think_67] & Catch2_69>Think_69] & Catch2_38>Think_38] & Catch2_66>Think_66] & Catch2_100>Think_100] & Catch2_12>Think_12] & Catch2_71>Think_71] & Catch2_96>Think_96] & Catch2_95>Think_95] & Catch2_41>Think_41] & Catch2_21>Think_21] & Catch2_19>Think_19] & Catch2_70>Think_70] & Catch2_32>Think_32] & Catch2_2>Think_2] & Catch2_87>Think_87] & Catch2_31>Think_31] & Catch2_34>Think_34] & Catch2_47>Think_47] & Catch2_29>Think_29] & Catch2_27>Think_27] & Catch2_64>Think_64] & Catch2_26>Think_26] & Catch2_93>Think_93] & Catch2_50>Think_50] & Catch2_94>Think_94] & Catch2_78>Think_78] & Catch2_22>Think_22] & Catch2_76>Think_76] & Catch2_1>Think_1] & Catch2_73>Think_73] & Catch2_85>Think_85] & Catch2_44>Think_44] & Catch2_62>Think_62] & Catch2_54>Think_54] & Catch2_84>Think_84] & Catch2_65>Think_65] & Catch2_7>Think_7] & Catch2_74>Think_74] & Catch2_11>Think_11] & Catch2_14>Think_14] & Catch2_63>Think_63] & Catch2_17>Think_17] & Catch2_25>Think_25] & Catch2_8>Think_8] & Catch2_53>Think_53] & Catch2_86>Think_86] & Catch2_39>Think_39] & Catch2_6>Think_6] & Catch2_55>Think_55] & Catch2_91>Think_91] & Catch2_80>Think_80] & Catch2_10>Think_10] & Catch2_3>Think_3] & Catch2_49>Think_49] & Catch2_33>Think_33] & Catch2_90>Think_90] & Catch2_77>Think_77] & Catch2_89>Think_89] & Catch2_5>Think_5] & Catch2_72>Think_72] & Catch2_43>Think_43] & Catch2_60>Think_60] & Catch2_48>Think_48]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch2_40>Think_40] | Catch2_88>Think_88] | Catch2_36>Think_36] | Catch2_15>Think_15] | Catch2_16>Think_16] | Catch2_24>Think_24] | Catch2_9>Think_9] | Catch2_92>Think_92] | Catch2_61>Think_61] | Catch2_99>Think_99] | Catch2_57>Think_57] | Catch2_28>Think_28] | Catch2_68>Think_68] | Catch2_4>Think_4] | Catch2_82>Think_82] | Catch2_56>Think_56] | Catch2_42>Think_42] | Catch2_52>Think_52] | Catch2_59>Think_59] | Catch2_98>Think_98] | Catch2_58>Think_58] | Catch2_35>Think_35] | Catch2_30>Think_30] | Catch2_45>Think_45] | Catch2_20>Think_20] | Catch2_79>Think_79] | Catch2_13>Think_13] | Catch2_18>Think_18] | Catch2_83>Think_83] | Catch2_46>Think_46] | Catch2_97>Think_97] | Catch2_51>Think_51] | Catch2_23>Think_23] | Catch2_75>Think_75] | Catch2_81>Think_81] | Catch2_37>Think_37] | Catch2_67>Think_67] | Catch2_69>Think_69] | Catch2_38>Think_38] | Catch2_66>Think_66] | Catch2_100>Think_100] | Catch2_12>Think_12] | Catch2_71>Think_71] | Catch2_96>Think_96] | Catch2_95>Think_95] | Catch2_41>Think_41] | Catch2_21>Think_21] | Catch2_19>Think_19] | Catch2_70>Think_70] | Catch2_32>Think_32] | Catch2_2>Think_2] | Catch2_87>Think_87] | Catch2_31>Think_31] | Catch2_34>Think_34] | Catch2_47>Think_47] | Catch2_29>Think_29] | Catch2_27>Think_27] | Catch2_64>Think_64] | Catch2_26>Think_26] | Catch2_93>Think_93] | Catch2_50>Think_50] | Catch2_94>Think_94] | Catch2_78>Think_78] | Catch2_22>Think_22] | Catch2_76>Think_76] | Catch2_1>Think_1] | Catch2_73>Think_73] | Catch2_85>Think_85] | Catch2_44>Think_44] | Catch2_62>Think_62] | Catch2_54>Think_54] | Catch2_84>Think_84] | Catch2_65>Think_65] | Catch2_7>Think_7] | Catch2_74>Think_74] | Catch2_11>Think_11] | Catch2_14>Think_14] | Catch2_63>Think_63] | Catch2_17>Think_17] | Catch2_25>Think_25] | Catch2_8>Think_8] | Catch2_53>Think_53] | Catch2_86>Think_86] | Catch2_39>Think_39] | Catch2_6>Think_6] | Catch2_55>Think_55] | Catch2_91>Think_91] | Catch2_80>Think_80] | Catch2_10>Think_10] | Catch2_3>Think_3] | Catch2_49>Think_49] | Catch2_33>Think_33] | Catch2_90>Think_90] | Catch2_77>Think_77] | Catch2_89>Think_89] | Catch2_5>Think_5] | Catch2_72>Think_72] | Catch2_43>Think_43] | Catch2_60>Think_60] | Catch2_48>Think_48] | false]]]]
normalized: ~ [EG [~ [[[[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch2_40>Think_40] | Catch2_88>Think_88] | Catch2_36>Think_36] | Catch2_15>Think_15] | Catch2_16>Think_16] | Catch2_24>Think_24] | Catch2_9>Think_9] | Catch2_92>Think_92] | Catch2_61>Think_61] | Catch2_99>Think_99] | Catch2_57>Think_57] | Catch2_28>Think_28] | Catch2_68>Think_68] | Catch2_4>Think_4] | Catch2_82>Think_82] | Catch2_56>Think_56] | Catch2_42>Think_42] | Catch2_52>Think_52] | Catch2_59>Think_59] | Catch2_98>Think_98] | Catch2_58>Think_58] | Catch2_35>Think_35] | Catch2_30>Think_30] | Catch2_45>Think_45] | Catch2_20>Think_20] | Catch2_79>Think_79] | Catch2_13>Think_13] | Catch2_18>Think_18] | Catch2_83>Think_83] | Catch2_46>Think_46] | Catch2_97>Think_97] | Catch2_51>Think_51] | Catch2_23>Think_23] | Catch2_75>Think_75] | Catch2_81>Think_81] | Catch2_37>Think_37] | Catch2_67>Think_67] | Catch2_69>Think_69] | Catch2_38>Think_38] | Catch2_66>Think_66] | Catch2_100>Think_100] | Catch2_12>Think_12] | Catch2_71>Think_71] | Catch2_96>Think_96] | Catch2_95>Think_95] | Catch2_41>Think_41] | Catch2_21>Think_21] | Catch2_19>Think_19] | Catch2_70>Think_70] | Catch2_32>Think_32] | Catch2_2>Think_2] | Catch2_87>Think_87] | Catch2_31>Think_31] | Catch2_34>Think_34] | Catch2_47>Think_47] | Catch2_29>Think_29] | Catch2_27>Think_27] | Catch2_64>Think_64] | Catch2_26>Think_26] | Catch2_93>Think_93] | Catch2_50>Think_50] | Catch2_94>Think_94] | Catch2_78>Think_78] | Catch2_22>Think_22] | Catch2_76>Think_76] | Catch2_1>Think_1] | Catch2_73>Think_73] | Catch2_85>Think_85] | Catch2_44>Think_44] | Catch2_62>Think_62] | Catch2_54>Think_54] | Catch2_84>Think_84] | Catch2_65>Think_65] | Catch2_7>Think_7] | Catch2_74>Think_74] | Catch2_11>Think_11] | Catch2_14>Think_14] | Catch2_63>Think_63] | Catch2_17>Think_17] | Catch2_25>Think_25] | Catch2_8>Think_8] | Catch2_53>Think_53] | Catch2_86>Think_86] | Catch2_39>Think_39] | Catch2_6>Think_6] | Catch2_55>Think_55] | Catch2_91>Think_91] | Catch2_80>Think_80] | Catch2_10>Think_10] | Catch2_3>Think_3] | Catch2_49>Think_49] | Catch2_33>Think_33] | Catch2_90>Think_90] | Catch2_77>Think_77] | Catch2_89>Think_89] | Catch2_5>Think_5] | Catch2_72>Think_72] | Catch2_43>Think_43] | Catch2_60>Think_60] | Catch2_48>Think_48]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Catch2_93>Think_93 & [Catch2_26>Think_26 & [Catch2_64>Think_64 & [Catch2_27>Think_27 & [Catch2_29>Think_29 & [Catch2_47>Think_47 & [Catch2_34>Think_34 & [Catch2_31>Think_31 & [Catch2_87>Think_87 & [Catch2_2>Think_2 & [Catch2_32>Think_32 & [Catch2_70>Think_70 & [Catch2_19>Think_19 & [Catch2_21>Think_21 & [Catch2_41>Think_41 & [Catch2_95>Think_95 & [Catch2_96>Think_96 & [Catch2_71>Think_71 & [Catch2_12>Think_12 & [Catch2_100>Think_100 & [Catch2_66>Think_66 & [Catch2_38>Think_38 & [Catch2_69>Think_69 & [Catch2_67>Think_67 & [Catch2_37>Think_37 & [Catch2_81>Think_81 & [Catch2_75>Think_75 & [Catch2_23>Think_23 & [Catch2_51>Think_51 & [Catch2_97>Think_97 & [Catch2_46>Think_46 & [Catch2_83>Think_83 & [Catch2_18>Think_18 & [Catch2_13>Think_13 & [Catch2_79>Think_79 & [Catch2_20>Think_20 & [Catch2_45>Think_45 & [Catch2_30>Think_30 & [Catch2_35>Think_35 & [Catch2_58>Think_58 & [Catch2_98>Think_98 & [Catch2_59>Think_59 & [Catch2_52>Think_52 & [Catch2_42>Think_42 & [Catch2_56>Think_56 & [Catch2_82>Think_82 & [Catch2_4>Think_4 & [Catch2_68>Think_68 & [Catch2_28>Think_28 & [Catch2_57>Think_57 & [Catch2_99>Think_99 & [Catch2_61>Think_61 & [Catch2_92>Think_92 & [Catch2_9>Think_9 & [Catch2_24>Think_24 & [Catch2_16>Think_16 & [Catch2_15>Think_15 & [Catch2_36>Think_36 & [Catch2_88>Think_88 & [Catch2_40>Think_40 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Catch2_50>Think_50] & Catch2_94>Think_94] & Catch2_78>Think_78] & Catch2_22>Think_22] & Catch2_76>Think_76] & Catch2_1>Think_1] & Catch2_73>Think_73] & Catch2_85>Think_85] & Catch2_44>Think_44] & Catch2_62>Think_62] & Catch2_54>Think_54] & Catch2_84>Think_84] & Catch2_65>Think_65] & Catch2_7>Think_7] & Catch2_74>Think_74] & Catch2_11>Think_11] & Catch2_14>Think_14] & Catch2_63>Think_63] & Catch2_17>Think_17] & Catch2_25>Think_25] & Catch2_8>Think_8] & Catch2_53>Think_53] & Catch2_86>Think_86] & Catch2_39>Think_39] & Catch2_6>Think_6] & Catch2_55>Think_55] & Catch2_91>Think_91] & Catch2_80>Think_80] & Catch2_10>Think_10] & Catch2_3>Think_3] & Catch2_49>Think_49] & Catch2_33>Think_33] & Catch2_90>Think_90] & Catch2_77>Think_77] & Catch2_89>Think_89] & Catch2_5>Think_5] & Catch2_72>Think_72] & Catch2_43>Think_43] & Catch2_60>Think_60] & Catch2_48>Think_48] & true]] | [Catch1_27=Catch2_27 & [Catch1_50=Catch2_50 & [Catch1_32=Catch2_32 & [Catch1_33=Catch2_33 & [Catch1_48=Catch2_48 & [Catch1_92=Catch2_92 & [Catch1_38=Catch2_38 & [Catch1_45=Catch2_45 & [Catch1_37=Catch2_37 & [Catch1_64=Catch2_64 & [Catch1_94=Catch2_94 & [Catch1_70=Catch2_70 & [Catch1_44=Catch2_44 & [Catch1_35=Catch2_35 & [Catch1_89=Catch2_89 & [Catch1_5=Catch2_5 & [Catch1_7=Catch2_7 & [Catch1_98=Catch2_98 & [Catch1_36=Catch2_36 & [Catch1_72=Catch2_72 & [Catch1_51=Catch2_51 & [Catch1_84=Catch2_84 & [Catch1_53=Catch2_53 & [Catch1_16=Catch2_16 & [Catch1_97=Catch2_97 & [Catch1_12=Catch2_12 & [Catch1_71=Catch2_71 & [Catch1_87=Catch2_87 & [Catch1_31=Catch2_31 & [Catch1_75=Catch2_75 & [Catch1_47=Catch2_47 & [Catch1_78=Catch2_78 & [Catch1_21=Catch2_21 & [Catch1_56=Catch2_56 & [Catch1_10=Catch2_10 & [Catch1_28=Catch2_28 & [Catch1_59=Catch2_59 & [Catch1_77=Catch2_77 & [Catch1_63=Catch2_63 & [Catch1_23=Catch2_23 & [Catch1_41=Catch2_41 & [Catch1_81=Catch2_81 & [Catch1_8=Catch2_8 & [Catch1_91=Catch2_91 & [Catch1_9=Catch2_9 & [Catch1_67=Catch2_67 & [Catch1_73=Catch2_73 & [Catch1_14=Catch2_14 & [Catch1_42=Catch2_42 & [Catch1_82=Catch2_82 & [Catch1_57=Catch2_57 & [Catch1_65=Catch2_65 & [Catch1_34=Catch2_34 & [Catch1_40=Catch2_40 & [Catch1_79=Catch2_79 & [Catch1_85=Catch2_85 & [Catch1_20=Catch2_20 & [Catch1_17=Catch2_17 & [Catch1_13=Catch2_13 & [Catch1_93=Catch2_93 & [Catch1_30=Catch2_30 & [Catch1_49=Catch2_49 & [Catch1_39=Catch2_39 & [Catch1_86=Catch2_86 & [Catch1_80=Catch2_80 & [Catch1_76=Catch2_76 & [Catch1_66=Catch2_66 & [Catch1_96=Catch2_96 & [Catch1_55=Catch2_55 & [Catch1_15=Catch2_15 & [Catch1_61=Catch2_61 & [Catch1_69=Catch2_69 & [Catch1_25=Catch2_25 & [Catch1_6=Catch2_6 & [Catch1_4=Catch2_4 & [Catch1_29=Catch2_29 & [Catch1_1=Catch2_1 & [Catch1_68=Catch2_68 & [Catch1_58=Catch2_58 & [Catch1_54=Catch2_54 & [Catch1_88=Catch2_88 & [Catch1_43=Catch2_43 & [Catch1_18=Catch2_18 & [Catch1_24=Catch2_24 & [Catch1_83=Catch2_83 & [Catch1_19=Catch2_19 & [Catch1_3=Catch2_3 & [Catch1_99=Catch2_99 & [Catch1_22=Catch2_22 & [Catch1_52=Catch2_52 & [Catch1_26=Catch2_26 & [Catch1_46=Catch2_46 & [Catch1_2=Catch2_2 & [Catch1_100=Catch2_100 & [Catch1_90=Catch2_90 & [Catch1_62=Catch2_62 & [Catch1_11=Catch2_11 & [Catch1_95=Catch2_95 & [Catch1_60=Catch2_60 & [Catch1_74=Catch2_74 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1852_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_74=Catch2_74] & Catch1_60=Catch2_60] & Catch1_95=Catch2_95] & Catch1_11=Catch2_11] & Catch1_62=Catch2_62] & Catch1_90=Catch2_90] & Catch1_100=Catch2_100] & Catch1_2=Catch2_2] & Catch1_46=Catch2_46] & Catch1_26=Catch2_26] & Catch1_52=Catch2_52] & Catch1_22=Catch2_22] & Catch1_99=Catch2_99] & Catch1_3=Catch2_3] & Catch1_19=Catch2_19] & Catch1_83=Catch2_83] & Catch1_24=Catch2_24] & Catch1_18=Catch2_18] & Catch1_43=Catch2_43] & Catch1_88=Catch2_88] & Catch1_54=Catch2_54] & Catch1_58=Catch2_58] & Catch1_68=Catch2_68] & Catch1_1=Catch2_1] & Catch1_29=Catch2_29] & Catch1_4=Catch2_4] & Catch1_6=Catch2_6] & Catch1_25=Catch2_25] & Catch1_69=Catch2_69] & Catch1_61=Catch2_61] & Catch1_15=Catch2_15] & Catch1_55=Catch2_55] & Catch1_96=Catch2_96] & Catch1_66=Catch2_66] & Catch1_76=Catch2_76] & Catch1_80=Catch2_80] & Catch1_86=Catch2_86] & Catch1_39=Catch2_39] & Catch1_49=Catch2_49] & Catch1_30=Catch2_30] & Catch1_93=Catch2_93] & Catch1_13=Catch2_13] & Catch1_17=Catch2_17] & Catch1_20=Catch2_20] & Catch1_85=Catch2_85] & Catch1_79=Catch2_79] & Catch1_40=Catch2_40] & Catch1_34=Catch2_34] & Catch1_65=Catch2_65] & Catch1_57=Catch2_57] & Catch1_82=Catch2_82] & Catch1_42=Catch2_42] & Catch1_14=Catch2_14] & Catch1_73=Catch2_73] & Catch1_67=Catch2_67] & Catch1_9=Catch2_9] & Catch1_91=Catch2_91] & Catch1_8=Catch2_8] & Catch1_81=Catch2_81] & Catch1_41=Catch2_41] & Catch1_23=Catch2_23] & Catch1_63=Catch2_63] & Catch1_77=Catch2_77] & Catch1_59=Catch2_59] & Catch1_28=Catch2_28] & Catch1_10=Catch2_10] & Catch1_56=Catch2_56] & Catch1_21=Catch2_21] & Catch1_78=Catch2_78] & Catch1_47=Catch2_47] & Catch1_75=Catch2_75] & Catch1_31=Catch2_31] & Catch1_87=Catch2_87] & Catch1_71=Catch2_71] & Catch1_12=Catch2_12] & Catch1_97=Catch2_97] & Catch1_16=Catch2_16] & Catch1_53=Catch2_53] & Catch1_84=Catch2_84] & Catch1_51=Catch2_51] & Catch1_72=Catch2_72] & Catch1_36=Catch2_36] & Catch1_98=Catch2_98] & Catch1_7=Catch2_7] & Catch1_5=Catch2_5] & Catch1_89=Catch2_89] & Catch1_35=Catch2_35] & Catch1_44=Catch2_44] & Catch1_70=Catch2_70] & Catch1_94=Catch2_94] & Catch1_64=Catch2_64] & Catch1_37=Catch2_37] & Catch1_45=Catch2_45] & Catch1_38=Catch2_38] & Catch1_92=Catch2_92] & Catch1_48=Catch2_48] & Catch1_33=Catch2_33] & Catch1_32=Catch2_32] & Catch1_50=Catch2_50] & Catch1_27=Catch2_27] & [[true & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch2_40>Think_40] & Catch2_88>Think_88] & Catch2_36>Think_36] & Catch2_15>Think_15] & Catch2_16>Think_16] & Catch2_24>Think_24] & Catch2_9>Think_9] & Catch2_92>Think_92] & Catch2_61>Think_61] & Catch2_99>Think_99] & Catch2_57>Think_57] & Catch2_28>Think_28] & Catch2_68>Think_68] & Catch2_4>Think_4] & Catch2_82>Think_82] & Catch2_56>Think_56] & Catch2_42>Think_42] & Catch2_52>Think_52] & Catch2_59>Think_59] & Catch2_98>Think_98] & Catch2_58>Think_58] & Catch2_35>Think_35] & Catch2_30>Think_30] & Catch2_45>Think_45] & Catch2_20>Think_20] & Catch2_79>Think_79] & Catch2_13>Think_13] & Catch2_18>Think_18] & Catch2_83>Think_83] & Catch2_46>Think_46] & Catch2_97>Think_97] & Catch2_51>Think_51] & Catch2_23>Think_23] & Catch2_75>Think_75] & Catch2_81>Think_81] & Catch2_37>Think_37] & Catch2_67>Think_67] & Catch2_69>Think_69] & Catch2_38>Think_38] & Catch2_66>Think_66] & Catch2_100>Think_100] & Catch2_12>Think_12] & Catch2_71>Think_71] & Catch2_96>Think_96] & Catch2_95>Think_95] & Catch2_41>Think_41] & Catch2_21>Think_21] & Catch2_19>Think_19] & Catch2_70>Think_70] & Catch2_32>Think_32] & Catch2_2>Think_2] & Catch2_87>Think_87] & Catch2_31>Think_31] & Catch2_34>Think_34] & Catch2_47>Think_47] & Catch2_29>Think_29] & Catch2_27>Think_27] & Catch2_64>Think_64] & Catch2_26>Think_26] & Catch2_93>Think_93] & Catch2_50>Think_50] & Catch2_94>Think_94] & Catch2_78>Think_78] & Catch2_22>Think_22] & Catch2_76>Think_76] & Catch2_1>Think_1] & Catch2_73>Think_73] & Catch2_85>Think_85] & Catch2_44>Think_44] & Catch2_62>Think_62] & Catch2_54>Think_54] & Catch2_84>Think_84] & Catch2_65>Think_65] & Catch2_7>Think_7] & Catch2_74>Think_74] & Catch2_11>Think_11] & Catch2_14>Think_14] & Catch2_63>Think_63] & Catch2_17>Think_17] & Catch2_25>Think_25] & Catch2_8>Think_8] & Catch2_53>Think_53] & Catch2_86>Think_86] & Catch2_39>Think_39] & Catch2_6>Think_6] & Catch2_55>Think_55] & Catch2_91>Think_91] & Catch2_80>Think_80] & Catch2_10>Think_10] & Catch2_3>Think_3] & Catch2_49>Think_49] & Catch2_33>Think_33] & Catch2_90>Think_90] & Catch2_77>Think_77] & Catch2_89>Think_89] & Catch2_5>Think_5] & Catch2_72>Think_72] & Catch2_43>Think_43] & Catch2_60>Think_60] & Catch2_48>Think_48]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch2_40>Think_40] | Catch2_88>Think_88] | Catch2_36>Think_36] | Catch2_15>Think_15] | Catch2_16>Think_16] | Catch2_24>Think_24] | Catch2_9>Think_9] | Catch2_92>Think_92] | Catch2_61>Think_61] | Catch2_99>Think_99] | Catch2_57>Think_57] | Catch2_28>Think_28] | Catch2_68>Think_68] | Catch2_4>Think_4] | Catch2_82>Think_82] | Catch2_56>Think_56] | Catch2_42>Think_42] | Catch2_52>Think_52] | Catch2_59>Think_59] | Catch2_98>Think_98] | Catch2_58>Think_58] | Catch2_35>Think_35] | Catch2_30>Think_30] | Catch2_45>Think_45] | Catch2_20>Think_20] | Catch2_79>Think_79] | Catch2_13>Think_13] | Catch2_18>Think_18] | Catch2_83>Think_83] | Catch2_46>Think_46] | Catch2_97>Think_97] | Catch2_51>Think_51] | Catch2_23>Think_23] | Catch2_75>Think_75] | Catch2_81>Think_81] | Catch2_37>Think_37] | Catch2_67>Think_67] | Catch2_69>Think_69] | Catch2_38>Think_38] | Catch2_66>Think_66] | Catch2_100>Think_100] | Catch2_12>Think_12] | Catch2_71>Think_71] | Catch2_96>Think_96] | Catch2_95>Think_95] | Catch2_41>Think_41] | Catch2_21>Think_21] | Catch2_19>Think_19] | Catch2_70>Think_70] | Catch2_32>Think_32] | Catch2_2>Think_2] | Catch2_87>Think_87] | Catch2_31>Think_31] | Catch2_34>Think_34] | Catch2_47>Think_47] | Catch2_29>Think_29] | Catch2_27>Think_27] | Catch2_64>Think_64] | Catch2_26>Think_26] | Catch2_93>Think_93] | Catch2_50>Think_50] | Catch2_94>Think_94] | Catch2_78>Think_78] | Catch2_22>Think_22] | Catch2_76>Think_76] | Catch2_1>Think_1] | Catch2_73>Think_73] | Catch2_85>Think_85] | Catch2_44>Think_44] | Catch2_62>Think_62] | Catch2_54>Think_54] | Catch2_84>Think_84] | Catch2_65>Think_65] | Catch2_7>Think_7] | Catch2_74>Think_74] | Catch2_11>Think_11] | Catch2_14>Think_14] | Catch2_63>Think_63] | Catch2_17>Think_17] | Catch2_25>Think_25] | Catch2_8>Think_8] | Catch2_53>Think_53] | Catch2_86>Think_86] | Catch2_39>Think_39] | Catch2_6>Think_6] | Catch2_55>Think_55] | Catch2_91>Think_91] | Catch2_80>Think_80] | Catch2_10>Think_10] | Catch2_3>Think_3] | Catch2_49>Think_49] | Catch2_33>Think_33] | Catch2_90>Think_90] | Catch2_77>Think_77] | Catch2_89>Think_89] | Catch2_5>Think_5] | Catch2_72>Think_72] | Catch2_43>Think_43] | Catch2_60>Think_60] | Catch2_48>Think_48] | false]]]]
normalized: EG [[[[false | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[false | Catch2_40>Think_40] | Catch2_88>Think_88] | Catch2_36>Think_36] | Catch2_15>Think_15] | Catch2_16>Think_16] | Catch2_24>Think_24] | Catch2_9>Think_9] | Catch2_92>Think_92] | Catch2_61>Think_61] | Catch2_99>Think_99] | Catch2_57>Think_57] | Catch2_28>Think_28] | Catch2_68>Think_68] | Catch2_4>Think_4] | Catch2_82>Think_82] | Catch2_56>Think_56] | Catch2_42>Think_42] | Catch2_52>Think_52] | Catch2_59>Think_59] | Catch2_98>Think_98] | Catch2_58>Think_58] | Catch2_35>Think_35] | Catch2_30>Think_30] | Catch2_45>Think_45] | Catch2_20>Think_20] | Catch2_79>Think_79] | Catch2_13>Think_13] | Catch2_18>Think_18] | Catch2_83>Think_83] | Catch2_46>Think_46] | Catch2_97>Think_97] | Catch2_51>Think_51] | Catch2_23>Think_23] | Catch2_75>Think_75] | Catch2_81>Think_81] | Catch2_37>Think_37] | Catch2_67>Think_67] | Catch2_69>Think_69] | Catch2_38>Think_38] | Catch2_66>Think_66] | Catch2_100>Think_100] | Catch2_12>Think_12] | Catch2_71>Think_71] | Catch2_96>Think_96] | Catch2_95>Think_95] | Catch2_41>Think_41] | Catch2_21>Think_21] | Catch2_19>Think_19] | Catch2_70>Think_70] | Catch2_32>Think_32] | Catch2_2>Think_2] | Catch2_87>Think_87] | Catch2_31>Think_31] | Catch2_34>Think_34] | Catch2_47>Think_47] | Catch2_29>Think_29] | Catch2_27>Think_27] | Catch2_64>Think_64] | Catch2_26>Think_26] | Catch2_93>Think_93] | Catch2_50>Think_50] | Catch2_94>Think_94] | Catch2_78>Think_78] | Catch2_22>Think_22] | Catch2_76>Think_76] | Catch2_1>Think_1] | Catch2_73>Think_73] | Catch2_85>Think_85] | Catch2_44>Think_44] | Catch2_62>Think_62] | Catch2_54>Think_54] | Catch2_84>Think_84] | Catch2_65>Think_65] | Catch2_7>Think_7] | Catch2_74>Think_74] | Catch2_11>Think_11] | Catch2_14>Think_14] | Catch2_63>Think_63] | Catch2_17>Think_17] | Catch2_25>Think_25] | Catch2_8>Think_8] | Catch2_53>Think_53] | Catch2_86>Think_86] | Catch2_39>Think_39] | Catch2_6>Think_6] | Catch2_55>Think_55] | Catch2_91>Think_91] | Catch2_80>Think_80] | Catch2_10>Think_10] | Catch2_3>Think_3] | Catch2_49>Think_49] | Catch2_33>Think_33] | Catch2_90>Think_90] | Catch2_77>Think_77] | Catch2_89>Think_89] | Catch2_5>Think_5] | Catch2_72>Think_72] | Catch2_43>Think_43] | Catch2_60>Think_60] | Catch2_48>Think_48]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch2_40>Think_40] & Catch2_88>Think_88] & Catch2_36>Think_36] & Catch2_15>Think_15] & Catch2_16>Think_16] & Catch2_24>Think_24] & Catch2_9>Think_9] & Catch2_92>Think_92] & Catch2_61>Think_61] & Catch2_99>Think_99] & Catch2_57>Think_57] & Catch2_28>Think_28] & Catch2_68>Think_68] & Catch2_4>Think_4] & Catch2_82>Think_82] & Catch2_56>Think_56] & Catch2_42>Think_42] & Catch2_52>Think_52] & Catch2_59>Think_59] & Catch2_98>Think_98] & Catch2_58>Think_58] & Catch2_35>Think_35] & Catch2_30>Think_30] & Catch2_45>Think_45] & Catch2_20>Think_20] & Catch2_79>Think_79] & Catch2_13>Think_13] & Catch2_18>Think_18] & Catch2_83>Think_83] & Catch2_46>Think_46] & Catch2_97>Think_97] & Catch2_51>Think_51] & Catch2_23>Think_23] & Catch2_75>Think_75] & Catch2_81>Think_81] & Catch2_37>Think_37] & Catch2_67>Think_67] & Catch2_69>Think_69] & Catch2_38>Think_38] & Catch2_66>Think_66] & Catch2_100>Think_100] & Catch2_12>Think_12] & Catch2_71>Think_71] & Catch2_96>Think_96] & Catch2_95>Think_95] & Catch2_41>Think_41] & Catch2_21>Think_21] & Catch2_19>Think_19] & Catch2_70>Think_70] & Catch2_32>Think_32] & Catch2_2>Think_2] & Catch2_87>Think_87] & Catch2_31>Think_31] & Catch2_34>Think_34] & Catch2_47>Think_47] & Catch2_29>Think_29] & Catch2_27>Think_27] & Catch2_64>Think_64] & Catch2_26>Think_26] & Catch2_93>Think_93] & Catch2_50>Think_50] & Catch2_94>Think_94] & Catch2_78>Think_78] & Catch2_22>Think_22] & Catch2_76>Think_76] & Catch2_1>Think_1] & Catch2_73>Think_73] & Catch2_85>Think_85] & Catch2_44>Think_44] & Catch2_62>Think_62] & Catch2_54>Think_54] & Catch2_84>Think_84] & Catch2_65>Think_65] & Catch2_7>Think_7] & Catch2_74>Think_74] & Catch2_11>Think_11] & Catch2_14>Think_14] & Catch2_63>Think_63] & Catch2_17>Think_17] & Catch2_25>Think_25] & Catch2_8>Think_8] & Catch2_53>Think_53] & Catch2_86>Think_86] & Catch2_39>Think_39] & Catch2_6>Think_6] & Catch2_55>Think_55] & Catch2_91>Think_91] & Catch2_80>Think_80] & Catch2_10>Think_10] & Catch2_3>Think_3] & Catch2_49>Think_49] & Catch2_33>Think_33] & Catch2_90>Think_90] & Catch2_77>Think_77] & Catch2_89>Think_89] & Catch2_5>Think_5] & Catch2_72>Think_72] & Catch2_43>Think_43] & Catch2_60>Think_60] & Catch2_48>Think_48] & true]] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & Catch1_74=Catch2_74] & Catch1_60=Catch2_60] & Catch1_95=Catch2_95] & Catch1_11=Catch2_11] & Catch1_62=Catch2_62] & Catch1_90=Catch2_90] & Catch1_100=Catch2_100] & Catch1_2=Catch2_2] & Catch1_46=Catch2_46] & Catch1_26=Catch2_26] & Catch1_52=Catch2_52] & Catch1_22=Catch2_22] & Catch1_99=Catch2_99] & Catch1_3=Catch2_3] & Catch1_19=Catch2_19] & Catch1_83=Catch2_83] & Catch1_24=Catch2_24] & Catch1_18=Catch2_18] & Catch1_43=Catch2_43] & Catch1_88=Catch2_88] & Catch1_54=Catch2_54] & Catch1_58=Catch2_58] & Catch1_68=Catch2_68] & Catch1_1=Catch2_1] & Catch1_29=Catch2_29] & Catch1_4=Catch2_4] & Catch1_6=Catch2_6] & Catch1_25=Catch2_25] & Catch1_69=Catch2_69] & Catch1_61=Catch2_61] & Catch1_15=Catch2_15] & Catch1_55=Catch2_55] & Catch1_96=Catch2_96] & Catch1_66=Catch2_66] & Catch1_76=Catch2_76] & Catch1_80=Catch2_80] & Catch1_86=Catch2_86] & Catch1_39=Catch2_39] & Catch1_49=Catch2_49] & Catch1_30=Catch2_30] & Catch1_93=Catch2_93] & Catch1_13=Catch2_13] & Catch1_17=Catch2_17] & Catch1_20=Catch2_20] & Catch1_85=Catch2_85] & Catch1_79=Catch2_79] & Catch1_40=Catch2_40] & Catch1_34=Catch2_34] & Catch1_65=Catch2_65] & Catch1_57=Catch2_57] & Catch1_82=Catch2_82] & Catch1_42=Catch2_42] & Catch1_14=Catch2_14] & Catch1_73=Catch2_73] & Catch1_67=Catch2_67] & Catch1_9=Catch2_9] & Catch1_91=Catch2_91] & Catch1_8=Catch2_8] & Catch1_81=Catch2_81] & Catch1_41=Catch2_41] & Catch1_23=Catch2_23] & Catch1_63=Catch2_63] & Catch1_77=Catch2_77] & Catch1_59=Catch2_59] & Catch1_28=Catch2_28] & Catch1_10=Catch2_10] & Catch1_56=Catch2_56] & Catch1_21=Catch2_21] & Catch1_78=Catch2_78] & Catch1_47=Catch2_47] & Catch1_75=Catch2_75] & Catch1_31=Catch2_31] & Catch1_87=Catch2_87] & Catch1_71=Catch2_71] & Catch1_12=Catch2_12] & Catch1_97=Catch2_97] & Catch1_16=Catch2_16] & Catch1_53=Catch2_53] & Catch1_84=Catch2_84] & Catch1_51=Catch2_51] & Catch1_72=Catch2_72] & Catch1_36=Catch2_36] & Catch1_98=Catch2_98] & Catch1_7=Catch2_7] & Catch1_5=Catch2_5] & Catch1_89=Catch2_89] & Catch1_35=Catch2_35] & Catch1_44=Catch2_44] & Catch1_70=Catch2_70] & Catch1_94=Catch2_94] & Catch1_64=Catch2_64] & Catch1_37=Catch2_37] & Catch1_45=Catch2_45] & Catch1_38=Catch2_38] & Catch1_92=Catch2_92] & Catch1_48=Catch2_48] & Catch1_33=Catch2_33] & Catch1_32=Catch2_32] & Catch1_50=Catch2_50] & Catch1_27=Catch2_27]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1853_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m9sec

STOP 1369712434

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

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