%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWV010-1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jun 25 02:14:51 EDT 2024 % Result : Unknown 0.42s 0.59s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV010-1 : TPTP v8.2.0. Released v2.4.0. % 0.07/0.12 % Command : run_zenon_modulo %d %s % 0.12/0.33 % Computer : n012.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 20:59:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.42/0.59 Zenon error: exhausted search space without finding a proof % 0.42/0.59 (* Current branch: % 0.42/0.59 (-. (message (sent zenon_X6 (b) (pair zenon_X6 zenon_X7)))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82)) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at)))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X71 (b))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88))) % 0.42/0.59 ((bt) != zenon_X38) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt))))) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5)) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((an_a_nonce) != zenon_X33) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93)) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) (an_a_nonce) zenon_X41)) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94)) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82))) % 0.42/0.59 ((b) != (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75)) % 0.42/0.59 ((key (at) (a)) != (key zenon_X42 (b))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent zenon_X6 (b) (pair zenon_X6 zenon_X7))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (pair zenon_X6 zenon_X7)) % 0.42/0.59 ((b) != (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt))))) % 0.42/0.59 ((bt) != zenon_X68) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (message (sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt)))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86)) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80))) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 (fresh_to_b (an_a_nonce)) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X64 (b))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5)) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5)) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X75) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((b) != (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 (-. (t_holds (key zenon_X30 (b)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (a) (t) (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X71 (b))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (a) (t) (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (a) (t) (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at))))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89)) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt)))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X80) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (t_holds (key zenon_X19 (a)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X73 (a))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88))) % 0.42/0.59 ((a) != zenon_X22) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80))) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (t_holds (key zenon_X53 zenon_X48))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt)))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X93) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X80) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X42 (b))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80)) % 0.42/0.59 ((pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))) != (pair (a) zenon_X29)) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))))) % 0.42/0.59 ((bt) != zenon_X56) % 0.42/0.59 ((an_a_nonce) != zenon_X7) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5))) % 0.42/0.59 (-. (t_holds (key zenon_X25 (b)))) % 0.42/0.59 (-. (t_holds (key zenon_X71 (b)))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X94) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91)) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X19 (a))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (pair zenon_X6 (an_a_nonce))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X84) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt)))))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X24) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80)))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X64 (b))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X92) % 0.42/0.59 ((bt) != zenon_X30) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X88) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))))) % 0.42/0.59 ((pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))) != (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at)))) % 0.42/0.59 ((an_a_nonce) != zenon_X54) % 0.42/0.59 ((bt) != zenon_X60) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3)) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 (message (sent (a) (b) (pair (a) (an_a_nonce)))) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (pair (a) zenon_X29)) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt)))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93)) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X86) % 0.42/0.59 (-. (t_holds (key zenon_X35 (b)))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X38 (b))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86))) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 (-. (t_holds (key zenon_X56 (b)))) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent zenon_X6 (b) (pair zenon_X6 zenon_X7))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt)))) % 0.42/0.59 (message (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X88) % 0.42/0.59 ((key (at) (a)) != (key zenon_X60 (b))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))) % 0.42/0.59 ((bt) != zenon_X64) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X86) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X13 zenon_X8)) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X35 (b))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X25 (b))) % 0.42/0.59 ((an_a_nonce) != (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple zenon_X22 zenon_X23 zenon_X24)) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75)) % 0.42/0.59 ((key (at) (a)) != (key zenon_X68 (b))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))))) % 0.42/0.59 ((bt) != zenon_X45) % 0.42/0.59 ((b) != (a)) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (a) (b) (pair (a) zenon_X29))) % 0.42/0.59 ((a) != zenon_X48) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X51 (b))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent zenon_X6 (b) (pair zenon_X6 zenon_X7))) % 0.42/0.59 ((b) != zenon_X48) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt)))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X5) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt)))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt))))) % 0.42/0.59 ((bt) != zenon_X71) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82)) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))) != zenon_X29) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt)))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X75) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (t_holds (key zenon_X42 (b)))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X67) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X3) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((an_a_nonce) != zenon_X29) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94)) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((at) != zenon_X19) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((b) != zenon_X8) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X91) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt)))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt)))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X21) % 0.42/0.59 ((key (at) (a)) != (key zenon_X56 (b))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt)))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (a) (b) (pair (a) zenon_X29))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) zenon_X54 zenon_X55)) % 0.42/0.59 ((at) != zenon_X73) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 (-. (t_holds (key zenon_X73 (a)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent zenon_X6 (b) (pair zenon_X6 (an_a_nonce)))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) zenon_X33 zenon_X34) (bt))) % 0.42/0.59 ((b) != (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 (-. (message (sent zenon_X6 (b) (pair zenon_X6 (an_a_nonce))))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X13 zenon_X8)) % 0.42/0.59 ((key (at) (a)) != (key zenon_X45 (b))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88)) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt)))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80)) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) zenon_X33 zenon_X34) (bt))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X82) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94))) % 0.42/0.59 ((an_a_nonce) != zenon_X76) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent zenon_X6 (b) (pair zenon_X6 (an_a_nonce)))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (a) zenon_X54 zenon_X55) (bt))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X38 (b))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) (an_a_nonce) zenon_X67)) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != zenon_X5) % 0.42/0.59 ((key (at) (a)) != (key zenon_X51 (b))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((pair (a) (an_a_nonce)) != (pair zenon_X6 (an_a_nonce))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (a) (t) (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at))))) % 0.42/0.59 (-. (message (sent (a) (b) (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt))))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X82) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X34) % 0.42/0.59 (-. (message (sent (a) (b) (pair (a) zenon_X29)))) % 0.42/0.59 (a_stored (pair (b) (an_a_nonce))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (t_holds (key zenon_X51 (b)))) % 0.42/0.59 ((b) != (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at))) % 0.42/0.59 (t_holds (key (bt) (b))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X19 (a))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 zenon_X82))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple (b) zenon_X76 zenon_X77 zenon_X78)) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X68 (b))) % 0.42/0.59 ((b) != zenon_X0) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (a) (b) (pair (a) zenon_X29))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X30 (b))) % 0.42/0.59 ((pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))) != (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) % 0.42/0.59 (-. (t_holds (key zenon_X60 (b)))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((generate_key (an_a_nonce)) != zenon_X83) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent zenon_X6 (b) (pair zenon_X6 zenon_X7))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X45 (b))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X30 (b))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple (b) zenon_X58 zenon_X59) (bt))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88)) % 0.42/0.59 ((encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) != (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 ((bt) != zenon_X42) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) != (a)) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86)) % 0.42/0.59 ((a) != zenon_X6) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X53 zenon_X48)) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X73 (a))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91)) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5))) % 0.42/0.59 ((a) != zenon_X8) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X93) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X56 (b))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (pair zenon_X6 zenon_X7)) % 0.42/0.59 (-. (t_holds (key zenon_X64 (b)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (a) (b) (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt)))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((b) != (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 zenon_X93))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X60 (b))) % 0.42/0.59 ((encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)) != zenon_X91) % 0.42/0.59 ((b) != (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 (-. (message (sent (a) (t) (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at)))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 zenon_X55) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (a) (b) (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))))) % 0.42/0.59 ((key (bt) (b)) != (key zenon_X53 zenon_X48)) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (t_holds (key (at) (a))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (b) zenon_X58 zenon_X59) (bt))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (a) (b) (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (a) zenon_X15 (encrypt (triple zenon_X16 zenon_X17 zenon_X18) (at)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91))) % 0.42/0.59 ((bt) != zenon_X35) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X89) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) zenon_X33 zenon_X34)) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 zenon_X91))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) zenon_X54 zenon_X55) (bt))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 (generate_expiration_time (an_a_nonce))) (at)) zenon_X81 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X78) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple zenon_X22 zenon_X23 zenon_X24) (bt))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (a) (b) (pair (a) zenon_X29))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 zenon_X5)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at)) zenon_X4 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (t_holds (key zenon_X38 (b)))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 zenon_X88)))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 zenon_X34) (bt))))) % 0.42/0.59 ((sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 zenon_X80))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) zenon_X67) (bt))))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84) (at)) zenon_X85 zenon_X86))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) zenon_X92 (generate_b_nonce (an_a_nonce)))))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent zenon_X6 (b) (pair zenon_X6 (an_a_nonce)))) % 0.42/0.59 ((generate_b_nonce (an_a_nonce)) != (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X25 (b))) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) zenon_X89) (at)) zenon_X90 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((bt) != zenon_X51) % 0.42/0.59 (-. (message (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94)))) % 0.42/0.59 (-. (t_holds (key zenon_X13 zenon_X8))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X41) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) zenon_X54 (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((b) != (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 zenon_X3) (at))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent zenon_X6 (b) (pair zenon_X6 (an_a_nonce)))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (b) zenon_X58 zenon_X59) (bt)))))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 (-. (t_holds (key zenon_X45 (b)))) % 0.42/0.59 ((sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce)))) != (sent (t) (a) (triple (encrypt (quadruple (b) zenon_X76 zenon_X77 zenon_X78) (at)) zenon_X79 (generate_b_nonce (an_a_nonce))))) % 0.42/0.59 ((key (at) (a)) != (key zenon_X35 (b))) % 0.42/0.59 ((bt) != zenon_X25) % 0.42/0.59 (-. (t_holds (key zenon_X68 (b)))) % 0.42/0.59 (-. (message (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple zenon_X22 zenon_X23 (generate_expiration_time (an_a_nonce))) (bt)))))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (t) (a) (triple (encrypt (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce))) (at)) zenon_X74 zenon_X75))) % 0.42/0.59 ((sent (a) (b) (pair (a) (an_a_nonce))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (t) (a) (triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) zenon_X94))) % 0.42/0.59 ((triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) != (triple (b) zenon_X58 zenon_X59)) % 0.42/0.59 ((triple (b) (generate_b_nonce (an_a_nonce)) (encrypt (triple (a) (an_a_nonce) (generate_expiration_time (an_a_nonce))) (bt))) != (triple (b) zenon_X21 (encrypt (triple (a) zenon_X33 (generate_expiration_time (an_a_nonce))) (bt)))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple (b) (an_a_nonce) zenon_X83 zenon_X84)) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (a) (b) (pair (a) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce)))))) % 0.42/0.59 ((sent (a) (b) (pair (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (encrypt (generate_b_nonce (an_a_nonce)) (generate_key (an_a_nonce))))) != (sent (b) (t) (triple (b) zenon_X21 (encrypt (triple (a) (an_a_nonce) zenon_X41) (bt))))) % 0.42/0.59 ((triple (encrypt (quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (at)) (encrypt (triple (a) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) (bt)) (generate_b_nonce (an_a_nonce))) != (triple (encrypt (quadruple (b) (an_a_nonce) zenon_X83 (generate_expiration_time (an_a_nonce))) (at)) zenon_X87 (generate_b_nonce (an_a_nonce)))) % 0.42/0.59 ((quadruple (b) (an_a_nonce) (generate_key (an_a_nonce)) (generate_expiration_time (an_a_nonce))) != (quadruple zenon_X0 zenon_X1 zenon_X2 (generate_expiration_time (an_a_nonce)))) % 0.42/0.59 ((generate_expiration_time (an_a_nonce)) != zenon_X55) % 0.42/0.59 *) % 0.42/0.59 (* NO-PROOF *) % 0.42/0.59 % SZS status GaveUp % 0.42/0.59 Number of rewrites on terms: 0 % 0.42/0.59 Number of rewrites on props: 0 % 0.42/0.59 nodes searched: 842 % 0.42/0.59 max branch formulas: 602 % 0.42/0.59 proof nodes created: 82 % 0.42/0.59 formulas created: 5157 % 0.42/0.59 %------------------------------------------------------------------------------