(
/****************************************************************/
/* 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_1_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(B_1) & 
N(A_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 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 */
(
/* INDEXED RESTRICTION */

/* PARALLEL COMPOSITION */
(
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* RESTRICTION */
(
/* OUTPUT - length 3 */
1 & GAMMA(LA_1, A_1)
 & GAMMA(LB_1, B_1)
 & GAMMA(Ln_1_1, n_1_1)
 & 
KAPPA3(LA_1, LB_1, Ln_1_1) & 
(
/* INPUT - length 3 */1 & GAMMA(LB_1, B_1)
 & GAMMA(LA_1, A_1)
 & 
(A L'_1. A L'_2. A L'_3. 
KAPPA3(L'_1, L'_2, L'_3) =>
((NEI(L'_1, LB_1) & NEI(L'_2, LA_1) & 1) => 
RHO(x_1_1, L'_3) & REACH(RC9))) & 
(REACH(RC9) => 
/* DECRYPTION - length 1 */
(A L'. RHO(x_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Lx_1_1, U)))
 & 

GAMMA(LK_1_1, K_1_1)
 & 1 & GAMMA(Ln_1_1, n_1_1)
 & 
(A L. A L'_0. A L'_1. A ELL0. A L0S. A L'. 
SE1(L',L'_0, L'_1, ELL0, L0S) & GAMMA(Lx_1_1, L') => 
((NEI(L'_0, LK_1_1) & NEI(L'_1, Ln_1_1) & 1) => 
PQD(L0S, _UCP__, _L_C_, ELL0) & 
REACH(RC10))) &
(REACH(RC10) => 
/* NIL */
1))))))&
1)&
1) & (
/* INDEXED PARALLEL */
(
/* INDEXED PARALLEL */
(
/* REPLICATION */
(
/* INPUT - length 3 */1 & GAMMA(LA_1, A_1)
 & GAMMA(LB_1, B_1)
 & 
(A L'_1. A L'_2. A L'_3. 
KAPPA3(L'_1, L'_2, L'_3) =>
((NEI(L'_1, LA_1) & NEI(L'_2, LB_1) & 1) => 
RHO(y_1_1, L'_3) & REACH(RC11))) & 
(REACH(RC11) => 
/* OUTPUT - length 3 */
1 & GAMMA(LB_1, B_1)
 & GAMMA(LA_1, A_1)
 & 1 & GAMMA(LK_1_1, K_1_1)
 & (A L'. RHO(y_1_1, L') => (A U.  GAMMA(L', U) => GAMMA(Ly_1_1, U)))
 & 
SE1(L17_1_1, LK_1_1, Ly_1_1, _UCP__, _L_C_) & 
GAMMA(L17_1_1, L17_1_1) & 
KAPPA3(LB_1, LA_1, L17_1_1) & 
(
/* NIL */
1))))&
1)&
1)) & (
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* PARALLEL COMPOSITION */
(
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC12))) & 
(REACH(RC12) => 
/* 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_1)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1))) & (
/* OUTPUT - length 1 */
1 & GAMMA(_L_DY_, A_1)
 & 
KAPPA1(_L_DY_) & 
(
/* NIL */
1)))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC13))) & 
(REACH(RC13) => 
/* 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(RC14))) & 
(REACH(RC14) => 
/* NIL */
1))))) & (
/* INPUT - length 1 */1 & 
(A L'_1. 
KAPPA1(L'_1) =>
((1) => 
RHO(_XDY_, L'_1) & REACH(RC15))) & 
(REACH(RC15) => 
/* 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(RC16))) &
(REACH(RC16) => 
/* 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)))