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

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

N(n_) & 
N(K_) & 
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(B_) & 
N(A_) & 


/****************************************************************/
/* 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 ELL1. E LS1. E L1'.
	 E L2_0. E L2_1. E ELL2. E LS2. E L2'.
		SE1(L1',L1_0, L1_1, ELL1, LS1) &
		SE1(L2',L2_0, L2_1, ELL2, LS2) &
		NEI(L1_0, L2_0) & NEI(L1_1, L2_1)&
		GAMMA(L1, L1') &
		GAMMA(L2, L2')) =>
			NEI(L1,L2))
) &

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

(

/* PARALLEL COMPOSITION */
(
/* RESTRICTION */
(
/* PARALLEL COMPOSITION */
(
/* REPLICATION */
(
/* RESTRICTION */
(
/* OUTPUT - length 3 */
1 & GAMMA(LA_, A_)
 & GAMMA(LB_, B_)
 & GAMMA(Ln_, n_)
 & 
KAPPA3(LA_, LB_, Ln_) & 
(
/* INPUT - length 3 */1 & GAMMA(LB_, B_)
 & GAMMA(LA_, A_)
 & 
(A L'_1. A L'_2. A L'_3. 
KAPPA3(L'_1, L'_2, L'_3) =>
((NEI(L'_1, LB_) & NEI(L'_2, LA_) & 1) => 
RHO(x_, L'_3) & REACH(RC1))) & 
(REACH(RC1) => 
/* DECRYPTION - length 1 */
(A L'. RHO(x_, L') => (A U.  GAMMA(L', U) => GAMMA(Lx_, U)))
 & 

GAMMA(LK_, K_)
 & 1 & GAMMA(Ln_, n_)
 & 
(A L. A L'_0. A L'_1. A ELL0. A L0S. A L'. 
SE1(L',L'_0, L'_1, ELL0, L0S) & GAMMA(Lx_, L') => 
((NEI(L'_0, LK_) & NEI(L'_1, Ln_) & 1) => 
PQD(L0S, _UCP__, _L_C_, ELL0) & 
REACH(RC2))) &
(REACH(RC2) => 
/* NIL */
1)))))) & (
/* REPLICATION */
(
/* INPUT - length 3 */1 & GAMMA(LA_, A_)
 & GAMMA(LB_, B_)
 & 
(A L'_1. A L'_2. A L'_3. 
KAPPA3(L'_1, L'_2, L'_3) =>
((NEI(L'_1, LA_) & NEI(L'_2, LB_) & 1) => 
RHO(y_, L'_3) & REACH(RC3))) & 
(REACH(RC3) => 
/* OUTPUT - length 3 */
1 & GAMMA(LB_, B_)
 & GAMMA(LA_, A_)
 & 1 & GAMMA(LK_, K_)
 & (A L'. RHO(y_, L') => (A U.  GAMMA(L', U) => GAMMA(Ly_, U)))
 & 
SE1(L17_, LK_, Ly_, _UCP__, _L_C_) & 
GAMMA(L17_, L17_) & 
KAPPA3(LB_, LA_, L17_) & 
(
/* NIL */
1)))))) & (
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC4))) & 
(REACH(RC4) => 
/* 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_, B_)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1))) & (
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, A_)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1)))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC5))) & 
(REACH(RC5) => 
/* OUTPUT - length 3 */
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)))
 & 
KAPPA3(_L_DY_, _L_DY_, _L_DY_) & 
(
/* INPUT - length 3 */1 & 
(A L'_1. A L'_2. A L'_3. 
KAPPA3(L'_1, L'_2, L'_3) =>
((1) => 
RHO(_XDY_, L'_1) & RHO(_XDY_, L'_2) & RHO(_XDY_, L'_3) & REACH(RC6))) & 
(REACH(RC6) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC7))) & 
(REACH(RC7) => 
/* 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)))
 & 
SE1(_L_DY_, _L_DY_, _L_DY_, _CPDY_, _L_C_) & 
GAMMA(_L_DY_, _L_DY_) & 
KAPPA1(_L_DY_) & 
(
/* DECRYPTION - length 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)))
 & 1 & 
(A L. A L'_0. A L'_1. A ELL0. A L0S. A L'. 
SE1(L',L'_0, L'_1, ELL0, L0S) & GAMMA(_L_DY_, L') => 
((NEI(L'_0, _L_DY_) & 1) => 
RHO(_XDY_, L'_1) & PQD(L0S, _CPDY_, _L_C_, ELL0) & 
REACH(RC8))) &
(REACH(RC8) => 
/* NIL */
1)))))) &

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

D(_L_C_, _UCP__) & 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)))