fof(initial_state,conjecture,p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ).
fof(wrap_hn1k1_hn1k1_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ( p(n1,n1,X1,X2,X3,X4,n1,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) => p(n1,n1,X1,X2,X3,X4,n1,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) ) ).
fof(wrap_hn1k1_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ( p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,n0,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k1_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ( p(n1,n1,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,n0,X24,X25,X26,X27,X28,X29,X30) => p(n1,n1,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k1_hn1k4_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ( p(n1,n1,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n0,X28,X29,X30) => p(n1,n1,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28,X29,X30) ) ).
fof(wrap_hn1k2_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,n0,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k2_hn1k2_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,n1,n1,X2,X3,X4,X5,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,n0,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) => p(Y,X,W,V,U,T,S,n1,n1,X2,X3,X4,X5,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) ) ).
fof(wrap_hn1k2_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,n1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,n0,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,n1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k2_hn1k4_command,conjecture,! [X30] : ! [X29] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,n1,X2,X3,X4,X5,X6,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n0,X29,X30) => p(R,Q,P,O,N,M,L,n1,n1,X2,X3,X4,X5,X6,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1,X29,X30) ) ).
fof(wrap_hn1k3_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,n1,n1,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,n0,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,n1,n1,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k3_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,n1,n1,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,n0,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,n1,n1,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k3_hn1k3_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,n1,n1,X3,X4,X5,X6,n1,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n0,X21,X22,X23,X24,X25) => p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,n1,n1,X3,X4,X5,X6,n1,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25) ) ).
fof(wrap_hn1k3_hn1k4_command,conjecture,! [X30] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X3,X4,X5,X6,X7,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,n0,X30) => p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X3,X4,X5,X6,X7,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,n1,X30) ) ).
fof(wrap_hn1k4_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,n0,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k4_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,K,J,I,H,G,F,E,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,n0,X23,X24,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,K,J,I,H,G,F,E,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(wrap_hn1k4_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X2,X3,X4,X5,X6,n1,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n0,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X2,X3,X4,X5,X6,n1,n1,n1,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28,X29,X30) ) ).
fof(wrap_hn1k4_hn1k4_command,conjecture,! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X4,X5,X6,X7,n1,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0) => p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,n1,X4,X5,X6,X7,n1,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1) ) ).
fof(unwrap_hn1k1_hn1k1_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X0] : ( p(n1,X0,n1,X2,X3,X4,X5,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) => p(n1,X0,n1,X2,X3,X4,n1,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) ) ).
fof(unwrap_hn1k1_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X0] : ( p(n1,X0,n1,X2,X3,X4,X5,n0,X6,X7,X8,X9,X10,X11,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,n1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k1_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X0] : ( p(n1,X0,n1,X2,X3,X4,X5,R,Q,P,O,N,M,L,n0,X7,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,n1,X2,X3,X4,X5,R,Q,P,O,N,M,L,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k1_hn1k4_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X0] : ( p(n1,X0,n1,X2,X3,X4,X5,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n0,X8,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28,X29,X30) => p(n1,X0,n1,X2,X3,X4,X5,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28,X29,X30) ) ).
fof(unwrap_hn1k2_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n0,X0,X1,X2,X3,X4,X5,n1,X6,n1,X8,X9,X10,X11,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,n1,X6,n1,X8,X9,X10,X11,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k2_hn1k2_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,n1,X1,n1,X3,X4,X5,X6,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) => p(Y,X,W,V,U,T,S,n1,X1,n1,X3,X4,X5,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25) ) ).
fof(unwrap_hn1k2_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,X1,n1,X3,X4,X5,X6,n0,X7,X8,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,n1,X3,X4,X5,X6,n1,X7,X8,X9,X10,X11,n1,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k2_hn1k4_command,conjecture,! [X30] : ! [X29] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n1,X1,n1,X3,X4,X5,X6,K,J,I,H,G,F,E,n0,X8,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,n1,X3,X4,X5,X6,K,J,I,H,G,F,E,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1,X29,X30) ) ).
fof(unwrap_hn1k3_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X7] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n0,X0,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,n1,X7,n1,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,n1,X7,n1,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k3_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n0,X1,X2,X3,X4,X5,X6,n1,X7,n1,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,n1,X7,n1,X9,X10,X11,X12,K,J,I,H,G,F,E,D,C,B,A,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k3_hn1k3_command,conjecture,! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,n1,X2,n1,X4,X5,X6,X7,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25) => p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,n1,X2,n1,X4,X5,X6,n1,K,J,I,H,G,F,E,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25) ) ).
fof(unwrap_hn1k3_hn1k4_command,conjecture,! [X30] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X2,n1,X4,X5,X6,X7,n0,X8,X9,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,n1,X30) => p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X2,n1,X4,X5,X6,X7,n1,X8,X9,X10,X11,X12,n1,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,n1,X30) ) ).
fof(unwrap_hn1k4_hn1k1_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n0,X0,X1,X2,X3,X4,X5,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) => p(n1,X0,X1,X2,X3,X4,n1,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k4_hn1k2_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,n0,X1,X2,X3,X4,X5,X6,K,J,I,H,G,F,E,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,n1,X1,X2,X3,X4,X5,n1,K,J,I,H,G,F,E,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k4_hn1k3_command,conjecture,! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ( p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n0,X2,X3,X4,X5,X6,X7,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28,X29,X30) => p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X2,X3,X4,X5,X6,n1,n1,X8,n1,X10,X11,X12,X13,D,C,B,A,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28,X29,X30) ) ).
fof(unwrap_hn1k4_hn1k4_command,conjecture,! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X3] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ( p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X3,n1,X5,X6,X7,X8,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1) => p(Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X3,n1,X5,X6,X7,n1,D,C,B,A,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1) ) ).
fof(set_attr_hn1k1_wrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X5] : ! [X4] : ! [X2] : ( p(n1,n0,n0,X2,n0,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,n1,n0,X2,n0,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k1_unwrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X5] : ! [X4] : ! [X3] : ( p(n1,n0,n0,n0,X3,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,n0,n1,n0,X3,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k1_encrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X5] : ! [X4] : ! [X3] : ( p(n1,n0,n0,n0,X3,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,n0,n0,n1,X3,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k1_decrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ( p(n1,n0,X1,X2,n0,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,n0,X1,X2,n1,X4,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k1_sensitive_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X5] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,X3,n0,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,X0,X1,X2,X3,n1,X5,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_wrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X6] : ! [X5] : ! [X3] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,n0,n0,X3,n0,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,n1,n0,X3,n0,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_unwrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X6] : ! [X5] : ! [X4] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,n0,n0,n0,X4,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,n0,n1,n0,X4,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_encrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X6] : ! [X5] : ! [X4] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,n0,n0,n0,X4,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,n0,n0,n1,X4,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_decrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,n0,X2,X3,n0,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,n0,X2,X3,n1,X5,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_sensitive_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X6] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,X1,X2,X3,X4,n0,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,X1,X2,X3,X4,n1,X6,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_wrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X7] : ! [X6] : ! [X4] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,n0,X4,n0,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n1,n0,X4,n0,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_unwrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X7] : ! [X6] : ! [X5] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,n0,n0,X5,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,n1,n0,X5,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_encrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X7] : ! [X6] : ! [X5] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,n0,n0,X5,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,n0,n1,X5,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_decrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,X3,X4,n0,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,n0,X3,X4,n1,X6,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_sensitive_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X7] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,X2,X3,X4,X5,n0,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,X2,X3,X4,X5,n1,X7,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_wrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X8] : ! [X7] : ! [X5] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,n0,X5,n0,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n1,n0,X5,n0,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_unwrap_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X8] : ! [X7] : ! [X6] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,n0,n0,X6,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,n1,n0,X6,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_encrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X8] : ! [X7] : ! [X6] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,n0,n0,X6,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,n0,n1,X6,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_decrypt_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,X4,X5,n0,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,n0,X4,X5,n1,X7,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_sensitive_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X8] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,X3,X4,X5,X6,n0,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,X3,X4,X5,X6,n1,X8,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k1_extractable_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,X3,X4,n1,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(n1,X0,X1,X2,X3,X4,n0,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k2_extractable_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,n1,X1,X2,X3,X4,X5,n1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,n1,X1,X2,X3,X4,X5,n0,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k3_extractable_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,X2,X3,X4,X5,X6,n1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,n1,X2,X3,X4,X5,X6,n0,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(set_attr_hn1k4_extractable_command,conjecture,! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ! [C1] : ! [D1] : ! [E1] : ! [F1] : ! [G1] : ! [H1] : ! [I1] : ! [J1] : ! [K1] : ! [L1] : ! [M1] : ! [N1] : ! [O1] : ( p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,X3,X4,X5,X6,X7,n1,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) => p(O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,n1,X3,X4,X5,X6,X7,n0,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) ) ).
fof(decrypt_hn1k1_k1Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k1_k2Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n0,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k1_k3Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n0,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k1_k4Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [X0] : ( p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1,X26,X27,X28) => p(n1,X0,X1,X2,n1,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1,X26,X27,X28) ) ).
fof(decrypt_hn1k2_k1Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k2_k2Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n0,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k2_k3Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n0,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k2_k4Enck2_command,conjecture,! [X28] : ! [X27] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,X3,n1,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28) ) ).
fof(decrypt_hn1k3_k1Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,n0,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k3_k2Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,n0,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k3_k3Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,X10,n0,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k3_k4Enck3_command,conjecture,! [X28] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,X10,X11,n0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,X4,n1,X6,X7,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28) ) ).
fof(decrypt_hn1k4_k1Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,n0,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,n1,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k4_k2Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,n0,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k4_k3Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,X10,n0,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28) ) ).
fof(decrypt_hn1k4_k4Enck4_command,conjecture,! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,X10,X11,n0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,X5,n1,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1) ) ).
fof(encrypt_hn1k1_k1Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [X0] : ( p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,n0,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k1_k2Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [X0] : ( p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,n0,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k1_k3Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [X0] : ( p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,n0,X22,X23,X24,X25,X26,X27,X28) => p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k1_k4Enck1_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [X5] : ! [X4] : ! [X3] : ! [X1] : ! [X0] : ( p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n0,X26,X27,X28) => p(n1,X0,X1,n1,X3,X4,X5,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,n1,X26,X27,X28) ) ).
fof(encrypt_hn1k2_k1Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,n0,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k2_k2Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,n0,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k2_k3Enck2_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n0,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k2_k4Enck2_command,conjecture,! [X28] : ! [X27] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [X6] : ! [X5] : ! [X4] : ! [X2] : ! [X1] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n0,X27,X28) => p(U,T,S,R,Q,P,O,n1,X1,X2,n1,X4,X5,X6,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,n1,X27,X28) ) ).
fof(encrypt_hn1k3_k1Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,X14,n0,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,n1,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k3_k2Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,n0,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k3_k3Enck3_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n0,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k3_k4Enck3_command,conjecture,! [X28] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [X7] : ! [X6] : ! [X5] : ! [X3] : ! [X2] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n0,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,n1,X2,X3,n1,X5,X6,X7,G,F,E,D,C,B,A,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,n1,X28) ) ).
fof(encrypt_hn1k4_k1Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,n1,X10,X11,X12,X13,X14,X15,n0,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,n1,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k4_k2Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,n0,X21,X22,X23,X24,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23,X24,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k4_k3Enck4_command,conjecture,! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n0,X25,X26,X27,X28) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,n1,X25,X26,X27,X28) ) ).
fof(encrypt_hn1k4_k4Enck4_command,conjecture,! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [X3] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ( p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n0) => p(U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,n1) ) ).
fof(encrypt_k1Enck1_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X7] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,n0,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,n1,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k2Enck1_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,n1,X6,X7,X8,X9,X10,X11,n0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,n1,X6,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k3Enck1_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,n0,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k4Enck1_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n0,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23) ) ).
fof(encrypt_k1Enck2_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [X7] : ! [X6] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,n1,X6,X7,X8,n0,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,n1,X6,X7,X8,n1,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k2Enck2_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,n0,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k3Enck2_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n0,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k4Enck2_command,conjecture,! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,n0,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23) ) ).
fof(encrypt_k1Enck3_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,n1,X7,X8,X9,n0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,n1,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k2Enck3_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,n1,X7,X8,X9,X10,X11,X12,X13,n0,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,n1,X7,X8,X9,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k3Enck3_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,n0,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k4Enck3_command,conjecture,! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n0,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23) ) ).
fof(encrypt_k1Enck4_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,n1,X8,X9,X10,n0,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,n1,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k2Enck4_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,n1,X8,X9,X10,X11,X12,X13,X14,n0,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,n1,X8,X9,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(encrypt_k3Enck4_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,n0,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23) ) ).
fof(encrypt_k4Enck4_command,conjecture,! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n0) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1) ) ).
fof(intruder_decrypt_k1Enck1_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X7] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,n1,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,n1,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k2Enck1_command,conjecture,! [X4] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,n0,X6,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,n1,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k3Enck1_command,conjecture,! [X4] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,n1,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k4Enck1_command,conjecture,! [X4] : ! [X23] : ! [X22] : ! [X21] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,n0,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,n1,X21,X22,X23) ) ).
fof(intruder_decrypt_k1Enck2_command,conjecture,! [X5] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X8] : ! [X7] : ! [X6] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,n1,X6,X7,X8,n1,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,X8,n1,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k2Enck2_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,n1,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k3Enck2_command,conjecture,! [X5] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,n1,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k4Enck2_command,conjecture,! [X5] : ! [X23] : ! [X22] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,n0,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,n1,X22,X23) ) ).
fof(intruder_decrypt_k1Enck3_command,conjecture,! [X6] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,X5,n1,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,X8,X9,n1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k2Enck3_command,conjecture,! [X6] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n0,n1,X7,X8,X9,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,X13,n1,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k3Enck3_command,conjecture,! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,n1,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k4Enck3_command,conjecture,! [X6] : ! [X23] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,n0,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,n1,X23) ) ).
fof(intruder_decrypt_k1Enck4_command,conjecture,! [X7] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,X5,X6,n1,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X5,X6,X7,X8,X9,X10,n1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k2Enck4_command,conjecture,! [X7] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n0,X6,n1,X8,X9,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,n1,X6,X7,X8,X9,X10,X11,X12,X13,X14,n1,X16,X17,X18,X19,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k3Enck4_command,conjecture,! [X7] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n0,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,n1,X20,X21,X22,X23) ) ).
fof(intruder_decrypt_k4Enck4_command,conjecture,! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X6] : ! [X5] : ! [X4] : ! [A] : ! [B] : ! [C] : ! [D] : ! [E] : ! [F] : ! [G] : ! [H] : ! [I] : ! [J] : ! [K] : ! [L] : ! [M] : ! [N] : ! [O] : ! [P] : ! [Q] : ! [R] : ! [S] : ! [T] : ! [U] : ! [V] : ! [W] : ! [X] : ! [Y] : ! [Z] : ! [A1] : ! [B1] : ( p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1) => p(B1,A1,Z,Y,X,W,V,U,T,S,R,Q,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A,X4,X5,X6,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,n1) ) ).
fof(domain_constraints,conjecture,! [X47] : ! [X46] : ! [X45] : ! [X44] : ! [X43] : ! [X42] : ! [X41] : ! [X40] : ! [X39] : ! [X38] : ! [X37] : ! [X36] : ! [X35] : ! [X34] : ! [X33] : ! [X32] : ! [X31] : ! [X30] : ! [X29] : ! [X28] : ! [X27] : ! [X26] : ! [X25] : ! [X24] : ! [X23] : ! [X22] : ! [X21] : ! [X20] : ! [X19] : ! [X18] : ! [X17] : ! [X16] : ! [X15] : ! [X14] : ! [X13] : ! [X12] : ! [X11] : ! [X10] : ! [X9] : ! [X8] : ! [X7] : ! [X6] : ! [X5] : ! [X4] : ! [X3] : ! [X2] : ! [X1] : ! [X0] : ( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47) => ( ( X0 = n1 <~> X0 = n0 ) & ( X1 = n1 <~> X1 = n0 ) & ( X2 = n1 <~> X2 = n0 ) & ( X3 = n1 <~> X3 = n0 ) & ( X4 = n1 <~> X4 = n0 ) & ( X5 = n1 <~> X5 = n0 ) & ( X6 = n1 <~> X6 = n0 ) & ( X7 = n1 <~> X7 = n0 ) & ( X8 = n1 <~> X8 = n0 ) & ( X9 = n1 <~> X9 = n0 ) & ( X10 = n1 <~> X10 = n0 ) & ( X11 = n1 <~> X11 = n0 ) & ( X12 = n1 <~> X12 = n0 ) & ( X13 = n1 <~> X13 = n0 ) & ( X14 = n1 <~> X14 = n0 ) & ( X15 = n1 <~> X15 = n0 ) & ( X16 = n1 <~> X16 = n0 ) & ( X17 = n1 <~> X17 = n0 ) & ( X18 = n1 <~> X18 = n0 ) & ( X19 = n1 <~> X19 = n0 ) & ( X20 = n1 <~> X20 = n0 ) & ( X21 = n1 <~> X21 = n0 ) & ( X22 = n1 <~> X22 = n0 ) & ( X23 = n1 <~> X23 = n0 ) & ( X24 = n1 <~> X24 = n0 ) & ( X25 = n1 <~> X25 = n0 ) & ( X26 = n1 <~> X26 = n0 ) & ( X27 = n1 <~> X27 = n0 ) & ( X28 = n1 <~> X28 = n0 ) & ( X29 = n1 <~> X29 = n0 ) & ( X30 = n1 <~> X30 = n0 ) & ( X31 = n1 <~> X31 = n0 ) & ( X32 = n1 <~> X32 = n0 ) & ( X33 = n1 <~> X33 = n0 ) & ( X34 = n1 <~> X34 = n0 ) & ( X35 = n1 <~> X35 = n0 ) & ( X36 = n1 <~> X36 = n0 ) & ( X37 = n1 <~> X37 = n0 ) & ( X38 = n1 <~> X38 = n0 ) & ( X39 = n1 <~> X39 = n0 ) & ( X40 = n1 <~> X40 = n0 ) & ( X41 = n1 <~> X41 = n0 ) & ( X42 = n1 <~> X42 = n0 ) & ( X43 = n1 <~> X43 = n0 ) & ( X44 = n1 <~> X44 = n0 ) & ( X45 = n1 <~> X45 = n0 ) & ( X46 = n1 <~> X46 = n0 ) & ( X47 = n1 <~> X47 = n0 ) ) ) ).
fof(co1,conjecture,~(? [A] : ? [B] : ? [C] : ? [D] : ? [E] : ? [F] : ? [G] : ? [H] : ? [I] : ? [J] : ? [K] : ? [L] : ? [M] : ? [N] : ? [O] : ? [P] : ? [X3] : ? [X2] : ? [X1] : ? [Q] : ? [R] : ? [S] : ? [T] : ? [U] : ? [V] : ? [W] : ? [X] : ? [Y] : ? [Z] : ? [A1] : ? [B1] : ? [C1] : ? [D1] : ? [E1] : ? [F1] : ? [G1] : ? [H1] : ? [I1] : ? [J1] : ? [K1] : ? [L1] : ? [M1] : ? [N1] : ? [O1] : ? [P1] : ? [Q1] : ? [R1] : p(R1,Q1,P1,O1,N1,M1,L1,K1,J1,I1,H1,G1,F1,E1,D1,C1,B1,A1,Z,Y,X,W,V,U,T,S,R,Q,n1,X1,X2,X3,P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A) )).
