(
/****************************************************************/
/* This file is generated with                                  */
/* Lysatool version 2.0      */
/* with the following parameters:
withAttacker          = true
attackerIndex         = "0"
mergeExpressionLabels = true
mergeInputVariables   = false
                                                                */
/****************************************************************/

/****************************************************************/
/* Names and Key Pairs                                          */
/****************************************************************/

N(na_1_1) & 
N(nb_1_1) & 
N(KS_1) & 
N(K_1_1) & 
N(_NDY_) & 
N(_PLUS__MDY_) & KP(_PLUS__MDY_, _MINUS__MDY_) & KP(_MINUS__MDY_, _PLUS__MDY_) &
N(_MINUS__MDY_) & KP(_PLUS__MDY_, _MINUS__MDY_) & KP(_MINUS__MDY_, _PLUS__MDY_) &
N(I_1) & 


/****************************************************************/
/* Non-empty intersection                                       */
/****************************************************************/

(
(A L1. A L2.
	(E U. N(U) & GAMMA(L1,U)  & GAMMA(L2,U))
		=> NEI(L1,L2))&

(A L1. A L2.  
	(E L1_0. E L1_1. E L1_2. E L1_3. E ELL1. E LS1. E L1'.
	 E L2_0. E L2_1. E L2_2. E L2_3. E ELL2. E LS2. E L2'.
		SE3(L1',L1_0, L1_1, L1_2, L1_3, ELL1, LS1) &
		SE3(L2',L2_0, L2_1, L2_2, L2_3, ELL2, LS2) &
		NEI(L1_0, L2_0) & NEI(L1_1, L2_1) & NEI(L1_2, L2_2) & NEI(L1_3, L2_3)&
		GAMMA(L1, L1') &
		GAMMA(L2, L2')) =>
			NEI(L1,L2))
) &

/****************************************************************/
/* Clauses for the process                                      */
/****************************************************************/

(

/* PARALLEL COMPOSITION */
(
/* INDEXED RESTRICTION */

/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* RESTRICTION */
(
/* OUTPUT - length 2 */
1 & GAMMA(LI_1, I_1)
 & GAMMA(Lna_1_1, na_1_1)
 & 
KAPPA2(LI_1, Lna_1_1) & 
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(xa_1_1, L'_1) & REACH(RC32))) & 
(REACH(RC32) => 
/* DECRYPTION - length 3 */
(A L'. RHO(xa_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lxa_1_1, U)))
 & 
D(L9_1_1, s2_1_1) & 
GAMMA(LKS_1, KS_1)
 & 1 & GAMMA(LI_1, I_1)
 & GAMMA(Lna_1_1, na_1_1)
 & 
(A L. A L'_0. A L'_1. A L'_2. A L'_3. A ELL0. A L0S. A L'. 
SE3(L',L'_0, L'_1, L'_2, L'_3, ELL0, L0S) & GAMMA(Lxa_1_1, L') => 
((NEI(L'_0, LKS_1) & NEI(L'_1, LI_1) & NEI(L'_2, Lna_1_1) & 1) => 
RHO(xk_1_1, L'_3) & PQD(L0S, a_1_1, L9_1_1, ELL0) & 
REACH(RC33))) &
(REACH(RC33) => 
/* NIL */
1))))))&
1)&
1) & (
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* INPUT - length 2 */1 & GAMMA(LI_1, I_1)
 & 
(A L'_1. A L'_2. 
KAPPA2(L'_1, L'_2) =>
((NEI(L'_1, LI_1) & 1) => 
RHO(yn_1_1, L'_2) & REACH(RC34))) & 
(REACH(RC34) => 
/* RESTRICTION */
(
/* OUTPUT - length 4 */
1 & GAMMA(LI_1, I_1)
 & GAMMA(LI_1, I_1)
 & (A L'. RHO(yn_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lyn_1_1, U)))
 & GAMMA(Lnb_1_1, nb_1_1)
 & 
KAPPA4(LI_1, LI_1, Lyn_1_1, Lnb_1_1) & 
(
/* INPUT - length 2 */1 & 
(A L'_1. A L'_2. 
KAPPA2(L'_1, L'_2) =>
((1) => 
RHO(yb_1_1, L'_1) & RHO(ya_1_1, L'_2) & REACH(RC35))) & 
(REACH(RC35) => 
/* DECRYPTION - length 3 */
(A L'. RHO(yb_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lyb_1_1, U)))
 & 
D(L20_1_1, s1_1_1) & 
GAMMA(LKS_1, KS_1)
 & 1 & GAMMA(LI_1, I_1)
 & GAMMA(Lnb_1_1, nb_1_1)
 & 
(A L. A L'_0. A L'_1. A L'_2. A L'_3. A ELL0. A L0S. A L'. 
SE3(L',L'_0, L'_1, L'_2, L'_3, ELL0, L0S) & GAMMA(Lyb_1_1, L') => 
((NEI(L'_0, LKS_1) & NEI(L'_1, LI_1) & NEI(L'_2, Lnb_1_1) & 1) => 
RHO(yk_1_1, L'_3) & PQD(L0S, b_1_1, L20_1_1, ELL0) & 
REACH(RC36))) &
(REACH(RC36) => 
/* OUTPUT - length 1 */
1 & (A L'. RHO(ya_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lya_1_1, U)))
 & 
KAPPA1(Lya_1_1) & 
(
/* NIL */
1))))))))&
1)&
1)) & (
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* INPUT - length 4 */1 & GAMMA(LI_1, I_1)
 & GAMMA(LI_1, I_1)
 & 
(A L'_1. A L'_2. A L'_3. A L'_4. 
KAPPA4(L'_1, L'_2, L'_3, L'_4) =>
((NEI(L'_1, LI_1) & NEI(L'_2, LI_1) & 1) => 
RHO(za_1_1, L'_3) & RHO(zb_1_1, L'_4) & REACH(RC37))) & 
(REACH(RC37) => 
/* RESTRICTION */
(
/* OUTPUT - length 2 */
1 & 1 & GAMMA(LKS_1, KS_1)
 & GAMMA(LI_1, I_1)
 & (A L'. RHO(zb_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lzb_1_1, U)))
 & GAMMA(LK_1_1, K_1_1)
 & 
SE3(L30_1_1, LKS_1, LI_1, Lzb_1_1, LK_1_1, s1_1_1, L29_1_1) & 
D(L29_1_1, b_1_1) & GAMMA(L30_1_1, L30_1_1) & 1 & GAMMA(LKS_1, KS_1)
 & GAMMA(LI_1, I_1)
 & (A L'. RHO(za_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lza_1_1, U)))
 & GAMMA(LK_1_1, K_1_1)
 & 
SE3(L36_1_1, LKS_1, LI_1, Lza_1_1, LK_1_1, s2_1_1, L35_1_1) & 
D(L35_1_1, a_1_1) & GAMMA(L36_1_1, L36_1_1) & 
KAPPA2(L30_1_1, L36_1_1) & 
(
/* NIL */
1)))))&
1)&
1)) & (
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC38))) & 
(REACH(RC38) => 
/* OUTPUT - length 1 */
1 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1))) & (
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, _NDY_)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1)) & (
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, _PLUS__MDY_)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1))) & (
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, _MINUS__MDY_)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1))) & (
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, I_1)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1)))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC39))) & 
(REACH(RC39) => 
/* OUTPUT - length 1 */
1 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 
KAPPA1(_L_DY_) & 
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC40))) & 
(REACH(RC40) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC41))) & 
(REACH(RC41) => 
/* OUTPUT - length 4 */
1 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 
KAPPA4(_L_DY_, _L_DY_, _L_DY_, _L_DY_) & 
(
/* INPUT - length 4 */1 & 
(A L'_1. A L'_2. A L'_3. A L'_4. 
KAPPA4(L'_1, L'_2, L'_3, L'_4) =>
((1) => 
RHO(_XDY_, L'_1) & RHO(_XDY_, L'_2) & RHO(_XDY_, L'_3) & RHO(_XDY_, L'_4) & REACH(RC42))) & 
(REACH(RC42) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC43))) & 
(REACH(RC43) => 
/* OUTPUT - length 2 */
1 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 
KAPPA2(_L_DY_, _L_DY_) & 
(
/* INPUT - length 2 */1 & 
(A L'_1. A L'_2. 
KAPPA2(L'_1, L'_2) =>
((1) => 
RHO(_XDY_, L'_1) & RHO(_XDY_, L'_2) & REACH(RC44))) & 
(REACH(RC44) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC45))) & 
(REACH(RC45) => 
/* OUTPUT - length 1 */
1 & 1 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & (A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 
SE3(_L_DY_, _L_DY_, _L_DY_, _L_DY_, _L_DY_, _CPDY_, _L_C_) & 
GAMMA(_L_DY_, _L_DY_) & 
KAPPA1(_L_DY_) & 
(
/* DECRYPTION - length 3 */
(A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 

(A L'. RHO(_XDY_, L') => (A U.  GAMMA(L', U) => GAMMA(_L_DY_, U)))
 & 1 & 
(A L. A L'_0. A L'_1. A L'_2. A L'_3. A ELL0. A L0S. A L'. 
SE3(L',L'_0, L'_1, L'_2, L'_3, ELL0, L0S) & GAMMA(_L_DY_, L') => 
((NEI(L'_0, _L_DY_) & 1) => 
RHO(_XDY_, L'_1) & RHO(_XDY_, L'_2) & RHO(_XDY_, L'_3) & PQD(L0S, _CPDY_, _L_C_, ELL0) & 
REACH(RC46))) &
(REACH(RC46) => 
/* NIL */
1)))))) &

/****************************************************************/
/* Set of all crypto points                                     */
/****************************************************************/

D(_L_C_, s1_1_1) & D(_L_C_, b_1_1) & D(_L_C_, s2_1_1) & D(_L_C_, a_1_1) & D(_L_C_, _CPDY_) & 
/****************************************************************/
/* Pending Queries to PSI                                       */
/****************************************************************/

1) & 
(A L0S. A ELL. A LS. A ELL0. PQD(L0S, ELL, LS, ELL0) => ((!D(L0S, ELL) | !D(LS, ELL0)) => PSI(ELL0, ELL)))