%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW968+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:09:51 PM UTC 2026
% Result : Theorem 0.32s 15.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW968+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/15.42 % CPULimit : 300
% 0.09/15.42 % WCLimit : 300
% 0.09/15.42 % DateTime : Mon Sep 21 10:21:00 UTC 2026
% 0.09/15.43 % CPUTime :
% 0.09/15.44 % Drodi V4.1.1
% 0.32/15.59 % Refutation found
% 0.32/15.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.32/15.59 % SZS output start CNFRefutation for theBenchmark
% 0.32/15.59 fof(f81,axiom,(
% 0.32/15.59 (! [VAR_K_53,VAR_X0X30_51,VAR_X1_52] : constr_cbc_dec_2(constr_cbc_enc_2(VAR_X0X30_51,VAR_X1_52,VAR_K_53),VAR_K_53) = tuple_2(VAR_X0X30_51,VAR_X1_52) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f84,axiom,(
% 0.32/15.59 (! [VAR_K_43,VAR_X0X30_39,VAR_X1_40X30,VAR_X2_41,VAR_X3_42] : constr_cbc_4_get_2_prefixes(constr_cbc_enc_4(VAR_X0X30_39,VAR_X1_40X30,VAR_X2_41,VAR_X3_42,VAR_K_43)) = constr_cbc_enc_2(VAR_X0X30_39,VAR_X1_40X30,VAR_K_43) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f89,axiom,(
% 0.32/15.59 (! [VAR_K_0X30,VAR_M_0X30] : constr_dec(constr_enc(VAR_M_0X30,VAR_K_0X30),VAR_K_0X30) = VAR_M_0X30 )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f92,axiom,(
% 0.32/15.59 (! [VAR_X0X30_13,VAR_X1_14] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_13,VAR_X1_14)) = VAR_X0X30_13 )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f96,axiom,(
% 0.32/15.59 (! [VAR_X_81,VAR_Y_82] : pred_eq_bitstring_bitstring(VAR_X_81,VAR_Y_82) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f107,axiom,(
% 0.32/15.59 (! [VAR_V_10X309] :( pred_attacker(tuple_server_S_out_2(VAR_V_10X309))=> pred_attacker(VAR_V_10X309) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f108,axiom,(
% 0.32/15.59 (! [VAR_V_114,VAR_V_115,VAR_V_116] :( ( pred_attacker(VAR_V_114)& pred_attacker(VAR_V_115)& pred_attacker(VAR_V_116) )=> pred_attacker(tuple_server_S_in_1(VAR_V_114,VAR_V_115,VAR_V_116)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f114,axiom,(
% 0.32/15.59 (! [VAR_V_148,VAR_V_149] :( ( pred_attacker(VAR_V_148)& pred_attacker(VAR_V_149) )=> pred_attacker(constr_dec(VAR_V_148,VAR_V_149)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f122,axiom,(
% 0.32/15.59 (! [VAR_V_172] :( pred_attacker(tuple_client_A_out_9(VAR_V_172))=> pred_attacker(VAR_V_172) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f130,axiom,(
% 0.32/15.59 (! [VAR_V_196] :( pred_attacker(tuple_client_A_out_10(VAR_V_196))=> pred_attacker(VAR_V_196) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f134,axiom,(
% 0.32/15.59 (! [VAR_V_224,VAR_V_225,VAR_V_226] :( pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226))=> pred_attacker(VAR_V_226) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f135,axiom,(
% 0.32/15.59 (! [VAR_V_229] :( pred_attacker(VAR_V_229)=> pred_attacker(tuple_client_A_in_8(VAR_V_229)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f136,axiom,(
% 0.32/15.59 (! [VAR_V_232] :( pred_attacker(tuple_client_A_in_8(VAR_V_232))=> pred_attacker(VAR_V_232) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f137,axiom,(
% 0.32/15.59 (! [VAR_V_235] :( pred_attacker(VAR_V_235)=> pred_attacker(tuple_client_A_in_6(VAR_V_235)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f139,axiom,(
% 0.32/15.59 (! [VAR_V_241] :( pred_attacker(VAR_V_241)=> pred_attacker(tuple_client_A_in_4(VAR_V_241)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f141,axiom,(
% 0.32/15.59 (! [VAR_V_247] :( pred_attacker(VAR_V_247)=> pred_attacker(tuple_client_A_in_2(VAR_V_247)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f152,axiom,(
% 0.32/15.59 (! [VAR_V_299] :( pred_attacker(VAR_V_299)=> pred_attacker(constr_cbc_4_get_2_prefixes(VAR_V_299)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f157,axiom,(
% 0.32/15.59 pred_attacker(constr_CONST_4) ),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f171,axiom,(
% 0.32/15.59 (! [VAR_V_392,VAR_V_393] :( ( pred_attacker(VAR_V_392)& pred_attacker(VAR_V_393) )=> pred_attacker(tuple_2(VAR_V_392,VAR_V_393)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f182,axiom,(
% 0.32/15.59 (! [VAR_0X40SID_426] : pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(VAR_0X40SID_426))) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f186,axiom,(
% 0.32/15.59 (! [VAR_0X40SID_60X304,VAR_ENC_KAB_A0X27_60X306,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_ENC_NB_60X302,VAR_ENC_SUCC_NA0X27_60X305] :( ( pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas))))& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306))& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302))& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))& pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303)) )=> pred_attacker(tuple_client_A_out_9(name_objective1)) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f187,axiom,(
% 0.32/15.59 (! [VAR_0X40SID_622,VAR_ENC_KAB_A0X27_624,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_ENC_NB_620X30,VAR_ENC_SUCC_NA0X27_623] :( ( pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624))& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30))& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))& pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621)) )=> pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f189,axiom,(
% 0.32/15.59 (! [VAR_0X40SID_758,VAR_A_755,VAR_B_756,VAR_NA_757] :( pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757))=> pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas))) ) )),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f190,conjecture,(
% 0.32/15.59 pred_attacker(tuple_2(name_objective1,name_objective2)) ),
% 0.32/15.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/15.59 fof(f191,negated_conjecture,(
% 0.32/15.59 ~(pred_attacker(tuple_2(name_objective1,name_objective2)) )),
% 0.32/15.59 inference(negated_conjecture,[status(cth)],[f190])).
% 0.32/15.59 fof(f272,plain,(
% 0.32/15.59 ![X0,X1,X2]: (constr_cbc_dec_2(constr_cbc_enc_2(X0,X1,X2),X2)=tuple_2(X0,X1))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f81])).
% 0.32/15.59 fof(f275,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (constr_cbc_4_get_2_prefixes(constr_cbc_enc_4(X0,X1,X2,X3,X4))=constr_cbc_enc_2(X0,X1,X4))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f84])).
% 0.32/15.59 fof(f280,plain,(
% 0.32/15.59 ![X0,X1]: (constr_dec(constr_enc(X0,X1),X1)=X0)),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f89])).
% 0.32/15.59 fof(f283,plain,(
% 0.32/15.59 ![X0,X1]: (constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1))=X0)),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f92])).
% 0.32/15.59 fof(f287,plain,(
% 0.32/15.59 ![X0,X1]: (pred_eq_bitstring_bitstring(X0,X1))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f96])).
% 0.32/15.59 fof(f307,plain,(
% 0.32/15.59 ![VAR_V_10X309]: (~pred_attacker(tuple_server_S_out_2(VAR_V_10X309))|pred_attacker(VAR_V_10X309))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 0.32/15.59 fof(f308,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_server_S_out_2(X0))|pred_attacker(X0))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f307])).
% 0.32/15.59 fof(f309,plain,(
% 0.32/15.59 ![VAR_V_114,VAR_V_115,VAR_V_116]: (((~pred_attacker(VAR_V_114)|~pred_attacker(VAR_V_115))|~pred_attacker(VAR_V_116))|pred_attacker(tuple_server_S_in_1(VAR_V_114,VAR_V_115,VAR_V_116)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f108])).
% 0.32/15.59 fof(f310,plain,(
% 0.32/15.59 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(tuple_server_S_in_1(X0,X1,X2)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f309])).
% 0.32/15.59 fof(f323,plain,(
% 0.32/15.59 ![VAR_V_148,VAR_V_149]: ((~pred_attacker(VAR_V_148)|~pred_attacker(VAR_V_149))|pred_attacker(constr_dec(VAR_V_148,VAR_V_149)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 0.32/15.59 fof(f324,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_dec(X0,X1)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f323])).
% 0.32/15.59 fof(f339,plain,(
% 0.32/15.59 ![VAR_V_172]: (~pred_attacker(tuple_client_A_out_9(VAR_V_172))|pred_attacker(VAR_V_172))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f122])).
% 0.32/15.59 fof(f340,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_out_9(X0))|pred_attacker(X0))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f339])).
% 0.32/15.59 fof(f355,plain,(
% 0.32/15.59 ![VAR_V_196]: (~pred_attacker(tuple_client_A_out_10(VAR_V_196))|pred_attacker(VAR_V_196))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f130])).
% 0.32/15.59 fof(f356,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_out_10(X0))|pred_attacker(X0))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f355])).
% 0.32/15.59 fof(f365,plain,(
% 0.32/15.59 ![VAR_V_224,VAR_V_225,VAR_V_226]: (~pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226))|pred_attacker(VAR_V_226))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f134])).
% 0.32/15.59 fof(f366,plain,(
% 0.32/15.59 ![VAR_V_226]: ((![VAR_V_224,VAR_V_225]: ~pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226)))|pred_attacker(VAR_V_226))),
% 0.32/15.59 inference(miniscoping,[status(thm)],[f365])).
% 0.32/15.59 fof(f367,plain,(
% 0.32/15.59 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_out_1(X0,X1,X2))|pred_attacker(X2))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f366])).
% 0.32/15.59 fof(f368,plain,(
% 0.32/15.59 ![VAR_V_229]: (~pred_attacker(VAR_V_229)|pred_attacker(tuple_client_A_in_8(VAR_V_229)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f135])).
% 0.32/15.59 fof(f369,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_8(X0)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f368])).
% 0.32/15.59 fof(f370,plain,(
% 0.32/15.59 ![VAR_V_232]: (~pred_attacker(tuple_client_A_in_8(VAR_V_232))|pred_attacker(VAR_V_232))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f136])).
% 0.32/15.59 fof(f371,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_8(X0))|pred_attacker(X0))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f370])).
% 0.32/15.59 fof(f372,plain,(
% 0.32/15.59 ![VAR_V_235]: (~pred_attacker(VAR_V_235)|pred_attacker(tuple_client_A_in_6(VAR_V_235)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f137])).
% 0.32/15.59 fof(f373,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_6(X0)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f372])).
% 0.32/15.59 fof(f376,plain,(
% 0.32/15.59 ![VAR_V_241]: (~pred_attacker(VAR_V_241)|pred_attacker(tuple_client_A_in_4(VAR_V_241)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f139])).
% 0.32/15.59 fof(f377,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_4(X0)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f376])).
% 0.32/15.59 fof(f380,plain,(
% 0.32/15.59 ![VAR_V_247]: (~pred_attacker(VAR_V_247)|pred_attacker(tuple_client_A_in_2(VAR_V_247)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f141])).
% 0.32/15.59 fof(f381,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_2(X0)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f380])).
% 0.32/15.59 fof(f402,plain,(
% 0.32/15.59 ![VAR_V_299]: (~pred_attacker(VAR_V_299)|pred_attacker(constr_cbc_4_get_2_prefixes(VAR_V_299)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f152])).
% 0.32/15.59 fof(f403,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_cbc_4_get_2_prefixes(X0)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f402])).
% 0.32/15.59 fof(f412,plain,(
% 0.32/15.59 pred_attacker(constr_CONST_4)),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f157])).
% 0.32/15.59 fof(f442,plain,(
% 0.32/15.59 ![VAR_V_392,VAR_V_393]: ((~pred_attacker(VAR_V_392)|~pred_attacker(VAR_V_393))|pred_attacker(tuple_2(VAR_V_392,VAR_V_393)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f171])).
% 0.32/15.59 fof(f443,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_2(X0,X1)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f442])).
% 0.32/15.59 fof(f461,plain,(
% 0.32/15.59 ![X0]: (pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(X0))))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f182])).
% 0.32/15.59 fof(f470,plain,(
% 0.32/15.59 ![VAR_0X40SID_60X304,VAR_ENC_KAB_A0X27_60X306,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_ENC_NB_60X302,VAR_ENC_SUCC_NA0X27_60X305]: ((((((((~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306)))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302)))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303)))|pred_attacker(tuple_client_A_out_9(name_objective1)))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f186])).
% 0.32/15.59 fof(f471,plain,(
% 0.32/15.59 (![VAR_ENC_NA_B_ENC_KAB_A_60X303]: ((![VAR_0X40SID_60X304]: (((![VAR_ENC_NB_60X302]: ((![VAR_ENC_KAB_A0X27_60X306]: (((![VAR_ENC_SUCC_NA0X27_60X305]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306))))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302))))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303))))|pred_attacker(tuple_client_A_out_9(name_objective1))),
% 0.32/15.59 inference(miniscoping,[status(thm)],[f470])).
% 0.32/15.59 fof(f472,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas))))|~pred_attacker(tuple_client_A_in_8(X3))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X4))|~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_9(name_objective1)))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f471])).
% 0.32/15.59 fof(f473,plain,(
% 0.32/15.59 ![VAR_0X40SID_622,VAR_ENC_KAB_A0X27_624,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_ENC_NB_620X30,VAR_ENC_SUCC_NA0X27_623]: ((((((((~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624)))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30)))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621)))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f187])).
% 0.32/15.59 fof(f474,plain,(
% 0.32/15.59 ![VAR_ENC_KAB_A0X27_624]: ((![VAR_ENC_NA_B_ENC_KAB_A_621]: ((![VAR_0X40SID_622]: (((![VAR_ENC_NB_620X30]: ((((![VAR_ENC_SUCC_NA0X27_623]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624)))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30))))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621))))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))))),
% 0.32/15.59 inference(miniscoping,[status(thm)],[f473])).
% 0.32/15.59 fof(f475,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas))))|~pred_attacker(tuple_client_A_in_8(X3))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X4))|~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas))))))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f474])).
% 0.32/15.59 fof(f479,plain,(
% 0.32/15.59 ![VAR_0X40SID_758,VAR_A_755,VAR_B_756,VAR_NA_757]: (~pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757))|pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas))))),
% 0.32/15.59 inference(pre_NNF_transformation,[status(thm)],[f189])).
% 0.32/15.59 fof(f480,plain,(
% 0.32/15.59 ![VAR_A_755,VAR_B_756,VAR_NA_757]: (~pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757))|(![VAR_0X40SID_758]: pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas)))))),
% 0.32/15.59 inference(miniscoping,[status(thm)],[f479])).
% 0.32/15.59 fof(f481,plain,(
% 0.32/15.59 ![X0,X1,X2,X3]: (~pred_attacker(tuple_server_S_in_1(X0,X1,X2))|pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(X2,X1,name_Kab_66(X3),constr_cbc_enc_2(name_Kab_66(X3),X0,name_Kbs),name_Kas))))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f480])).
% 0.32/15.59 fof(f482,plain,(
% 0.32/15.59 ~pred_attacker(tuple_2(name_objective1,name_objective2))),
% 0.32/15.59 inference(cnf_transformation,[status(thm)],[f191])).
% 0.32/15.59 fof(f483,definition,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (sQ0_spl <=> (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas))))|~pred_attacker(tuple_client_A_in_8(X3))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X4))|~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f484,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas))))|~pred_attacker(tuple_client_A_in_8(X3))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X4))|~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|~sQ0_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f483])).
% 0.32/15.59 fof(f486,definition,(
% 0.32/15.59 sQ1_spl <=> (pred_attacker(tuple_client_A_out_9(name_objective1)))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f487,plain,(
% 0.32/15.59 pred_attacker(tuple_client_A_out_9(name_objective1))|~sQ1_spl),
% 0.32/15.59 inference(component_clause,[status(thm)],[f486])).
% 0.32/15.59 fof(f489,plain,(
% 0.32/15.59 sQ0_spl|sQ1_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f472,f483,f486])).
% 0.32/15.59 fof(f496,definition,(
% 0.32/15.59 ![X0]: (sQ2_spl <=> (~pred_attacker(X0)))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f497,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ2_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f496])).
% 0.32/15.59 fof(f503,plain,(
% 0.32/15.59 $false|~sQ2_spl),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f412,f497])).
% 0.32/15.59 fof(f506,plain,(
% 0.32/15.59 ~sQ2_spl),
% 0.32/15.59 inference(contradiction_clause,[status(thm)],[f503])).
% 0.32/15.59 fof(f507,plain,(
% 0.32/15.59 ~pred_attacker(name_objective1)|~pred_attacker(name_objective2)),
% 0.32/15.59 inference(resolution,[status(thm)],[f443,f482])).
% 0.32/15.59 fof(f508,definition,(
% 0.32/15.59 sQ4_spl <=> (pred_attacker(name_objective1))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f510,plain,(
% 0.32/15.59 ~pred_attacker(name_objective1)|sQ4_spl),
% 0.32/15.59 inference(component_clause,[status(thm)],[f508])).
% 0.32/15.59 fof(f511,definition,(
% 0.32/15.59 sQ5_spl <=> (pred_attacker(name_objective2))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f514,plain,(
% 0.32/15.59 ~sQ4_spl|~sQ5_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f507,f508,f511])).
% 0.32/15.59 fof(f567,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_attacker(constr_cbc_enc_4(X0,X1,X2,X3,X4))|pred_attacker(constr_cbc_enc_2(X0,X1,X4)))),
% 0.32/15.59 inference(paramodulation,[status(thm)],[f275,f403])).
% 0.32/15.59 fof(f576,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_attacker(constr_enc(X0,X1))|~pred_attacker(X1)|pred_attacker(X0))),
% 0.32/15.59 inference(paramodulation,[status(thm)],[f280,f324])).
% 0.32/15.59 fof(f584,definition,(
% 0.32/15.59 ![X0]: (sQ10_spl <=> (~pred_attacker(X0)|~pred_attacker(X0)))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f585,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~pred_attacker(X0)|~sQ10_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f584])).
% 0.32/15.59 fof(f588,plain,(
% 0.32/15.59 ![X0]: (pred_attacker(name_Na(X0)))),
% 0.32/15.59 inference(resolution,[status(thm)],[f461,f367])).
% 0.32/15.59 fof(f655,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ10_spl)),
% 0.32/15.59 inference(duplicate_literals_removal,[status(thm)],[f585])).
% 0.32/15.59 fof(f656,plain,(
% 0.32/15.59 $false|~sQ10_spl),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f588,f655])).
% 0.32/15.59 fof(f670,plain,(
% 0.32/15.59 ~sQ10_spl),
% 0.32/15.59 inference(contradiction_clause,[status(thm)],[f656])).
% 0.32/15.59 fof(f677,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_8(X0))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))|~pred_attacker(tuple_client_A_in_4(X2))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X1,name_Kas))))))),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f475,f287])).
% 0.32/15.59 fof(f701,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_8(X0))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))|~pred_attacker(tuple_client_A_in_4(X2))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))|~sQ0_spl)),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f484,f287])).
% 0.32/15.59 fof(f704,plain,(
% 0.32/15.59 ![X0,X1,X2,X3,X4]: (~pred_attacker(X0)|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))|~pred_attacker(tuple_client_A_in_4(X2))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))|~sQ0_spl)),
% 0.32/15.59 inference(resolution,[status(thm)],[f369,f701])).
% 0.32/15.59 fof(f705,definition,(
% 0.32/15.59 ![X1]: (sQ16_spl <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f706,plain,(
% 0.32/15.59 ![X0]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X0))|~sQ16_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f705])).
% 0.32/15.59 fof(f708,definition,(
% 0.32/15.59 ![X2]: (sQ17_spl <=> (~pred_attacker(tuple_client_A_in_4(X2))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f709,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_4(X0))|~sQ17_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f708])).
% 0.32/15.59 fof(f711,definition,(
% 0.32/15.59 ![X3,X4]: (sQ18_spl <=> (~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f712,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X0,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X0,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X0))|~sQ18_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f711])).
% 0.32/15.59 fof(f714,plain,(
% 0.32/15.59 sQ2_spl|sQ16_spl|sQ17_spl|sQ18_spl|~sQ0_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f704,f496,f705,f708,f711,f483])).
% 0.32/15.59 fof(f715,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|~sQ18_spl)),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f712,f287])).
% 0.32/15.59 fof(f716,definition,(
% 0.32/15.59 ![X0]: (sQ19_spl <=> (~pred_attacker(tuple_client_A_in_8(X0))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f717,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_8(X0))|~sQ19_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f716])).
% 0.32/15.59 fof(f719,definition,(
% 0.32/15.59 ![X1]: (sQ20_spl <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X1,name_Kas)))))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f720,plain,(
% 0.32/15.59 ![X0]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X0))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))))|~sQ20_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f719])).
% 0.32/15.59 fof(f722,plain,(
% 0.32/15.59 sQ19_spl|sQ20_spl|sQ17_spl|sQ18_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f677,f716,f719,f708,f711])).
% 0.32/15.59 fof(f742,plain,(
% 0.32/15.59 pred_attacker(name_objective1)|~sQ1_spl),
% 0.32/15.59 inference(resolution,[status(thm)],[f340,f487])).
% 0.32/15.59 fof(f744,plain,(
% 0.32/15.59 $false|sQ4_spl|~sQ1_spl),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f742,f510])).
% 0.32/15.59 fof(f745,plain,(
% 0.32/15.59 sQ4_spl|~sQ1_spl),
% 0.32/15.59 inference(contradiction_clause,[status(thm)],[f744])).
% 0.32/15.59 fof(f788,plain,(
% 0.32/15.59 ![X0,X1,X2,X3]: (~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(X2,X1,name_Kab_66(X3),constr_cbc_enc_2(name_Kab_66(X3),X0,name_Kbs),name_Kas))))),
% 0.32/15.59 inference(resolution,[status(thm)],[f310,f481])).
% 0.32/15.59 fof(f827,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ18_spl)),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f381,f828])).
% 0.32/15.59 fof(f828,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_2(X0))|~sQ18_spl)),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f715,f287])).
% 0.32/15.59 fof(f829,plain,(
% 0.32/15.59 sQ2_spl|~sQ18_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f827,f496,f711])).
% 0.32/15.59 fof(f831,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ17_spl)),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f377,f709])).
% 0.32/15.59 fof(f832,plain,(
% 0.32/15.59 sQ2_spl|~sQ17_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f831,f496,f708])).
% 0.32/15.59 fof(f833,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_6(X0))|~sQ16_spl)),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f706,f287])).
% 0.32/15.59 fof(f834,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ16_spl)),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f373,f833])).
% 0.32/15.59 fof(f835,plain,(
% 0.32/15.59 sQ2_spl|~sQ16_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f834,f496,f705])).
% 0.32/15.59 fof(f836,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~sQ19_spl)),
% 0.32/15.59 inference(backward_subsumption_resolution,[status(thm)],[f369,f717])).
% 0.32/15.59 fof(f837,plain,(
% 0.32/15.59 sQ2_spl|~sQ19_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f836,f496,f716])).
% 0.32/15.59 fof(f838,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(tuple_client_A_in_6(X0))|pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))))|~sQ20_spl)),
% 0.32/15.59 inference(forward_subsumption_resolution,[status(thm)],[f720,f287])).
% 0.32/15.59 fof(f872,plain,(
% 0.32/15.59 ![X0]: (pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))))|~pred_attacker(X0)|~sQ20_spl)),
% 0.32/15.59 inference(resolution,[status(thm)],[f838,f373])).
% 0.32/15.59 fof(f873,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas))))|~sQ20_spl)),
% 0.32/15.59 inference(resolution,[status(thm)],[f872,f356])).
% 0.32/15.59 fof(f876,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))|pred_attacker(name_objective2)|~sQ20_spl)),
% 0.32/15.59 inference(resolution,[status(thm)],[f873,f576])).
% 0.32/15.59 fof(f878,definition,(
% 0.32/15.59 ![X0]: (sQ28_spl <=> (~pred_attacker(X0)|~pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))))),
% 0.32/15.59 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.32/15.59 fof(f879,plain,(
% 0.32/15.59 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))|~sQ28_spl)),
% 0.32/15.59 inference(component_clause,[status(thm)],[f878])).
% 0.32/15.59 fof(f881,plain,(
% 0.32/15.59 sQ28_spl|sQ5_spl|~sQ20_spl),
% 0.32/15.59 inference(split_clause,[status(thm)],[f876,f878,f511,f719])).
% 0.32/15.59 fof(f884,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas))|~pred_attacker(constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1)))|~sQ28_spl)),
% 0.32/15.59 inference(paramodulation,[status(thm)],[f272,f879])).
% 0.32/15.59 fof(f885,plain,(
% 0.32/15.59 ![X0,X1]: (~pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas))|~pred_attacker(X0)|~sQ28_spl)),
% 0.32/15.59 inference(forward_demodulation,[status(thm)],[f283,f884])).
% 0.32/15.59 fof(f914,plain,(
% 0.32/15.59 ![X0,X1,X2,X3]: (~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(constr_cbc_enc_4(X2,X1,name_Kab_66(X3),constr_cbc_enc_2(name_Kab_66(X3),X0,name_Kbs),name_Kas)))),
% 0.32/15.60 inference(resolution,[status(thm)],[f788,f308])).
% 0.32/15.60 fof(f929,plain,(
% 0.32/15.60 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(constr_cbc_enc_2(X2,X1,name_Kas)))),
% 0.32/15.60 inference(resolution,[status(thm)],[f914,f567])).
% 0.32/15.60 fof(f941,definition,(
% 0.32/15.60 ![X1,X2]: (sQ36_spl <=> (~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(constr_cbc_enc_2(X2,X1,name_Kas))))),
% 0.32/15.60 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.32/15.60 fof(f942,plain,(
% 0.32/15.60 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_cbc_enc_2(X1,X0,name_Kas))|~sQ36_spl)),
% 0.32/15.60 inference(component_clause,[status(thm)],[f941])).
% 0.32/15.60 fof(f944,plain,(
% 0.32/15.60 sQ2_spl|sQ36_spl),
% 0.32/15.60 inference(split_clause,[status(thm)],[f929,f496,f941])).
% 0.32/15.60 fof(f957,plain,(
% 0.32/15.60 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|~sQ28_spl|~sQ36_spl)),
% 0.32/15.60 inference(forward_subsumption_resolution,[status(thm)],[f942,f885])).
% 0.32/15.60 fof(f971,plain,(
% 0.32/15.60 ![X0]: (~pred_attacker(tuple_client_A_in_8(X0))|~sQ28_spl|~sQ36_spl)),
% 0.32/15.60 inference(backward_subsumption_resolution,[status(thm)],[f371,f957])).
% 0.32/15.60 fof(f1056,plain,(
% 0.32/15.60 sQ19_spl|~sQ28_spl|~sQ36_spl),
% 0.32/15.60 inference(split_clause,[status(thm)],[f971,f716,f878,f941])).
% 0.32/15.60 fof(f1110,plain,(
% 0.32/15.60 $false),
% 0.32/15.60 inference(sat_refutation,[status(thm)],[f489,f506,f514,f670,f714,f722,f745,f829,f832,f835,f837,f881,f944,f1056])).
% 0.32/15.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.32/15.62 % Elapsed time: 0.173593 seconds
% 0.32/15.62 % CPU time: 1.181897 seconds
% 0.32/15.62 % Total memory used: 87.676 MB
% 0.32/15.62 % Net memory used: 85.990 MB
%------------------------------------------------------------------------------