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

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

START 1369715697

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 500 NrTr: 500)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


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



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

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


EG iterations: 0
-> the formula is FALSE

FORMULA p_1856_cardinalitycomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is FALSE

FORMULA p_1857_cardinalitycomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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

-> the formula is FALSE

FORMULA p_1858_cardinalitycomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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


EG iterations: 0
-> the formula is FALSE

FORMULA p_1859_cardinalitycomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

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


EG iterations: 0

EG iterations: 0

EG iterations: 0
-> the formula is FALSE

FORMULA p_1860_cardinalitycomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1861_cardinalitycomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]
normalized: ~ [E [true U ~ [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) | ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]]]

-> the formula is FALSE

FORMULA p_1862_cardinalitycomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]]
normalized: EG [[ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Think_68 + Think_52 ) + Think_44 ) + Think_2 ) + Think_38 ) + Think_36 ) + Think_26 ) + Think_60 ) + Think_6 ) + Think_13 ) + Think_11 ) + Think_4 ) + Think_87 ) + Think_59 ) + Think_9 ) + Think_40 ) + Think_23 ) + Think_99 ) + Think_56 ) + Think_57 ) + Think_94 ) + Think_22 ) + Think_63 ) + Think_74 ) + Think_98 ) + Think_55 ) + Think_92 ) + Think_76 ) + Think_93 ) + Think_12 ) + Think_19 ) + Think_49 ) + Think_53 ) + Think_48 ) + Think_17 ) + Think_8 ) + Think_10 ) + Think_58 ) + Think_15 ) + Think_41 ) + Think_25 ) + Think_77 ) + Think_96 ) + Think_39 ) + Think_62 ) + Think_85 ) + Think_32 ) + Think_78 ) + Think_24 ) + Think_91 ) + Think_7 ) + Think_18 ) + Think_29 ) + Think_21 ) + Think_73 ) + Think_46 ) + Think_16 ) + Think_51 ) + Think_95 ) + Think_79 ) + Think_89 ) + Think_5 ) + Think_97 ) + Think_81 ) + Think_67 ) + Think_75 ) + Think_65 ) + Think_61 ) + Think_100 ) + Think_43 ) + Think_20 ) + Think_64 ) + Think_37 ) + Think_31 ) + Think_71 ) + Think_35 ) + Think_70 ) + Think_88 ) + Think_83 ) + Think_69 ) + Think_42 ) + Think_72 ) + Think_34 ) + Think_66 ) + Think_80 ) + Think_1 ) + Think_50 ) + Think_28 ) + Think_54 ) + Think_45 ) + Think_84 ) + Think_14 ) + Think_90 ) + Think_3 ) + Think_33 ) + Think_27 ) + Think_47 ) + Think_86 ) + Think_30 ) + Think_82 ) & ~ [ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Fork_2 + Fork_70 ) + Fork_23 ) + Fork_35 ) + Fork_98 ) + Fork_60 ) + Fork_12 ) + Fork_26 ) + Fork_68 ) + Fork_71 ) + Fork_69 ) + Fork_5 ) + Fork_95 ) + Fork_91 ) + Fork_73 ) + Fork_62 ) + Fork_100 ) + Fork_67 ) + Fork_15 ) + Fork_13 ) + Fork_25 ) + Fork_53 ) + Fork_52 ) + Fork_97 ) + Fork_51 ) + Fork_36 ) + Fork_33 ) + Fork_1 ) + Fork_82 ) + Fork_87 ) + Fork_88 ) + Fork_39 ) + Fork_27 ) + Fork_6 ) + Fork_72 ) + Fork_14 ) + Fork_9 ) + Fork_74 ) + Fork_80 ) + Fork_21 ) + Fork_56 ) + Fork_48 ) + Fork_11 ) + Fork_63 ) + Fork_99 ) + Fork_96 ) + Fork_50 ) + Fork_59 ) + Fork_40 ) + Fork_17 ) + Fork_83 ) + Fork_85 ) + Fork_65 ) + Fork_54 ) + Fork_44 ) + Fork_76 ) + Fork_84 ) + Fork_55 ) + Fork_93 ) + Fork_7 ) + Fork_34 ) + Fork_32 ) + Fork_86 ) + Fork_58 ) + Fork_4 ) + Fork_46 ) + Fork_24 ) + Fork_47 ) + Fork_78 ) + Fork_22 ) + Fork_16 ) + Fork_90 ) + Fork_57 ) + Fork_43 ) + Fork_77 ) + Fork_89 ) + Fork_94 ) + Fork_42 ) + Fork_3 ) + Fork_30 ) + Fork_79 ) + Fork_45 ) + Fork_37 ) + Fork_38 ) + Fork_10 ) + Fork_61 ) + Fork_64 ) + Fork_8 ) + Fork_41 ) + Fork_49 ) + Fork_31 ) + Fork_29 ) + Fork_19 ) + Fork_81 ) + Fork_92 ) + Fork_18 ) + Fork_20 ) + Fork_75 ) + Fork_66 ) + Fork_28 ) <= ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( Eat_68 + Eat_7 ) + Eat_44 ) + Eat_59 ) + Eat_39 ) + Eat_12 ) + Eat_16 ) + Eat_37 ) + Eat_92 ) + Eat_89 ) + Eat_94 ) + Eat_74 ) + Eat_14 ) + Eat_82 ) + Eat_30 ) + Eat_96 ) + Eat_21 ) + Eat_38 ) + Eat_86 ) + Eat_76 ) + Eat_22 ) + Eat_26 ) + Eat_18 ) + Eat_72 ) + Eat_95 ) + Eat_100 ) + Eat_19 ) + Eat_55 ) + Eat_27 ) + Eat_81 ) + Eat_62 ) + Eat_77 ) + Eat_93 ) + Eat_25 ) + Eat_28 ) + Eat_90 ) + Eat_15 ) + Eat_11 ) + Eat_41 ) + Eat_65 ) + Eat_58 ) + Eat_83 ) + Eat_43 ) + Eat_29 ) + Eat_88 ) + Eat_61 ) + Eat_79 ) + Eat_73 ) + Eat_49 ) + Eat_69 ) + Eat_24 ) + Eat_32 ) + Eat_34 ) + Eat_54 ) + Eat_20 ) + Eat_23 ) + Eat_75 ) + Eat_47 ) + Eat_46 ) + Eat_42 ) + Eat_1 ) + Eat_60 ) + Eat_53 ) + Eat_48 ) + Eat_9 ) + Eat_70 ) + Eat_71 ) + Eat_51 ) + Eat_6 ) + Eat_98 ) + Eat_31 ) + Eat_97 ) + Eat_8 ) + Eat_13 ) + Eat_17 ) + Eat_2 ) + Eat_52 ) + Eat_66 ) + Eat_10 ) + Eat_91 ) + Eat_84 ) + Eat_87 ) + Eat_56 ) + Eat_78 ) + Eat_80 ) + Eat_5 ) + Eat_45 ) + Eat_57 ) + Eat_63 ) + Eat_64 ) + Eat_33 ) + Eat_99 ) + Eat_40 ) + Eat_3 ) + Eat_35 ) + Eat_50 ) + Eat_4 ) + Eat_85 ) + Eat_36 ) + Eat_67 ) ]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1863_cardinalitycomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m9sec

STOP 1369715707

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

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

initing FirstDep: 0m0sec


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

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

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

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

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

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

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