(
/****************************************************************/
/* 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_0_1) & 
N(nb_0_1) & 
N(KS_1) & 
N(KS_0) & 
N(K_0_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_0) & 
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_0, I_0)
 & GAMMA(Lna_0_1, na_0_1)
 & 
KAPPA2(LI_0, Lna_0_1) & 
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(xa_0_1, L'_1) & REACH(RC17))) & 
(REACH(RC17) => 
/* DECRYPTION - length 3 */
(A L'. RHO(xa_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lxa_0_1, U)))
 & 
D(L9_0_1, s2_0_1) & D(L9_0_1, _CPDY_) & 
GAMMA(LKS_0, KS_0)
 & 1 & GAMMA(LI_1, I_1)
 & GAMMA(Lna_0_1, na_0_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_0_1, L') => 
((NEI(L'_0, LKS_0) & NEI(L'_1, LI_1) & NEI(L'_2, Lna_0_1) & 1) => 
RHO(xk_0_1, L'_3) & PQD(L0S, a_0_1, L9_0_1, ELL0) & 
REACH(RC18))) &
(REACH(RC18) => 
/* NIL */
1))))))&
1)&
1) & (
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* INPUT - length 2 */1 & GAMMA(LI_0, I_0)
 & 
(A L'_1. A L'_2. 
KAPPA2(L'_1, L'_2) =>
((NEI(L'_1, LI_0) & 1) => 
RHO(yn_0_1, L'_2) & REACH(RC19))) & 
(REACH(RC19) => 
/* RESTRICTION */
(
/* OUTPUT - length 4 */
1 & GAMMA(LI_0, I_0)
 & GAMMA(LI_1, I_1)
 & (A L'. RHO(yn_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lyn_0_1, U)))
 & GAMMA(Lnb_0_1, nb_0_1)
 & 
KAPPA4(LI_0, LI_1, Lyn_0_1, Lnb_0_1) & 
(
/* INPUT - length 2 */1 & 
(A L'_1. A L'_2. 
KAPPA2(L'_1, L'_2) =>
((1) => 
RHO(yb_0_1, L'_1) & RHO(ya_0_1, L'_2) & REACH(RC20))) & 
(REACH(RC20) => 
/* DECRYPTION - length 3 */
(A L'. RHO(yb_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lyb_0_1, U)))
 & 
D(L20_1_0, s1_0_1) & D(L20_1_0, _CPDY_) & 
GAMMA(LKS_1, KS_1)
 & 1 & GAMMA(LI_0, I_0)
 & GAMMA(Lnb_0_1, nb_0_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_0_1, L') => 
((NEI(L'_0, LKS_1) & NEI(L'_1, LI_0) & NEI(L'_2, Lnb_0_1) & 1) => 
RHO(yk_0_1, L'_3) & PQD(L0S, b_0_1, L20_1_0, ELL0) & 
REACH(RC21))) &
(REACH(RC21) => 
/* OUTPUT - length 1 */
1 & (A L'. RHO(ya_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lya_0_1, U)))
 & 
KAPPA1(Lya_0_1) & 
(
/* NIL */
1))))))))&
1)&
1)) & (
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* INPUT - length 4 */1 & GAMMA(LI_0, I_0)
 & 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_0) & NEI(L'_2, LI_1) & 1) => 
RHO(za_0_1, L'_3) & RHO(zb_0_1, L'_4) & REACH(RC22))) & 
(REACH(RC22) => 
/* RESTRICTION */
(
/* OUTPUT - length 2 */
1 & 1 & GAMMA(LKS_1, KS_1)
 & GAMMA(LI_0, I_0)
 & (A L'. RHO(zb_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lzb_0_1, U)))
 & GAMMA(LK_0_1, K_0_1)
 & 
SE3(L30_0_1, LKS_1, LI_0, Lzb_0_1, LK_0_1, s1_0_1, L29_0_1) & 
D(L29_0_1, b_0_1) & D(L29_0_1, _CPDY_) & GAMMA(L30_0_1, L30_0_1) & 1 & GAMMA(LKS_0, KS_0)
 & GAMMA(LI_1, I_1)
 & (A L'. RHO(za_0_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lza_0_1, U)))
 & GAMMA(LK_0_1, K_0_1)
 & 
SE3(L36_0_1, LKS_0, LI_1, Lza_0_1, LK_0_1, s2_0_1, L35_0_1) & 
D(L35_0_1, a_0_1) & D(L35_0_1, _CPDY_) & GAMMA(L36_0_1, L36_0_1) & 
KAPPA2(L30_0_1, L36_0_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(RC23))) & 
(REACH(RC23) => 
/* 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 */
(
/* 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_0)
 & 
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(RC24))) & 
(REACH(RC24) => 
/* 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(RC25))) & 
(REACH(RC25) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC26))) & 
(REACH(RC26) => 
/* 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(RC27))) & 
(REACH(RC27) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC28))) & 
(REACH(RC28) => 
/* 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(RC29))) & 
(REACH(RC29) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC30))) & 
(REACH(RC30) => 
/* 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(RC31))) &
(REACH(RC31) => 
/* NIL */
1)))))) &

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

D(_L_C_, s1_0_1) & D(_L_C_, b_0_1) & D(_L_C_, s2_0_1) & D(_L_C_, a_0_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)))