%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW969+1 : TPTP v9.0.0. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n016.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 : Wed Apr 9 09:53:34 PM UTC 2025
% Result : CounterSatisfiable 7.95s 2.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW969+1 : TPTP v9.0.0. Released v7.4.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n016.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 06:49:08 EDT 2025
% 0.14/0.34 % CPUTime :
% 7.95/2.77
% 7.95/2.77 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.95/2.77
% 7.95/2.77 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.95/2.78 %$ pred_mess > pred_equal > pred_eq_bitstring_bitstring > pred_attacker > constr_cbc_enc_4 > tuple_4 > constr_cbc_enc_3 > tuple_server_S_in_1 > tuple_client_A_out_1 > tuple_3 > constr_cbc_enc_2 > tuple_2 > constr_cbc_enc_1 > constr_cbc_dec_4 > constr_cbc_dec_3 > constr_cbc_dec_2 > constr_cbc_dec_1 > #nlpp > tuple_succ > tuple_server_S_out_2 > tuple_client_B_out_2 > tuple_client_B_in_3 > tuple_client_B_in_1 > tuple_client_A_out_5 > tuple_client_A_out_3 > tuple_client_A_in_4 > tuple_client_A_in_2 > name_new0x2Dname > name_Nb_62 > name_Na > name_Kab_65 > constr_tuple_4_get_3_bitstring > constr_tuple_4_get_2_bitstring > constr_tuple_4_get_1 > constr_tuple_4_get_0x30 > constr_tuple_2_get_1 > constr_tuple_2_get_0x30_bitstring > constr_cbc_4_get_3_prefixes > constr_cbc_4_get_2_prefixes > constr_cbc_4_get_1_prefixes > constr_cbc_3_get_2_prefixes > constr_cbc_3_get_1_prefixes > constr_cbc_2_get_1_prefixes > tuple_true > tuple_false > name_c > name_Kbs > name_Kas > name_I > name_B > name_A > constr_CONST_4 > constr_CONST_3 > constr_CONST_2 > constr_CONST_1 > constr_CONST_0x30 > #skF_1
% 7.95/2.78
% 7.95/2.78 %Foreground sorts:
% 7.95/2.78
% 7.95/2.78
% 7.95/2.78 %Background operators:
% 7.95/2.78
% 7.95/2.78
% 7.95/2.78 %Foreground operators:
% 7.95/2.78 tff(tuple_client_A_in_2, type, tuple_client_A_in_2: $i > $i).
% 7.95/2.78 tff(tuple_server_S_out_2, type, tuple_server_S_out_2: $i > $i).
% 7.95/2.78 tff(name_I, type, name_I: $i).
% 7.95/2.78 tff(pred_mess, type, pred_mess: ($i * $i) > $o).
% 7.95/2.78 tff(name_c, type, name_c: $i).
% 7.95/2.78 tff(pred_equal, type, pred_equal: ($i * $i) > $o).
% 7.95/2.78 tff(constr_tuple_4_get_2_bitstring, type, constr_tuple_4_get_2_bitstring: $i > $i).
% 7.95/2.78 tff(tuple_client_A_out_3, type, tuple_client_A_out_3: $i > $i).
% 7.95/2.78 tff(constr_cbc_4_get_2_prefixes, type, constr_cbc_4_get_2_prefixes: $i > $i).
% 7.95/2.78 tff(constr_cbc_4_get_3_prefixes, type, constr_cbc_4_get_3_prefixes: $i > $i).
% 7.95/2.78 tff(constr_cbc_dec_3, type, constr_cbc_dec_3: ($i * $i) > $i).
% 7.95/2.78 tff(constr_CONST_2, type, constr_CONST_2: $i).
% 7.95/2.78 tff(constr_cbc_dec_4, type, constr_cbc_dec_4: ($i * $i) > $i).
% 7.95/2.78 tff(constr_cbc_enc_1, type, constr_cbc_enc_1: ($i * $i) > $i).
% 7.95/2.78 tff(tuple_client_B_out_2, type, tuple_client_B_out_2: $i > $i).
% 7.95/2.78 tff(name_A, type, name_A: $i).
% 7.95/2.78 tff(pred_attacker, type, pred_attacker: $i > $o).
% 7.95/2.78 tff(tuple_false, type, tuple_false: $i).
% 7.95/2.78 tff(constr_tuple_4_get_3_bitstring, type, constr_tuple_4_get_3_bitstring: $i > $i).
% 7.95/2.78 tff(constr_cbc_dec_1, type, constr_cbc_dec_1: ($i * $i) > $i).
% 7.95/2.78 tff(constr_tuple_2_get_1, type, constr_tuple_2_get_1: $i > $i).
% 7.95/2.78 tff(name_B, type, name_B: $i).
% 7.95/2.78 tff(constr_tuple_2_get_0x30_bitstring, type, constr_tuple_2_get_0x30_bitstring: $i > $i).
% 7.95/2.78 tff(tuple_server_S_in_1, type, tuple_server_S_in_1: ($i * $i * $i) > $i).
% 7.95/2.78 tff(name_Kas, type, name_Kas: $i).
% 7.95/2.78 tff(constr_CONST_4, type, constr_CONST_4: $i).
% 7.95/2.78 tff('#skF_1', type, '#skF_1': $i).
% 7.95/2.78 tff(tuple_client_A_out_5, type, tuple_client_A_out_5: $i > $i).
% 7.95/2.78 tff(constr_cbc_enc_4, type, constr_cbc_enc_4: ($i * $i * $i * $i * $i) > $i).
% 7.95/2.78 tff(constr_cbc_3_get_1_prefixes, type, constr_cbc_3_get_1_prefixes: $i > $i).
% 7.95/2.78 tff(constr_cbc_enc_3, type, constr_cbc_enc_3: ($i * $i * $i * $i) > $i).
% 7.95/2.78 tff(constr_cbc_dec_2, type, constr_cbc_dec_2: ($i * $i) > $i).
% 7.95/2.78 tff(name_Na, type, name_Na: $i > $i).
% 7.95/2.78 tff(constr_cbc_4_get_1_prefixes, type, constr_cbc_4_get_1_prefixes: $i > $i).
% 7.95/2.78 tff(tuple_2, type, tuple_2: ($i * $i) > $i).
% 7.95/2.78 tff(tuple_client_B_in_1, type, tuple_client_B_in_1: $i > $i).
% 7.95/2.78 tff(constr_cbc_2_get_1_prefixes, type, constr_cbc_2_get_1_prefixes: $i > $i).
% 7.95/2.78 tff(constr_CONST_0x30, type, constr_CONST_0x30: $i).
% 7.95/2.78 tff(constr_tuple_4_get_1, type, constr_tuple_4_get_1: $i > $i).
% 7.95/2.78 tff(name_Kbs, type, name_Kbs: $i).
% 7.95/2.78 tff(constr_cbc_3_get_2_prefixes, type, constr_cbc_3_get_2_prefixes: $i > $i).
% 7.95/2.78 tff(name_Nb_62, type, name_Nb_62: $i > $i).
% 7.95/2.78 tff(constr_CONST_3, type, constr_CONST_3: $i).
% 7.95/2.78 tff(constr_CONST_1, type, constr_CONST_1: $i).
% 7.95/2.78 tff(tuple_client_B_in_3, type, tuple_client_B_in_3: $i > $i).
% 7.95/2.78 tff(constr_cbc_enc_2, type, constr_cbc_enc_2: ($i * $i * $i) > $i).
% 7.95/2.78 tff(name_new0x2Dname, type, name_new0x2Dname: $i > $i).
% 7.95/2.78 tff(constr_tuple_4_get_0x30, type, constr_tuple_4_get_0x30: $i > $i).
% 7.95/2.78 tff(tuple_client_A_out_1, type, tuple_client_A_out_1: ($i * $i * $i) > $i).
% 7.95/2.78 tff(pred_eq_bitstring_bitstring, type, pred_eq_bitstring_bitstring: ($i * $i) > $o).
% 7.95/2.78 tff(tuple_3, type, tuple_3: ($i * $i * $i) > $i).
% 7.95/2.78 tff(name_Kab_65, type, name_Kab_65: $i > $i).
% 7.95/2.78 tff(tuple_4, type, tuple_4: ($i * $i * $i * $i) > $i).
% 7.95/2.78 tff(tuple_client_A_in_4, type, tuple_client_A_in_4: $i > $i).
% 7.95/2.78 tff(tuple_true, type, tuple_true: $i).
% 7.95/2.78 tff(tuple_succ, type, tuple_succ: $i > $i).
% 7.95/2.78
% 7.95/2.78 %Saturated clause set:
% 7.95/2.78 tff(c_3376, plain, (![VAR_NA_618_463, VAR_B_617_464, VAR_0X40SID_619_465, VAR_A_616_466]: (~pred_attacker(tuple_4(VAR_NA_618_463, VAR_B_617_464, name_Kab_65(VAR_0X40SID_619_465), constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_465), VAR_A_616_466, name_Kbs))) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_466, VAR_B_617_464, VAR_NA_618_463))))).
% 7.95/2.78 tff(c_3367, plain, (![VAR_X0X30_57_668, VAR_X1_58_669, VAR_X2_59_670, VAR_X3_60X30_671]: (~pred_attacker(tuple_4(VAR_X0X30_57_668, VAR_X1_58_669, VAR_X2_59_670, VAR_X3_60X30_671)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_668, VAR_X1_58_669, VAR_X2_59_670, VAR_X3_60X30_671, name_Kas))))).
% 7.95/2.78 tff(c_3342, plain, (![VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5]: (~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(tuple_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5))))).
% 7.95/2.78 tff(c_3352, plain, (![VAR_X2_59_662, VAR_X0X30_57_660, VAR_X1_58_661, VAR_X3_60X30_663]: (~pred_attacker(VAR_X2_59_662) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_660, VAR_X1_58_661, VAR_X2_59_662, VAR_X3_60X30_663, name_Kas))))).
% 7.95/2.78 tff(c_3336, plain, (![VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5]: (~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(VAR_X2_59_4)))).
% 7.95/2.78 tff(c_3337, plain, (![VAR_ENC_NA_B_ENC_KAB_A_490X30_658]: (~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_658)) | ~pred_attacker(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_658, name_Kas))))).
% 7.95/2.78 tff(c_3327, plain, (![VAR_ENC_NA_B_ENC_KAB_A_490X30_657]: (~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_657)) | ~pred_attacker(constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_657, name_Kas)))))).
% 7.95/2.79 tff(c_3205, plain, (![VAR_X0X30_57_603, VAR_X1_58_606, VAR_X3_60X30_605, VAR_X2_59_604, VAR_X0X30_48_607]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_607), VAR_X2_59_604))) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_607, VAR_X2_59_604))) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_603, VAR_X1_58_606, VAR_X2_59_604, VAR_X3_60X30_605, name_Kas))))).
% 7.95/2.79 tff(c_3159, plain, (![VAR_X2_59_4, VAR_X0X30_48_574, VAR_X1_58_3, VAR_X0X30_57_2, VAR_X3_60X30_5]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_574), VAR_X2_59_4))) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_574, VAR_X2_59_4)))))).
% 7.95/2.79 tff(c_1857, plain, (![VAR_X0X30_48_14, VAR_ENC_NA_B_ENC_KAB_A_490X30_497]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_14), constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_497, name_Kas))))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_497)) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_14, constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_497, name_Kas)))))))).
% 7.95/2.79 tff(c_3112, plain, (![VAR_X2_59_556, VAR_X0X30_48_557, VAR_X1_58_559, VAR_X3_60X30_558, VAR_X0X30_57_555]: (pred_attacker(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_557), VAR_X2_59_556)) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_557, VAR_X2_59_556))) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_555, VAR_X1_58_559, VAR_X2_59_556, VAR_X3_60X30_558, name_Kas))))).
% 7.95/2.79 tff(c_2758, plain, (![VAR_X0X30_48_546, VAR_X2_59_4, VAR_X1_58_3, VAR_X0X30_57_2, VAR_X3_60X30_5]: (pred_attacker(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_546), VAR_X2_59_4)) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_546, VAR_X2_59_4)))))).
% 7.95/2.79 tff(c_3101, plain, (![VAR_X0X30_48_14, VAR_0X40SID_619_552]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_14), name_Kab_65(VAR_0X40SID_619_552)))) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_14, name_Kab_65(VAR_0X40SID_619_552))))))).
% 7.95/2.79 tff(c_3093, plain, (![VAR_ENC_NB_489_523, VAR_0X40SID_619_465]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_523, name_Kab_65(VAR_0X40SID_619_465))), name_Kab_65(VAR_0X40SID_619_465)))) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_523))))).
% 7.95/2.79 tff(c_1990, plain, (![VAR_X0X30_48_14, VAR_ENC_NA_B_ENC_KAB_A_490X30_501]: (pred_attacker(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_14), constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_501, name_Kas)))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_501)) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_14, constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_501, name_Kas)))))))).
% 7.95/2.79 tff(c_2742, plain, (![VAR_X0X30_48_14, VAR_0X40SID_619_543]: (pred_attacker(constr_cbc_enc_1(tuple_succ(VAR_X0X30_48_14), name_Kab_65(VAR_0X40SID_619_543))) | ~pred_attacker(tuple_client_A_in_4(constr_cbc_enc_1(VAR_X0X30_48_14, name_Kab_65(VAR_0X40SID_619_543))))))).
% 7.95/2.79 tff(c_2734, plain, (![VAR_ENC_NB_489_535, VAR_0X40SID_619_465]: (pred_attacker(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_535, name_Kab_65(VAR_0X40SID_619_465))), name_Kab_65(VAR_0X40SID_619_465))) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_535))))).
% 7.95/2.79 tff(c_2387, plain, (![VAR_X2_59_528, VAR_X1_58_531, VAR_X0X30_57_527, VAR_ENC_NB_489_529, VAR_X3_60X30_530]: (pred_attacker(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_529, VAR_X2_59_528)), VAR_X2_59_528)) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_529)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_527, VAR_X1_58_531, VAR_X2_59_528, VAR_X3_60X30_530, name_Kas))))).
% 7.95/2.79 tff(c_1993, plain, (![VAR_X2_59_4, VAR_X1_58_3, VAR_X0X30_57_2, VAR_X3_60X30_5, VAR_ENC_NB_489_500]: (pred_attacker(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_500, VAR_X2_59_4)), VAR_X2_59_4)) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_500))))).
% 7.95/2.79 tff(c_2125, plain, (![VAR_X0X30_57_512, VAR_X1_58_516, VAR_ENC_NB_489_513, VAR_X2_59_514, VAR_X3_60X30_515]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_513, VAR_X2_59_514)), VAR_X2_59_514))) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_513)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_512, VAR_X1_58_516, VAR_X2_59_514, VAR_X3_60X30_515, name_Kas))))).
% 7.95/2.79 tff(c_2369, plain, (![VAR_0X40SID_619_508, VAR_V_114_73]: (pred_attacker(tuple_client_A_out_3(constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_508), VAR_V_114_73, name_Kbs))) | ~pred_attacker(VAR_V_114_73)))).
% 7.95/2.79 tff(c_2139, plain, (~pred_attacker(name_Kas))).
% 7.95/2.79 tff(c_2120, plain, (![VAR_V_116_75, VAR_V_115_74, VAR_0X40SID_619_506]: (pred_attacker(constr_cbc_enc_3(VAR_V_116_75, VAR_V_115_74, name_Kab_65(VAR_0X40SID_619_506), name_Kas)) | ~pred_attacker(VAR_V_116_75) | ~pred_attacker(VAR_V_115_74)))).
% 7.95/2.79 tff(c_1859, plain, (![VAR_X2_59_4, VAR_X1_58_3, VAR_X0X30_57_2, VAR_ENC_NB_489_496, VAR_X3_60X30_5]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_496, VAR_X2_59_4)), VAR_X2_59_4))) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, name_Kas))) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_496))))).
% 7.95/2.79 tff(c_879, plain, (![VAR_0X40SID_619_469, VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467]: (pred_attacker(tuple_client_A_out_3(constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_469), VAR_A_616_470, name_Kbs))) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467))))).
% 7.95/2.79 tff(c_877, plain, (![VAR_NA_618_467, VAR_B_617_468, VAR_0X40SID_619_469, VAR_A_616_470]: (pred_attacker(constr_cbc_enc_3(VAR_NA_618_467, VAR_B_617_468, name_Kab_65(VAR_0X40SID_619_469), name_Kas)) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467))))).
% 7.95/2.79 tff(c_1974, plain, (![VAR_0X40SID_549_443, VAR_0X40SID_619_486]: (pred_attacker(tuple_client_B_out_2(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_443), name_Kab_65(VAR_0X40SID_619_486))))))).
% 7.95/2.79 tff(c_1858, plain, (![VAR_ENC_NB_489_496, VAR_ENC_NA_B_ENC_KAB_A_490X30_497]: (pred_attacker(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_496, constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_497, name_Kas)))), constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_497, name_Kas)))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_497)) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_496))))).
% 7.95/2.79 tff(c_1841, plain, (![VAR_0X40SID_549_427, VAR_0X40SID_619_486]: (pred_attacker(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_427), name_Kab_65(VAR_0X40SID_619_486)))))).
% 7.95/2.79 tff(c_308, plain, (![VAR_ENC_NB_489_188, VAR_ENC_NA_B_ENC_KAB_A_490X30_187]: (pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_489_188, constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_187, name_Kas)))), constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_490X30_187, name_Kas))))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_490X30_187)) | ~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_489_188))))).
% 7.95/2.79 tff(c_1466, plain, (![VAR_0X40SID_619_486, VAR_V_114_487]: (~pred_attacker(tuple_2(name_Kab_65(VAR_0X40SID_619_486), VAR_V_114_487)) | ~pred_attacker(VAR_V_114_487)))).
% 7.95/2.79 tff(c_1722, plain, (![VAR_0X40SID_619_486]: (pred_attacker(constr_cbc_enc_1(name_Kab_65(VAR_0X40SID_619_486), name_Kbs))))).
% 7.95/2.79 tff(c_1595, plain, (![VAR_0X40SID_619_486]: (~pred_attacker(name_Kab_65(VAR_0X40SID_619_486))))).
% 7.95/2.79 tff(c_1446, plain, (![VAR_0X40SID_619_482, VAR_V_114_73]: (pred_attacker(constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_482), VAR_V_114_73, name_Kbs)) | ~pred_attacker(VAR_V_114_73)))).
% 7.95/2.79 tff(c_880, plain, (![VAR_0X40SID_619_469, VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467]: (pred_attacker(constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_469), VAR_A_616_470, name_Kbs)) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467))))).
% 7.95/2.79 tff(c_1223, plain, (![VAR_V_116_75, VAR_V_115_74]: (pred_attacker(constr_cbc_enc_2(VAR_V_116_75, VAR_V_115_74, name_Kas)) | ~pred_attacker(VAR_V_116_75) | ~pred_attacker(VAR_V_115_74)))).
% 7.95/2.79 tff(c_1095, plain, (![VAR_V_116_75]: (pred_attacker(constr_cbc_enc_1(VAR_V_116_75, name_Kas)) | ~pred_attacker(VAR_V_116_75)))).
% 7.95/2.79 tff(c_878, plain, (![VAR_NA_618_467, VAR_B_617_468, VAR_A_616_470]: (pred_attacker(constr_cbc_enc_2(VAR_NA_618_467, VAR_B_617_468, name_Kas)) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467))))).
% 7.95/2.79 tff(c_881, plain, (![VAR_NA_618_467, VAR_A_616_470, VAR_B_617_468]: (pred_attacker(constr_cbc_enc_1(VAR_NA_618_467, name_Kas)) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_470, VAR_B_617_468, VAR_NA_618_467))))).
% 7.95/2.79 tff(c_856, plain, (![VAR_NA_618_463, VAR_B_617_464, VAR_0X40SID_619_465, VAR_A_616_466]: (pred_attacker(constr_cbc_enc_4(VAR_NA_618_463, VAR_B_617_464, name_Kab_65(VAR_0X40SID_619_465), constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_465), VAR_A_616_466, name_Kbs), name_Kas)) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_466, VAR_B_617_464, VAR_NA_618_463))))).
% 7.95/2.79 tff(c_300, plain, (![VAR_NA_618_194, VAR_B_617_193, VAR_0X40SID_619_191, VAR_A_616_192]: (pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_618_194, VAR_B_617_193, name_Kab_65(VAR_0X40SID_619_191), constr_cbc_enc_2(name_Kab_65(VAR_0X40SID_619_191), VAR_A_616_192, name_Kbs), name_Kas))) | ~pred_attacker(tuple_server_S_in_1(VAR_A_616_192, VAR_B_617_193, VAR_NA_618_194))))).
% 7.95/2.79 tff(c_729, plain, (![VAR_X1_58_394, VAR_X3_60X30_392, VAR_K_61_393, VAR_X0X30_57_390, VAR_X2_59_391]: (pred_attacker(tuple_4(VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391, VAR_X3_60X30_392)) | ~pred_attacker(VAR_K_61_393) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391, VAR_X3_60X30_392, VAR_K_61_393))))).
% 7.95/2.79 tff(c_687, plain, (![VAR_K_47_386, VAR_X2_45_385, VAR_X0X30_43_387, VAR_X3_46_384, VAR_X1_44_383]: (pred_attacker(constr_cbc_enc_3(VAR_X0X30_43_387, VAR_X1_44_383, VAR_X2_45_385, VAR_K_47_386)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_43_387, VAR_X1_44_383, VAR_X2_45_385, VAR_X3_46_384, VAR_K_47_386))))).
% 7.95/2.79 tff(c_610, plain, (![VAR_X0X30_53_352, VAR_X1_54_353, VAR_X2_55_354, VAR_K_56_355]: (pred_attacker(tuple_3(VAR_X0X30_53_352, VAR_X1_54_353, VAR_X2_55_354)) | ~pred_attacker(VAR_K_56_355) | ~pred_attacker(constr_cbc_enc_3(VAR_X0X30_53_352, VAR_X1_54_353, VAR_X2_55_354, VAR_K_56_355))))).
% 7.95/2.79 tff(c_831, plain, (![VAR_0X40SID_549_443, VAR_X0X30_50X30_444, VAR_X1_51_445]: (pred_attacker(tuple_client_B_out_2(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_443), VAR_X0X30_50X30_444))) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_50X30_444, VAR_X1_51_445, name_Kbs))))).
% 7.95/2.79 tff(c_664, plain, (![VAR_0X40SID_549_371, VAR_X0X30_50X30_11, VAR_X1_51_12]: (pred_attacker(tuple_client_B_out_2(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_371), VAR_X0X30_50X30_11))) | ~pred_attacker(tuple_client_B_in_1(constr_cbc_enc_2(VAR_X0X30_50X30_11, VAR_X1_51_12, name_Kbs)))))).
% 7.95/2.79 tff(c_214, plain, (![VAR_V_221_113, VAR_V_223_115, VAR_V_220X30_112, VAR_V_222_114, VAR_V_219_111]: (pred_attacker(constr_cbc_enc_4(VAR_V_219_111, VAR_V_220X30_112, VAR_V_221_113, VAR_V_222_114, VAR_V_223_115)) | ~pred_attacker(VAR_V_223_115) | ~pred_attacker(VAR_V_222_114) | ~pred_attacker(VAR_V_221_113) | ~pred_attacker(VAR_V_220X30_112) | ~pred_attacker(VAR_V_219_111)))).
% 7.95/2.79 tff(c_635, plain, (![VAR_K_42_360, VAR_X3_41_361, VAR_X1_39_359, VAR_X0X30_38_363, VAR_X2_40X30_362]: (pred_attacker(constr_cbc_enc_2(VAR_X0X30_38_363, VAR_X1_39_359, VAR_K_42_360)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_38_363, VAR_X1_39_359, VAR_X2_40X30_362, VAR_X3_41_361, VAR_K_42_360))))).
% 7.95/2.79 tff(c_801, plain, (![VAR_0X40SID_549_427, VAR_X0X30_50X30_428, VAR_X1_51_429]: (pred_attacker(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_427), VAR_X0X30_50X30_428)) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_50X30_428, VAR_X1_51_429, name_Kbs))))).
% 7.95/2.79 tff(c_680, plain, (![VAR_0X40SID_549_381, VAR_X0X30_50X30_11, VAR_X1_51_12]: (pred_attacker(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_381), VAR_X0X30_50X30_11)) | ~pred_attacker(tuple_client_B_in_1(constr_cbc_enc_2(VAR_X0X30_50X30_11, VAR_X1_51_12, name_Kbs)))))).
% 7.95/2.79 tff(c_252, plain, (![VAR_V_278_139, VAR_V_279_140, VAR_V_280X30_141, VAR_V_281_142]: (pred_attacker(tuple_4(VAR_V_278_139, VAR_V_279_140, VAR_V_280X30_141, VAR_V_281_142)) | ~pred_attacker(VAR_V_281_142) | ~pred_attacker(VAR_V_280X30_141) | ~pred_attacker(VAR_V_279_140) | ~pred_attacker(VAR_V_278_139)))).
% 7.95/2.79 tff(c_778, plain, (![VAR_X3_60X30_415, VAR_X0X30_57_416, VAR_X1_58_417, VAR_X2_59_418]: (pred_attacker(tuple_client_A_out_3(VAR_X3_60X30_415)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_416, VAR_X1_58_417, VAR_X2_59_418, VAR_X3_60X30_415, name_Kas))))).
% 7.95/2.79 tff(c_735, plain, (![VAR_X3_60X30_392, VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391]: (pred_attacker(tuple_client_A_out_3(VAR_X3_60X30_392)) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391, VAR_X3_60X30_392, name_Kas)))))).
% 7.95/2.80 tff(c_767, plain, (![VAR_X0X30_50X30_411, VAR_X1_51_412]: (~pred_attacker(tuple_2(VAR_X0X30_50X30_411, VAR_X1_51_412)) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_50X30_411, VAR_X1_51_412, name_Kbs))))).
% 7.95/2.80 tff(c_708, plain, (![VAR_X0X30_50X30_11, VAR_X1_51_12]: (~pred_attacker(tuple_client_B_in_1(constr_cbc_enc_2(VAR_X0X30_50X30_11, VAR_X1_51_12, name_Kbs))) | ~pred_attacker(tuple_2(VAR_X0X30_50X30_11, VAR_X1_51_12))))).
% 7.95/2.80 tff(c_752, plain, (![VAR_X3_60X30_399, VAR_X0X30_57_400, VAR_X1_58_401, VAR_X2_59_402]: (pred_attacker(VAR_X3_60X30_399) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_57_400, VAR_X1_58_401, VAR_X2_59_402, VAR_X3_60X30_399, name_Kas))))).
% 7.95/2.80 tff(c_216, plain, (![VAR_V_228_116, VAR_V_229_117, VAR_V_230X30_118, VAR_V_231_119]: (pred_attacker(constr_cbc_enc_3(VAR_V_228_116, VAR_V_229_117, VAR_V_230X30_118, VAR_V_231_119)) | ~pred_attacker(VAR_V_231_119) | ~pred_attacker(VAR_V_230X30_118) | ~pred_attacker(VAR_V_229_117) | ~pred_attacker(VAR_V_228_116)))).
% 7.95/2.80 tff(c_734, plain, (![VAR_X3_60X30_392, VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391]: (pred_attacker(VAR_X3_60X30_392) | ~pred_attacker(tuple_client_A_in_2(constr_cbc_enc_4(VAR_X0X30_57_390, VAR_X1_58_394, VAR_X2_59_391, VAR_X3_60X30_392, name_Kas)))))).
% 7.95/2.80 tff(c_741, plain, (![VAR_X0X30_50X30_395, VAR_X1_51_396]: (~pred_attacker(VAR_X0X30_50X30_395) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_50X30_395, VAR_X1_51_396, name_Kbs))))).
% 7.95/2.80 tff(c_702, plain, (![VAR_X0X30_50X30_11, VAR_X1_51_12]: (~pred_attacker(VAR_X0X30_50X30_11) | ~pred_attacker(tuple_client_B_in_1(constr_cbc_enc_2(VAR_X0X30_50X30_11, VAR_X1_51_12, name_Kbs)))))).
% 7.95/2.80 tff(c_112, plain, (![VAR_X2_59_4, VAR_X1_58_3, VAR_K_61_1, VAR_X0X30_57_2, VAR_X3_60X30_5]: (constr_cbc_dec_4(constr_cbc_enc_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5, VAR_K_61_1), VAR_K_61_1)=tuple_4(VAR_X0X30_57_2, VAR_X1_58_3, VAR_X2_59_4, VAR_X3_60X30_5)))).
% 8.32/2.80 tff(c_714, plain, (~pred_attacker(name_Kbs))).
% 8.32/2.80 tff(c_703, plain, (![VAR_ENC_KAB_A_548_388]: (~pred_attacker(tuple_client_B_in_1(VAR_ENC_KAB_A_548_388)) | ~pred_attacker(constr_cbc_dec_2(VAR_ENC_KAB_A_548_388, name_Kbs))))).
% 8.32/2.80 tff(c_693, plain, (![VAR_ENC_KAB_A_548_382]: (~pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A_548_382, name_Kbs))) | ~pred_attacker(tuple_client_B_in_1(VAR_ENC_KAB_A_548_382))))).
% 8.32/2.80 tff(c_120, plain, (![VAR_X1_44_17, VAR_X2_45_18, VAR_X3_46_19, VAR_K_47_15, VAR_X0X30_43_16]: (constr_cbc_4_get_3_prefixes(constr_cbc_enc_4(VAR_X0X30_43_16, VAR_X1_44_17, VAR_X2_45_18, VAR_X3_46_19, VAR_K_47_15))=constr_cbc_enc_3(VAR_X0X30_43_16, VAR_X1_44_17, VAR_X2_45_18, VAR_K_47_15)))).
% 8.32/2.80 tff(c_663, plain, (![VAR_0X40SID_549_371, VAR_ENC_KAB_A_548_372]: (pred_attacker(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_371), constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A_548_372, name_Kbs)))) | ~pred_attacker(tuple_client_B_in_1(VAR_ENC_KAB_A_548_372))))).
% 8.32/2.80 tff(c_548, plain, (![VAR_X0X30_50X30_325, VAR_X1_51_326, VAR_K_52_327]: (pred_attacker(tuple_2(VAR_X0X30_50X30_325, VAR_X1_51_326)) | ~pred_attacker(VAR_K_52_327) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_50X30_325, VAR_X1_51_326, VAR_K_52_327))))).
% 8.32/2.80 tff(c_567, plain, (![VAR_X0X30_33_335, VAR_X2_35_336, VAR_K_37_334, VAR_X1_34_333, VAR_X3_36_337]: (pred_attacker(constr_cbc_enc_1(VAR_X0X30_33_335, VAR_K_37_334)) | ~pred_attacker(constr_cbc_enc_4(VAR_X0X30_33_335, VAR_X1_34_333, VAR_X2_35_336, VAR_X3_36_337, VAR_K_37_334))))).
% 8.32/2.80 tff(c_306, plain, (![VAR_0X40SID_549_189, VAR_ENC_KAB_A_548_190]: (pred_attacker(tuple_client_B_out_2(constr_cbc_enc_1(name_Nb_62(VAR_0X40SID_549_189), constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A_548_190, name_Kbs))))) | ~pred_attacker(tuple_client_B_in_1(VAR_ENC_KAB_A_548_190))))).
% 8.32/2.80 tff(c_579, plain, (![VAR_X0X30_29_338, VAR_X1_30X30_339, VAR_K_32_341, VAR_X2_31_340]: (pred_attacker(constr_cbc_enc_2(VAR_X0X30_29_338, VAR_X1_30X30_339, VAR_K_32_341)) | ~pred_attacker(constr_cbc_enc_3(VAR_X0X30_29_338, VAR_X1_30X30_339, VAR_X2_31_340, VAR_K_32_341))))).
% 8.32/2.80 tff(c_168, plain, (![VAR_V_114_73, VAR_V_115_74, VAR_V_116_75]: (pred_attacker(tuple_server_S_in_1(VAR_V_114_73, VAR_V_115_74, VAR_V_116_75)) | ~pred_attacker(VAR_V_116_75) | ~pred_attacker(VAR_V_115_74) | ~pred_attacker(VAR_V_114_73)))).
% 8.32/2.80 tff(c_122, plain, (![VAR_X2_40X30_23, VAR_X1_39_22, VAR_K_42_20, VAR_X0X30_38_21, VAR_X3_41_24]: (constr_cbc_4_get_2_prefixes(constr_cbc_enc_4(VAR_X0X30_38_21, VAR_X1_39_22, VAR_X2_40X30_23, VAR_X3_41_24, VAR_K_42_20))=constr_cbc_enc_2(VAR_X0X30_38_21, VAR_X1_39_22, VAR_K_42_20)))).
% 8.32/2.80 tff(c_198, plain, (![VAR_V_175_95, VAR_V_176_96, VAR_V_177_97]: (pred_attacker(tuple_client_A_out_1(VAR_V_175_95, VAR_V_176_96, VAR_V_177_97)) | ~pred_attacker(VAR_V_177_97) | ~pred_attacker(VAR_V_176_96) | ~pred_attacker(VAR_V_175_95)))).
% 8.32/2.80 tff(c_114, plain, (![VAR_X0X30_53_7, VAR_X1_54_8, VAR_X2_55_9, VAR_K_56_6]: (constr_cbc_dec_3(constr_cbc_enc_3(VAR_X0X30_53_7, VAR_X1_54_8, VAR_X2_55_9, VAR_K_56_6), VAR_K_56_6)=tuple_3(VAR_X0X30_53_7, VAR_X1_54_8, VAR_X2_55_9)))).
% 8.32/2.80 tff(c_262, plain, (![VAR_V_325_159, VAR_V_326_160, VAR_V_327_161]: (pred_attacker(tuple_3(VAR_V_325_159, VAR_V_326_160, VAR_V_327_161)) | ~pred_attacker(VAR_V_327_161) | ~pred_attacker(VAR_V_326_160) | ~pred_attacker(VAR_V_325_159)))).
% 8.32/2.80 tff(c_218, plain, (![VAR_V_235_120, VAR_V_236_121, VAR_V_237_122]: (pred_attacker(constr_cbc_enc_2(VAR_V_235_120, VAR_V_236_121, VAR_V_237_122)) | ~pred_attacker(VAR_V_237_122) | ~pred_attacker(VAR_V_236_121) | ~pred_attacker(VAR_V_235_120)))).
% 8.32/2.80 tff(c_531, plain, (![VAR_X0X30_25_319, VAR_K_28_322, VAR_X1_26_320, VAR_X2_27_321]: (pred_attacker(constr_cbc_enc_1(VAR_X0X30_25_319, VAR_K_28_322)) | ~pred_attacker(constr_cbc_enc_3(VAR_X0X30_25_319, VAR_X1_26_320, VAR_X2_27_321, VAR_K_28_322))))).
% 8.32/2.80 tff(c_126, plain, (![VAR_X0X30_29_31, VAR_X1_30X30_32, VAR_X2_31_33, VAR_K_32_30]: (constr_cbc_3_get_2_prefixes(constr_cbc_enc_3(VAR_X0X30_29_31, VAR_X1_30X30_32, VAR_X2_31_33, VAR_K_32_30))=constr_cbc_enc_2(VAR_X0X30_29_31, VAR_X1_30X30_32, VAR_K_32_30)))).
% 8.32/2.80 tff(c_124, plain, (![VAR_X1_34_27, VAR_X0X30_33_26, VAR_K_37_25, VAR_X3_36_29, VAR_X2_35_28]: (constr_cbc_4_get_1_prefixes(constr_cbc_enc_4(VAR_X0X30_33_26, VAR_X1_34_27, VAR_X2_35_28, VAR_X3_36_29, VAR_K_37_25))=constr_cbc_enc_1(VAR_X0X30_33_26, VAR_K_37_25)))).
% 8.32/2.80 tff(c_516, plain, (![VAR_X0X30_23_304, VAR_K_0X30_306, VAR_X1_24_305]: (pred_attacker(constr_cbc_enc_1(VAR_X0X30_23_304, VAR_K_0X30_306)) | ~pred_attacker(constr_cbc_enc_2(VAR_X0X30_23_304, VAR_X1_24_305, VAR_K_0X30_306))))).
% 8.32/2.80 tff(c_558, plain, (![VAR_ENC_NA_B_ENC_KAB_A_458_328]: (pred_attacker(constr_tuple_4_get_3_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_458_328, name_Kas))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_458_328))))).
% 8.32/2.80 tff(c_304, plain, (![VAR_ENC_NA_B_ENC_KAB_A_458_185]: (pred_attacker(tuple_client_A_out_3(constr_tuple_4_get_3_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_458_185, name_Kas)))) | ~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_458_185))))).
% 8.32/2.80 tff(c_116, plain, (![VAR_X0X30_50X30_11, VAR_X1_51_12, VAR_K_52_10]: (constr_cbc_dec_2(constr_cbc_enc_2(VAR_X0X30_50X30_11, VAR_X1_51_12, VAR_K_52_10), VAR_K_52_10)=tuple_2(VAR_X0X30_50X30_11, VAR_X1_51_12)))).
% 8.32/2.80 tff(c_504, plain, (![VAR_X0X30_48_14, VAR_K_49_13]: (pred_attacker(VAR_X0X30_48_14) | ~pred_attacker(VAR_K_49_13) | ~pred_attacker(constr_cbc_enc_1(VAR_X0X30_48_14, VAR_K_49_13))))).
% 8.32/2.80 tff(c_128, plain, (![VAR_X0X30_25_35, VAR_X1_26_36, VAR_X2_27_37, VAR_K_28_34]: (constr_cbc_3_get_1_prefixes(constr_cbc_enc_3(VAR_X0X30_25_35, VAR_X1_26_36, VAR_X2_27_37, VAR_K_28_34))=constr_cbc_enc_1(VAR_X0X30_25_35, VAR_K_28_34)))).
% 8.32/2.80 tff(c_258, plain, (![VAR_V_314_153, VAR_V_312_151, VAR_V_313_152, VAR_V_315_154]: (pred_attacker(VAR_V_314_153) | ~pred_attacker(tuple_4(VAR_V_312_151, VAR_V_313_152, VAR_V_314_153, VAR_V_315_154))))).
% 8.32/2.80 tff(c_256, plain, (![VAR_V_30X308_148, VAR_V_30X307_147, VAR_V_30X309_149, VAR_V_310X30_150]: (pred_attacker(VAR_V_30X308_148) | ~pred_attacker(tuple_4(VAR_V_30X307_147, VAR_V_30X308_148, VAR_V_30X309_149, VAR_V_310X30_150))))).
% 8.32/2.80 tff(c_260, plain, (![VAR_V_320X30_158, VAR_V_317_155, VAR_V_318_156, VAR_V_319_157]: (pred_attacker(VAR_V_320X30_158) | ~pred_attacker(tuple_4(VAR_V_317_155, VAR_V_318_156, VAR_V_319_157, VAR_V_320X30_158))))).
% 8.32/2.80 tff(c_130, plain, (![VAR_X0X30_23_39, VAR_X1_24_40, VAR_K_0X30_38]: (constr_cbc_2_get_1_prefixes(constr_cbc_enc_2(VAR_X0X30_23_39, VAR_X1_24_40, VAR_K_0X30_38))=constr_cbc_enc_1(VAR_X0X30_23_39, VAR_K_0X30_38)))).
% 8.32/2.80 tff(c_220, plain, (![VAR_V_240X30_123, VAR_V_241_124]: (pred_attacker(constr_cbc_enc_1(VAR_V_240X30_123, VAR_V_241_124)) | ~pred_attacker(VAR_V_241_124) | ~pred_attacker(VAR_V_240X30_123)))).
% 8.32/2.80 tff(c_222, plain, (![VAR_V_244_125, VAR_V_245_126]: (pred_attacker(constr_cbc_dec_4(VAR_V_244_125, VAR_V_245_126)) | ~pred_attacker(VAR_V_245_126) | ~pred_attacker(VAR_V_244_125)))).
% 8.32/2.80 tff(c_224, plain, (![VAR_V_248_127, VAR_V_249_128]: (pred_attacker(constr_cbc_dec_3(VAR_V_248_127, VAR_V_249_128)) | ~pred_attacker(VAR_V_249_128) | ~pred_attacker(VAR_V_248_127)))).
% 8.32/2.80 tff(c_226, plain, (![VAR_V_252_129, VAR_V_253_130]: (pred_attacker(constr_cbc_dec_2(VAR_V_252_129, VAR_V_253_130)) | ~pred_attacker(VAR_V_253_130) | ~pred_attacker(VAR_V_252_129)))).
% 8.32/2.80 tff(c_254, plain, (![VAR_V_30X302_143, VAR_V_30X303_144, VAR_V_30X304_145, VAR_V_30X305_146]: (pred_attacker(VAR_V_30X302_143) | ~pred_attacker(tuple_4(VAR_V_30X302_143, VAR_V_30X303_144, VAR_V_30X304_145, VAR_V_30X305_146))))).
% 8.32/2.80 tff(c_228, plain, (![VAR_V_256_131, VAR_V_257_132]: (pred_attacker(constr_cbc_dec_1(VAR_V_256_131, VAR_V_257_132)) | ~pred_attacker(VAR_V_257_132) | ~pred_attacker(VAR_V_256_131)))).
% 8.32/2.80 tff(c_270, plain, (![VAR_V_354_171, VAR_V_355_172]: (pred_attacker(tuple_2(VAR_V_354_171, VAR_V_355_172)) | ~pred_attacker(VAR_V_355_172) | ~pred_attacker(VAR_V_354_171)))).
% 8.32/2.80 tff(c_266, plain, (![VAR_V_345_166, VAR_V_344_165, VAR_V_346_167]: (pred_attacker(VAR_V_345_166) | ~pred_attacker(tuple_3(VAR_V_344_165, VAR_V_345_166, VAR_V_346_167))))).
% 8.32/2.80 tff(c_200, plain, (![VAR_V_190X30_98, VAR_V_191_99, VAR_V_192_100]: (pred_attacker(VAR_V_190X30_98) | ~pred_attacker(tuple_client_A_out_1(VAR_V_190X30_98, VAR_V_191_99, VAR_V_192_100))))).
% 8.32/2.80 tff(c_268, plain, (![VAR_V_350X30_170, VAR_V_348_168, VAR_V_349_169]: (pred_attacker(VAR_V_350X30_170) | ~pred_attacker(tuple_3(VAR_V_348_168, VAR_V_349_169, VAR_V_350X30_170))))).
% 8.32/2.80 tff(c_138, plain, (![VAR_X0X30_9_51, VAR_X1_10X30_52, VAR_X2_11_53, VAR_X3_12_54]: (constr_tuple_4_get_1(tuple_4(VAR_X0X30_9_51, VAR_X1_10X30_52, VAR_X2_11_53, VAR_X3_12_54))=VAR_X1_10X30_52))).
% 8.32/2.80 tff(c_264, plain, (![VAR_V_340X30_162, VAR_V_341_163, VAR_V_342_164]: (pred_attacker(VAR_V_340X30_162) | ~pred_attacker(tuple_3(VAR_V_340X30_162, VAR_V_341_163, VAR_V_342_164))))).
% 8.32/2.80 tff(c_174, plain, (![VAR_V_139_84, VAR_V_137_82, VAR_V_138_83]: (pred_attacker(VAR_V_139_84) | ~pred_attacker(tuple_server_S_in_1(VAR_V_137_82, VAR_V_138_83, VAR_V_139_84))))).
% 8.32/2.80 tff(c_134, plain, (![VAR_X0X30_15_45, VAR_X1_16_46, VAR_X2_17_47, VAR_X3_18_48]: (constr_tuple_4_get_2_bitstring(tuple_4(VAR_X0X30_15_45, VAR_X1_16_46, VAR_X2_17_47, VAR_X3_18_48))=VAR_X2_17_47))).
% 8.32/2.80 tff(c_170, plain, (![VAR_V_129_76, VAR_V_130X30_77, VAR_V_131_78]: (pred_attacker(VAR_V_129_76) | ~pred_attacker(tuple_server_S_in_1(VAR_V_129_76, VAR_V_130X30_77, VAR_V_131_78))))).
% 8.32/2.80 tff(c_278, plain, (![VAR_V_371_180, VAR_V_370X30_179]: (pred_mess(VAR_V_371_180, VAR_V_370X30_179) | ~pred_attacker(VAR_V_370X30_179) | ~pred_attacker(VAR_V_371_180)))).
% 8.32/2.80 tff(c_202, plain, (![VAR_V_195_102, VAR_V_194_101, VAR_V_196_103]: (pred_attacker(VAR_V_195_102) | ~pred_attacker(tuple_client_A_out_1(VAR_V_194_101, VAR_V_195_102, VAR_V_196_103))))).
% 8.32/2.80 tff(c_132, plain, (![VAR_X0X30_19_41, VAR_X1_20X30_42, VAR_X2_21_43, VAR_X3_22_44]: (constr_tuple_4_get_3_bitstring(tuple_4(VAR_X0X30_19_41, VAR_X1_20X30_42, VAR_X2_21_43, VAR_X3_22_44))=VAR_X3_22_44))).
% 8.32/2.80 tff(c_172, plain, (![VAR_V_134_80, VAR_V_133_79, VAR_V_135_81]: (pred_attacker(VAR_V_134_80) | ~pred_attacker(tuple_server_S_in_1(VAR_V_133_79, VAR_V_134_80, VAR_V_135_81))))).
% 8.32/2.80 tff(c_140, plain, (![VAR_X0X30_7_55, VAR_X1_8_56, VAR_X2_0X30_57, VAR_X3_0X30_58]: (constr_tuple_4_get_0x30(tuple_4(VAR_X0X30_7_55, VAR_X1_8_56, VAR_X2_0X30_57, VAR_X3_0X30_58))=VAR_X0X30_7_55))).
% 8.32/2.80 tff(c_419, plain, (![VAR_0X40SID_388_183]: (pred_attacker(name_Na(VAR_0X40SID_388_183))))).
% 8.32/2.80 tff(c_204, plain, (![VAR_V_20X300X30_106, VAR_V_198_104, VAR_V_199_105]: (pred_attacker(VAR_V_20X300X30_106) | ~pred_attacker(tuple_client_A_out_1(VAR_V_198_104, VAR_V_199_105, VAR_V_20X300X30_106))))).
% 8.32/2.80 tff(c_276, plain, (![VAR_V_368_177, VAR_V_369_178]: (pred_attacker(VAR_V_368_177) | ~pred_attacker(VAR_V_369_178) | ~pred_mess(VAR_V_369_178, VAR_V_368_177)))).
% 8.32/2.80 tff(c_274, plain, (![VAR_V_366_176, VAR_V_365_175]: (pred_attacker(VAR_V_366_176) | ~pred_attacker(tuple_2(VAR_V_365_175, VAR_V_366_176))))).
% 8.32/2.80 tff(c_292, plain, (![VAR_0X40SID_388_183]: (pred_attacker(tuple_client_A_out_1(name_A, name_B, name_Na(VAR_0X40SID_388_183)))))).
% 8.32/2.80 tff(c_118, plain, (![VAR_X0X30_48_14, VAR_K_49_13]: (constr_cbc_dec_1(constr_cbc_enc_1(VAR_X0X30_48_14, VAR_K_49_13), VAR_K_49_13)=VAR_X0X30_48_14))).
% 8.32/2.80 tff(c_272, plain, (![VAR_V_362_173, VAR_V_363_174]: (pred_attacker(VAR_V_362_173) | ~pred_attacker(tuple_2(VAR_V_362_173, VAR_V_363_174))))).
% 8.32/2.80 tff(c_182, plain, (![VAR_V_149_87]: (pred_attacker(tuple_client_B_in_3(VAR_V_149_87)) | ~pred_attacker(VAR_V_149_87)))).
% 8.32/2.80 tff(c_208, plain, (![VAR_V_20X306_108]: (pred_attacker(VAR_V_20X306_108) | ~pred_attacker(tuple_client_A_in_4(VAR_V_20X306_108))))).
% 8.32/2.80 tff(c_192, plain, (![VAR_V_164_92]: (pred_attacker(VAR_V_164_92) | ~pred_attacker(tuple_client_A_out_5(VAR_V_164_92))))).
% 8.32/2.80 tff(c_206, plain, (![VAR_V_20X303_107]: (pred_attacker(tuple_client_A_in_4(VAR_V_20X303_107)) | ~pred_attacker(VAR_V_20X303_107)))).
% 8.32/2.80 tff(c_212, plain, (![VAR_V_212_110]: (pred_attacker(VAR_V_212_110) | ~pred_attacker(tuple_client_A_in_2(VAR_V_212_110))))).
% 8.32/2.80 tff(c_178, plain, (![VAR_V_143_85]: (pred_attacker(tuple_client_B_out_2(VAR_V_143_85)) | ~pred_attacker(VAR_V_143_85)))).
% 8.32/2.80 tff(c_196, plain, (![VAR_V_170X30_94]: (pred_attacker(VAR_V_170X30_94) | ~pred_attacker(tuple_client_A_out_3(VAR_V_170X30_94))))).
% 8.32/2.80 tff(c_142, plain, (![VAR_X0X30_0X30_59, VAR_X1_0X30_60]: (constr_tuple_2_get_1(tuple_2(VAR_X0X30_0X30_59, VAR_X1_0X30_60))=VAR_X1_0X30_60))).
% 8.32/2.80 tff(c_240, plain, (![VAR_V_269_138]: (pred_attacker(constr_cbc_2_get_1_prefixes(VAR_V_269_138)) | ~pred_attacker(VAR_V_269_138)))).
% 8.32/2.81 tff(c_148, plain, (![VAR_V_90X30_64]: (pred_attacker(constr_tuple_4_get_2_bitstring(VAR_V_90X30_64)) | ~pred_attacker(VAR_V_90X30_64)))).
% 8.32/2.81 tff(c_190, plain, (![VAR_V_161_91]: (pred_attacker(tuple_client_A_out_5(VAR_V_161_91)) | ~pred_attacker(VAR_V_161_91)))).
% 8.32/2.81 tff(c_210, plain, (![VAR_V_20X309_109]: (pred_attacker(tuple_client_A_in_2(VAR_V_20X309_109)) | ~pred_attacker(VAR_V_20X309_109)))).
% 8.32/2.81 tff(c_136, plain, (![VAR_X0X30_13_49, VAR_X1_14_50]: (constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_13_49, VAR_X1_14_50))=VAR_X0X30_13_49))).
% 8.32/2.81 tff(c_188, plain, (![VAR_V_158_90]: (pred_attacker(VAR_V_158_90) | ~pred_attacker(tuple_client_B_in_1(VAR_V_158_90))))).
% 8.32/2.81 tff(c_230, plain, (![VAR_V_259_133]: (pred_attacker(constr_cbc_4_get_3_prefixes(VAR_V_259_133)) | ~pred_attacker(VAR_V_259_133)))).
% 8.32/2.81 tff(c_152, plain, (![VAR_V_94_66]: (pred_attacker(constr_tuple_4_get_0x30(VAR_V_94_66)) | ~pred_attacker(VAR_V_94_66)))).
% 8.32/2.81 tff(c_232, plain, (![VAR_V_261_134]: (pred_attacker(constr_cbc_4_get_2_prefixes(VAR_V_261_134)) | ~pred_attacker(VAR_V_261_134)))).
% 8.32/2.81 tff(c_166, plain, (![VAR_V_10X309_72]: (pred_attacker(VAR_V_10X309_72) | ~pred_attacker(tuple_server_S_out_2(VAR_V_10X309_72))))).
% 8.32/2.81 tff(c_160, plain, (![VAR_V_10X300X30_69]: (pred_attacker(tuple_succ(VAR_V_10X300X30_69)) | ~pred_attacker(VAR_V_10X300X30_69)))).
% 8.32/2.81 tff(c_164, plain, (![VAR_V_10X306_71]: (pred_attacker(tuple_server_S_out_2(VAR_V_10X306_71)) | ~pred_attacker(VAR_V_10X306_71)))).
% 8.32/2.81 tff(c_146, plain, (![VAR_V_88_63]: (pred_attacker(constr_tuple_4_get_3_bitstring(VAR_V_88_63)) | ~pred_attacker(VAR_V_88_63)))).
% 8.32/2.81 tff(c_184, plain, (![VAR_V_152_88]: (pred_attacker(VAR_V_152_88) | ~pred_attacker(tuple_client_B_in_3(VAR_V_152_88))))).
% 8.32/2.81 tff(c_156, plain, (![VAR_V_98_68]: (pred_attacker(constr_tuple_2_get_0x30_bitstring(VAR_V_98_68)) | ~pred_attacker(VAR_V_98_68)))).
% 8.32/2.81 tff(c_180, plain, (![VAR_V_146_86]: (pred_attacker(VAR_V_146_86) | ~pred_attacker(tuple_client_B_out_2(VAR_V_146_86))))).
% 8.32/2.81 tff(c_150, plain, (![VAR_V_92_65]: (pred_attacker(constr_tuple_4_get_1(VAR_V_92_65)) | ~pred_attacker(VAR_V_92_65)))).
% 8.32/2.81 tff(c_186, plain, (![VAR_V_155_89]: (pred_attacker(tuple_client_B_in_1(VAR_V_155_89)) | ~pred_attacker(VAR_V_155_89)))).
% 8.32/2.81 tff(c_236, plain, (![VAR_V_265_136]: (pred_attacker(constr_cbc_3_get_2_prefixes(VAR_V_265_136)) | ~pred_attacker(VAR_V_265_136)))).
% 8.32/2.81 tff(c_154, plain, (![VAR_V_96_67]: (pred_attacker(constr_tuple_2_get_1(VAR_V_96_67)) | ~pred_attacker(VAR_V_96_67)))).
% 8.32/2.81 tff(c_162, plain, (![VAR_V_10X303_70]: (pred_attacker(VAR_V_10X303_70) | ~pred_attacker(tuple_succ(VAR_V_10X303_70))))).
% 8.32/2.81 tff(c_234, plain, (![VAR_V_263_135]: (pred_attacker(constr_cbc_4_get_1_prefixes(VAR_V_263_135)) | ~pred_attacker(VAR_V_263_135)))).
% 8.32/2.81 tff(c_194, plain, (![VAR_V_167_93]: (pred_attacker(tuple_client_A_out_3(VAR_V_167_93)) | ~pred_attacker(VAR_V_167_93)))).
% 8.32/2.81 tff(c_238, plain, (![VAR_V_267_137]: (pred_attacker(constr_cbc_3_get_1_prefixes(VAR_V_267_137)) | ~pred_attacker(VAR_V_267_137)))).
% 8.32/2.81 tff(c_288, plain, (![VAR_V_373_181]: (pred_equal(VAR_V_373_181, VAR_V_373_181)))).
% 8.32/2.81 tff(c_144, plain, (![VAR_X_81_61, VAR_Y_82_62]: (pred_eq_bitstring_bitstring(VAR_X_81_61, VAR_Y_82_62)))).
% 8.32/2.81 tff(c_290, plain, (![VAR_V_374_182]: (pred_attacker(name_new0x2Dname(VAR_V_374_182))))).
% 8.32/2.81 tff(c_248, plain, (pred_attacker(constr_CONST_1))).
% 8.32/2.81 tff(c_86, plain, (name_Kas!=name_A)).
% 8.32/2.81 tff(c_98, plain, (name_c!=name_B)).
% 8.32/2.81 tff(c_90, plain, (name_c!=name_A)).
% 8.32/2.81 tff(c_92, plain, (name_I!=name_B)).
% 8.32/2.81 tff(c_88, plain, (name_Kbs!=name_A)).
% 8.32/2.81 tff(c_94, plain, (name_Kas!=name_B)).
% 8.32/2.81 tff(c_246, plain, (pred_attacker(constr_CONST_2))).
% 8.32/2.81 tff(c_78, plain, (name_Kbs!=constr_CONST_4)).
% 8.32/2.81 tff(c_96, plain, (name_Kbs!=name_B)).
% 8.32/2.81 tff(c_102, plain, (name_Kbs!=name_I)).
% 8.32/2.81 tff(c_100, plain, (name_Kas!=name_I)).
% 8.32/2.81 tff(c_82, plain, (name_B!=name_A)).
% 8.32/2.81 tff(c_84, plain, (name_I!=name_A)).
% 8.32/2.81 tff(c_104, plain, (name_c!=name_I)).
% 8.32/2.81 tff(c_74, plain, (name_I!=constr_CONST_4)).
% 8.32/2.81 tff(c_80, plain, (name_c!=constr_CONST_4)).
% 8.32/2.81 tff(c_106, plain, (name_Kbs!=name_Kas)).
% 8.32/2.81 tff(c_72, plain, (name_B!=constr_CONST_4)).
% 8.32/2.81 tff(c_70, plain, (name_A!=constr_CONST_4)).
% 8.32/2.81 tff(c_108, plain, (name_c!=name_Kas)).
% 8.32/2.81 tff(c_76, plain, (name_Kas!=constr_CONST_4)).
% 8.32/2.81 tff(c_110, plain, (name_c!=name_Kbs)).
% 8.32/2.81 tff(c_250, plain, (pred_attacker(constr_CONST_0x30))).
% 8.32/2.81 tff(c_66, plain, (name_Kbs!=constr_CONST_3)).
% 8.32/2.81 tff(c_68, plain, (name_c!=constr_CONST_3)).
% 8.32/2.81 tff(c_280, plain, (pred_attacker(name_c))).
% 8.32/2.81 tff(c_282, plain, (pred_attacker(name_I))).
% 8.32/2.81 tff(c_244, plain, (pred_attacker(constr_CONST_3))).
% 8.32/2.81 tff(c_62, plain, (name_I!=constr_CONST_3)).
% 8.32/2.81 tff(c_54, plain, (name_c!=constr_CONST_2)).
% 8.32/2.81 tff(c_4, plain, (constr_CONST_2!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_58, plain, (name_A!=constr_CONST_3)).
% 8.32/2.81 tff(c_64, plain, (name_Kas!=constr_CONST_3)).
% 8.32/2.81 tff(c_6, plain, (constr_CONST_3!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_8, plain, (constr_CONST_4!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_50, plain, (name_Kas!=constr_CONST_2)).
% 8.32/2.81 tff(c_60, plain, (name_B!=constr_CONST_3)).
% 8.32/2.81 tff(c_242, plain, (pred_attacker(constr_CONST_4))).
% 8.32/2.81 tff(c_56, plain, (constr_CONST_4!=constr_CONST_3)).
% 8.32/2.81 tff(c_42, plain, (constr_CONST_4!=constr_CONST_2)).
% 8.32/2.81 tff(c_12, plain, (name_B!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_52, plain, (name_Kbs!=constr_CONST_2)).
% 8.32/2.81 tff(c_28, plain, (name_A!=constr_CONST_1)).
% 8.32/2.81 tff(c_30, plain, (name_B!=constr_CONST_1)).
% 8.32/2.81 tff(c_32, plain, (name_I!=constr_CONST_1)).
% 8.32/2.81 tff(c_34, plain, (name_Kas!=constr_CONST_1)).
% 8.32/2.81 tff(c_26, plain, (constr_CONST_4!=constr_CONST_1)).
% 8.32/2.81 tff(c_22, plain, (constr_CONST_2!=constr_CONST_1)).
% 8.32/2.81 tff(c_36, plain, (name_Kbs!=constr_CONST_1)).
% 8.32/2.81 tff(c_20, plain, (name_c!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_38, plain, (name_c!=constr_CONST_1)).
% 8.32/2.81 tff(c_40, plain, (constr_CONST_3!=constr_CONST_2)).
% 8.32/2.81 tff(c_24, plain, (constr_CONST_3!=constr_CONST_1)).
% 8.32/2.81 tff(c_18, plain, (name_Kbs!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_44, plain, (name_A!=constr_CONST_2)).
% 8.32/2.81 tff(c_46, plain, (name_B!=constr_CONST_2)).
% 8.32/2.81 tff(c_158, plain, (pred_attacker(tuple_true))).
% 8.32/2.81 tff(c_16, plain, (name_Kas!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_14, plain, (name_I!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_10, plain, (name_A!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_48, plain, (name_I!=constr_CONST_2)).
% 8.32/2.81 tff(c_176, plain, (pred_attacker(tuple_false))).
% 8.32/2.81 tff(c_284, plain, (pred_attacker(name_B))).
% 8.32/2.81 tff(c_2, plain, (constr_CONST_1!=constr_CONST_0x30)).
% 8.32/2.81 tff(c_286, plain, (pred_attacker(name_A))).
% 8.32/2.81 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.32/2.81
%------------------------------------------------------------------------------