%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:50 PM UTC 2026
% Result : Theorem 14.96s 2.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:20:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 14.96/2.56 % Refutation found
% 14.96/2.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.96/2.56 % SZS output start CNFRefutation for theBenchmark
% 14.96/2.56 fof(f43,axiom,(
% 14.96/2.56 constr_CONST_4 != name_A ),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f44,axiom,(
% 14.96/2.56 constr_CONST_4 != name_B ),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f81,axiom,(
% 14.96/2.56 (! [VAR_K_44,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_44),constr_pkey(VAR_K_44)) = VAR_M_0X30 )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f84,axiom,(
% 14.96/2.56 (! [VAR_K_34,VAR_X1_32,VAR_X2_33] : constr_ecb_dec_2(constr_ecb_enc_2(VAR_X1_32,VAR_X2_33,constr_pkey(VAR_K_34)),VAR_K_34) = tuple_2(VAR_X1_32,VAR_X2_33) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f87,axiom,(
% 14.96/2.56 (! [VAR_K_25,VAR_X1_23,VAR_X2_24,VAR_X3_0X30] : constr_ecb_enc_3(VAR_X1_23,VAR_X2_24,VAR_X3_0X30,VAR_K_25) = tuple_3(constr_ecb_enc_1(VAR_X1_23,VAR_K_25),constr_ecb_enc_1(VAR_X2_24,VAR_K_25),constr_ecb_enc_1(VAR_X3_0X30,VAR_K_25)) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f88,axiom,(
% 14.96/2.56 (! [VAR_K_0X30,VAR_X1_21,VAR_X2_22] : constr_ecb_enc_2(VAR_X1_21,VAR_X2_22,VAR_K_0X30) = tuple_2(constr_ecb_enc_1(VAR_X1_21,VAR_K_0X30),constr_ecb_enc_1(VAR_X2_22,VAR_K_0X30)) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f90,axiom,(
% 14.96/2.56 (! [VAR_X0X30_16,VAR_X1_17] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_16,VAR_X1_17)) = VAR_X1_17 )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f96,axiom,(
% 14.96/2.56 (! [VAR_X_66,VAR_Y_67] : pred_eq_bitstring_bitstring(VAR_X_66,VAR_Y_67) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f106,axiom,(
% 14.96/2.56 (! [VAR_V_91] :( pred_attacker(VAR_V_91)=> pred_attacker(constr_pkey(VAR_V_91)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f114,axiom,(
% 14.96/2.56 (! [VAR_V_115] :( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_115))=> pred_attacker(VAR_V_115) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f115,axiom,(
% 14.96/2.56 (! [VAR_V_119,VAR_V_120X30] :( ( pred_attacker(VAR_V_119)& pred_attacker(VAR_V_120X30) )=> pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_119,VAR_V_120X30)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f118,axiom,(
% 14.96/2.56 (! [VAR_V_135,VAR_V_136] :( ( pred_attacker(VAR_V_135)& pred_attacker(VAR_V_136) )=> pred_attacker(tuple_key_register_server_in_1(VAR_V_135,VAR_V_136)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f119,axiom,(
% 14.96/2.56 (! [VAR_V_143,VAR_V_144] :( pred_attacker(tuple_key_register_server_in_1(VAR_V_143,VAR_V_144))=> pred_attacker(VAR_V_143) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f127,axiom,(
% 14.96/2.56 (! [VAR_V_181,VAR_V_182] :( ( pred_attacker(VAR_V_181)& pred_attacker(VAR_V_182) )=> pred_attacker(constr_ecb_enc_1(VAR_V_181,VAR_V_182)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f130,axiom,(
% 14.96/2.56 (! [VAR_V_193,VAR_V_194] :( ( pred_attacker(VAR_V_193)& pred_attacker(VAR_V_194) )=> pred_attacker(constr_ecb_dec_2(VAR_V_193,VAR_V_194)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f134,axiom,(
% 14.96/2.56 (! [VAR_V_20X307] :( pred_attacker(tuple_client_B_out_6(VAR_V_20X307))=> pred_attacker(VAR_V_20X307) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f136,axiom,(
% 14.96/2.56 (! [VAR_V_213] :( pred_attacker(tuple_client_B_out_4(VAR_V_213))=> pred_attacker(VAR_V_213) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f140,axiom,(
% 14.96/2.56 (! [VAR_V_232] :( pred_attacker(VAR_V_232)=> pred_attacker(tuple_client_B_in_5(VAR_V_232)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f142,axiom,(
% 14.96/2.56 (! [VAR_V_238] :( pred_attacker(VAR_V_238)=> pred_attacker(tuple_client_B_in_3(VAR_V_238)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f144,axiom,(
% 14.96/2.56 (! [VAR_V_244] :( pred_attacker(VAR_V_244)=> pred_attacker(tuple_client_B_in_2(VAR_V_244)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f158,axiom,(
% 14.96/2.56 pred_attacker(constr_CONST_4) ),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f170,axiom,(
% 14.96/2.56 (! [VAR_V_367,VAR_V_368,VAR_V_369] :( pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369))=> pred_attacker(VAR_V_368) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f172,axiom,(
% 14.96/2.56 (! [VAR_V_377,VAR_V_378] :( ( pred_attacker(VAR_V_377)& pred_attacker(VAR_V_378) )=> pred_attacker(tuple_2(VAR_V_377,VAR_V_378)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f174,axiom,(
% 14.96/2.56 (! [VAR_V_388,VAR_V_389] :( pred_attacker(tuple_2(VAR_V_388,VAR_V_389))=> pred_attacker(VAR_V_389) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f178,axiom,(
% 14.96/2.56 pred_attacker(name_I) ),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f185,axiom,(
% 14.96/2.56 pred_attacker(tuple_out_1(constr_pkey(name_skA))) ),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f192,axiom,(
% 14.96/2.56 (! [VAR_0X40SID_688,VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687] :( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687)) )=> pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS)))))) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f193,axiom,(
% 14.96/2.56 (! [VAR_0X40SID_718,VAR_ECB_ENC_NA_A_720X30,VAR_ECB_ENC_NB_719,VAR_SIGN_A_PKA_721] :( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB))& pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721)) )=> pred_attacker(tuple_client_B_out_6(name_objective)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f194,axiom,(
% 14.96/2.56 (! [VAR_DST_760X30,VAR_PKDST_761,VAR_SRC_762] :( ( pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761))& pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30)) )=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS))) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f195,axiom,(
% 14.96/2.56 (! [VAR_HOST_814,VAR_PK_815] :( ( VAR_HOST_814 != name_B& VAR_HOST_814 != name_A& pred_attacker(tuple_key_register_server_in_1(VAR_HOST_814,VAR_PK_815)) )=> pred_table(tuple_keys(VAR_HOST_814,VAR_PK_815)) ) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f196,conjecture,(
% 14.96/2.56 (! [VAR_V_823] : pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)) )),
% 14.96/2.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.96/2.56 fof(f197,negated_conjecture,(
% 14.96/2.56 ~((! [VAR_V_823] : pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)) ))),
% 14.96/2.56 inference(negated_conjecture,[status(cth)],[f196])).
% 14.96/2.56 fof(f240,plain,(
% 14.96/2.56 ~constr_CONST_4=name_A),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f43])).
% 14.96/2.56 fof(f241,plain,(
% 14.96/2.56 ~constr_CONST_4=name_B),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f44])).
% 14.96/2.56 fof(f278,plain,(
% 14.96/2.56 ![X0,X1]: (constr_checksign(constr_sign(X0,X1),constr_pkey(X1))=X0)),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f81])).
% 14.96/2.56 fof(f281,plain,(
% 14.96/2.56 ![X0,X1,X2]: (constr_ecb_dec_2(constr_ecb_enc_2(X0,X1,constr_pkey(X2)),X2)=tuple_2(X0,X1))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f84])).
% 14.96/2.56 fof(f284,plain,(
% 14.96/2.56 ![X0,X1,X2,X3]: (constr_ecb_enc_3(X0,X1,X2,X3)=tuple_3(constr_ecb_enc_1(X0,X3),constr_ecb_enc_1(X1,X3),constr_ecb_enc_1(X2,X3)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f87])).
% 14.96/2.56 fof(f285,plain,(
% 14.96/2.56 ![X0,X1,X2]: (constr_ecb_enc_2(X0,X1,X2)=tuple_2(constr_ecb_enc_1(X0,X2),constr_ecb_enc_1(X1,X2)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f88])).
% 14.96/2.56 fof(f287,plain,(
% 14.96/2.56 ![X0,X1]: (constr_tuple_2_get_1_bitstring(tuple_2(X0,X1))=X1)),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f90])).
% 14.96/2.56 fof(f293,plain,(
% 14.96/2.56 ![X0,X1]: (pred_eq_bitstring_bitstring(X0,X1))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f96])).
% 14.96/2.56 fof(f311,plain,(
% 14.96/2.56 ![VAR_V_91]: (~pred_attacker(VAR_V_91)|pred_attacker(constr_pkey(VAR_V_91)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 14.96/2.56 fof(f312,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_pkey(X0)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f311])).
% 14.96/2.56 fof(f327,plain,(
% 14.96/2.56 ![VAR_V_115]: (~pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_115))|pred_attacker(VAR_V_115))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 14.96/2.56 fof(f328,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(tuple_key_retrieval_server_out_2(X0))|pred_attacker(X0))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f327])).
% 14.96/2.56 fof(f329,plain,(
% 14.96/2.56 ![VAR_V_119,VAR_V_120X30]: ((~pred_attacker(VAR_V_119)|~pred_attacker(VAR_V_120X30))|pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_119,VAR_V_120X30)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f115])).
% 14.96/2.56 fof(f330,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f329])).
% 14.96/2.56 fof(f337,plain,(
% 14.96/2.56 ![VAR_V_135,VAR_V_136]: ((~pred_attacker(VAR_V_135)|~pred_attacker(VAR_V_136))|pred_attacker(tuple_key_register_server_in_1(VAR_V_135,VAR_V_136)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 14.96/2.56 fof(f338,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_register_server_in_1(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f337])).
% 14.96/2.56 fof(f339,plain,(
% 14.96/2.56 ![VAR_V_143,VAR_V_144]: (~pred_attacker(tuple_key_register_server_in_1(VAR_V_143,VAR_V_144))|pred_attacker(VAR_V_143))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f119])).
% 14.96/2.56 fof(f340,plain,(
% 14.96/2.56 ![VAR_V_143]: ((![VAR_V_144]: ~pred_attacker(tuple_key_register_server_in_1(VAR_V_143,VAR_V_144)))|pred_attacker(VAR_V_143))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f339])).
% 14.96/2.56 fof(f341,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(tuple_key_register_server_in_1(X0,X1))|pred_attacker(X0))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f340])).
% 14.96/2.56 fof(f356,plain,(
% 14.96/2.56 ![VAR_V_181,VAR_V_182]: ((~pred_attacker(VAR_V_181)|~pred_attacker(VAR_V_182))|pred_attacker(constr_ecb_enc_1(VAR_V_181,VAR_V_182)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f127])).
% 14.96/2.56 fof(f357,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_enc_1(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f356])).
% 14.96/2.56 fof(f362,plain,(
% 14.96/2.56 ![VAR_V_193,VAR_V_194]: ((~pred_attacker(VAR_V_193)|~pred_attacker(VAR_V_194))|pred_attacker(constr_ecb_dec_2(VAR_V_193,VAR_V_194)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f130])).
% 14.96/2.56 fof(f363,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_dec_2(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f362])).
% 14.96/2.56 fof(f370,plain,(
% 14.96/2.56 ![VAR_V_20X307]: (~pred_attacker(tuple_client_B_out_6(VAR_V_20X307))|pred_attacker(VAR_V_20X307))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f134])).
% 14.96/2.56 fof(f371,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(tuple_client_B_out_6(X0))|pred_attacker(X0))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f370])).
% 14.96/2.56 fof(f374,plain,(
% 14.96/2.56 ![VAR_V_213]: (~pred_attacker(tuple_client_B_out_4(VAR_V_213))|pred_attacker(VAR_V_213))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f136])).
% 14.96/2.56 fof(f375,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(tuple_client_B_out_4(X0))|pred_attacker(X0))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f374])).
% 14.96/2.56 fof(f384,plain,(
% 14.96/2.56 ![VAR_V_232]: (~pred_attacker(VAR_V_232)|pred_attacker(tuple_client_B_in_5(VAR_V_232)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 14.96/2.56 fof(f385,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_5(X0)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f384])).
% 14.96/2.56 fof(f388,plain,(
% 14.96/2.56 ![VAR_V_238]: (~pred_attacker(VAR_V_238)|pred_attacker(tuple_client_B_in_3(VAR_V_238)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 14.96/2.56 fof(f389,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_3(X0)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f388])).
% 14.96/2.56 fof(f392,plain,(
% 14.96/2.56 ![VAR_V_244]: (~pred_attacker(VAR_V_244)|pred_attacker(tuple_client_B_in_2(VAR_V_244)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f144])).
% 14.96/2.56 fof(f393,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_2(X0)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f392])).
% 14.96/2.56 fof(f422,plain,(
% 14.96/2.56 pred_attacker(constr_CONST_4)),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f158])).
% 14.96/2.56 fof(f446,plain,(
% 14.96/2.56 ![VAR_V_367,VAR_V_368,VAR_V_369]: (~pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369))|pred_attacker(VAR_V_368))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f170])).
% 14.96/2.56 fof(f447,plain,(
% 14.96/2.56 ![VAR_V_368]: ((![VAR_V_367,VAR_V_369]: ~pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369)))|pred_attacker(VAR_V_368))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f446])).
% 14.96/2.56 fof(f448,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(tuple_3(X0,X1,X2))|pred_attacker(X1))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f447])).
% 14.96/2.56 fof(f452,plain,(
% 14.96/2.56 ![VAR_V_377,VAR_V_378]: ((~pred_attacker(VAR_V_377)|~pred_attacker(VAR_V_378))|pred_attacker(tuple_2(VAR_V_377,VAR_V_378)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f172])).
% 14.96/2.56 fof(f453,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_2(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f452])).
% 14.96/2.56 fof(f457,plain,(
% 14.96/2.56 ![VAR_V_388,VAR_V_389]: (~pred_attacker(tuple_2(VAR_V_388,VAR_V_389))|pred_attacker(VAR_V_389))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f174])).
% 14.96/2.56 fof(f458,plain,(
% 14.96/2.56 ![VAR_V_389]: ((![VAR_V_388]: ~pred_attacker(tuple_2(VAR_V_388,VAR_V_389)))|pred_attacker(VAR_V_389))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f457])).
% 14.96/2.56 fof(f459,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(tuple_2(X0,X1))|pred_attacker(X1))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f458])).
% 14.96/2.56 fof(f466,plain,(
% 14.96/2.56 pred_attacker(name_I)),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f178])).
% 14.96/2.56 fof(f473,plain,(
% 14.96/2.56 pred_attacker(tuple_out_1(constr_pkey(name_skA)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f185])).
% 14.96/2.56 fof(f484,plain,(
% 14.96/2.56 ![VAR_0X40SID_688,VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687)))|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS)))))))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f192])).
% 14.96/2.56 fof(f485,plain,(
% 14.96/2.56 ![VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687)))|(![VAR_0X40SID_688]: pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))))))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f484])).
% 14.96/2.56 fof(f486,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X0,name_skB)))|~pred_attacker(tuple_client_B_in_3(X0))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))|~pred_attacker(tuple_client_B_in_2(X1))|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f485])).
% 14.96/2.56 fof(f487,plain,(
% 14.96/2.56 ![VAR_0X40SID_718,VAR_ECB_ENC_NA_A_720X30,VAR_ECB_ENC_NB_719,VAR_SIGN_A_PKA_721]: ((((((~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB))|~pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721)))|pred_attacker(tuple_client_B_out_6(name_objective)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f193])).
% 14.96/2.56 fof(f488,plain,(
% 14.96/2.56 (![VAR_SIGN_A_PKA_721]: (((![VAR_ECB_ENC_NA_A_720X30]: (((![VAR_ECB_ENC_NB_719]: ((![VAR_0X40SID_718]: ~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB)))|~pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721))))|pred_attacker(tuple_client_B_out_6(name_objective))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f487])).
% 14.96/2.56 fof(f489,plain,(
% 14.96/2.56 ![X0,X1,X2,X3]: (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X2,name_skB)))|~pred_attacker(tuple_client_B_in_3(X2))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))|~pred_attacker(tuple_client_B_in_2(X3))|pred_attacker(tuple_client_B_out_6(name_objective)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f488])).
% 14.96/2.56 fof(f490,plain,(
% 14.96/2.56 ![VAR_DST_760X30,VAR_PKDST_761,VAR_SRC_762]: ((~pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761))|~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30)))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS))))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f194])).
% 14.96/2.56 fof(f491,plain,(
% 14.96/2.56 ![VAR_DST_760X30,VAR_PKDST_761]: ((~pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761))|(![VAR_SRC_762]: ~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30))))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS))))),
% 14.96/2.56 inference(miniscoping,[status(thm)],[f490])).
% 14.96/2.56 fof(f492,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_table(tuple_keys(X0,X1))|~pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f491])).
% 14.96/2.56 fof(f493,plain,(
% 14.96/2.56 ![VAR_HOST_814,VAR_PK_815]: (((VAR_HOST_814=name_B|VAR_HOST_814=name_A)|~pred_attacker(tuple_key_register_server_in_1(VAR_HOST_814,VAR_PK_815)))|pred_table(tuple_keys(VAR_HOST_814,VAR_PK_815)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f195])).
% 14.96/2.56 fof(f494,plain,(
% 14.96/2.56 ![X0,X1]: (X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|pred_table(tuple_keys(X0,X1)))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f493])).
% 14.96/2.56 fof(f495,plain,(
% 14.96/2.56 (?[VAR_V_823]: ~pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)))),
% 14.96/2.56 inference(pre_NNF_transformation,[status(thm)],[f197])).
% 14.96/2.56 fof(f496,plain,(
% 14.96/2.56 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 14.96/2.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VAR_V_823,sK0_skl)],[f495])).
% 14.96/2.56 fof(f497,plain,(
% 14.96/2.56 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 14.96/2.56 inference(cnf_transformation,[status(thm)],[f496])).
% 14.96/2.56 fof(f498,definition,(
% 14.96/2.56 ![X0,X1]: (sQ0_spl <=> (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f499,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))|~sQ0_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f498])).
% 14.96/2.56 fof(f501,definition,(
% 14.96/2.56 ![X2]: (sQ1_spl <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X2,name_skB)))|~pred_attacker(tuple_client_B_in_3(X2))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f502,plain,(
% 14.96/2.56 ![X0]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X0,name_skB)))|~pred_attacker(tuple_client_B_in_3(X0))|~sQ1_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f501])).
% 14.96/2.56 fof(f504,definition,(
% 14.96/2.56 ![X3]: (sQ2_spl <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))|~pred_attacker(tuple_client_B_in_2(X3))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f505,plain,(
% 14.96/2.56 ![X0]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS))))|~pred_attacker(tuple_client_B_in_2(X0))|~sQ2_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f504])).
% 14.96/2.56 fof(f507,definition,(
% 14.96/2.56 sQ3_spl <=> (pred_attacker(tuple_client_B_out_6(name_objective)))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f508,plain,(
% 14.96/2.56 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ3_spl),
% 14.96/2.56 inference(component_clause,[status(thm)],[f507])).
% 14.96/2.56 fof(f510,plain,(
% 14.96/2.56 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f489,f498,f501,f504,f507])).
% 14.96/2.56 fof(f511,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,tuple_client_B_out_6(name_objective)))|~sQ3_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f453,f508])).
% 14.96/2.56 fof(f512,plain,(
% 14.96/2.56 pred_attacker(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)))|~sQ3_spl),
% 14.96/2.56 inference(resolution,[status(thm)],[f511,f508])).
% 14.96/2.56 fof(f515,plain,(
% 14.96/2.56 pred_attacker(tuple_2(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)),tuple_client_B_out_6(name_objective)))|~sQ3_spl),
% 14.96/2.56 inference(resolution,[status(thm)],[f512,f511])).
% 14.96/2.56 fof(f520,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,tuple_2(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)),tuple_client_B_out_6(name_objective))))|~sQ3_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f515,f453])).
% 14.96/2.56 fof(f534,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)),tuple_client_B_out_6(name_objective)))|~sQ3_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f520,f459])).
% 14.96/2.56 fof(f539,definition,(
% 14.96/2.56 ![X0]: (sQ4_spl <=> (~pred_attacker(X0)))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f540,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~sQ4_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f539])).
% 14.96/2.56 fof(f542,definition,(
% 14.96/2.56 sQ5_spl <=> (pred_attacker(tuple_2(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)),tuple_client_B_out_6(name_objective))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f543,plain,(
% 14.96/2.56 pred_attacker(tuple_2(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)),tuple_client_B_out_6(name_objective)))|~sQ5_spl),
% 14.96/2.56 inference(component_clause,[status(thm)],[f542])).
% 14.96/2.56 fof(f545,plain,(
% 14.96/2.56 sQ4_spl|sQ5_spl|~sQ3_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f534,f539,f542,f507])).
% 14.96/2.56 fof(f546,plain,(
% 14.96/2.56 $false|~sQ4_spl),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f466,f540])).
% 14.96/2.56 fof(f547,plain,(
% 14.96/2.56 ~sQ4_spl),
% 14.96/2.56 inference(contradiction_clause,[status(thm)],[f546])).
% 14.96/2.56 fof(f558,definition,(
% 14.96/2.56 sQ7_spl <=> (pred_attacker(name_objective))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f560,plain,(
% 14.96/2.56 ~pred_attacker(name_objective)|sQ7_spl),
% 14.96/2.56 inference(component_clause,[status(thm)],[f558])).
% 14.96/2.56 fof(f568,plain,(
% 14.96/2.56 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ5_spl),
% 14.96/2.56 inference(resolution,[status(thm)],[f543,f459])).
% 14.96/2.56 fof(f569,plain,(
% 14.96/2.56 pred_attacker(name_objective)|~sQ5_spl),
% 14.96/2.56 inference(resolution,[status(thm)],[f568,f371])).
% 14.96/2.56 fof(f570,plain,(
% 14.96/2.56 $false|sQ7_spl|~sQ5_spl),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f569,f560])).
% 14.96/2.56 fof(f571,plain,(
% 14.96/2.56 sQ7_spl|~sQ5_spl),
% 14.96/2.56 inference(contradiction_clause,[status(thm)],[f570])).
% 14.96/2.56 fof(f574,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS))))|~sQ2_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f393,f505])).
% 14.96/2.56 fof(f610,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~sQ2_spl)),
% 14.96/2.56 inference(backward_subsumption_resolution,[status(thm)],[f574,f293])).
% 14.96/2.56 fof(f611,plain,(
% 14.96/2.56 sQ4_spl|~sQ2_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f610,f539,f504])).
% 14.96/2.56 fof(f612,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(tuple_client_B_in_3(X0))|~sQ1_spl)),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f502,f293])).
% 14.96/2.56 fof(f613,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(tuple_client_B_in_3(X0))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))|~pred_attacker(tuple_client_B_in_2(X1))|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f486,f293])).
% 14.96/2.56 fof(f614,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~sQ1_spl)),
% 14.96/2.56 inference(backward_subsumption_resolution,[status(thm)],[f389,f612])).
% 14.96/2.56 fof(f615,plain,(
% 14.96/2.56 sQ4_spl|~sQ1_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f614,f539,f501])).
% 14.96/2.56 fof(f616,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(tuple_client_B_in_5(X0))|~sQ0_spl)),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f499,f293])).
% 14.96/2.56 fof(f617,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~sQ0_spl)),
% 14.96/2.56 inference(backward_subsumption_resolution,[status(thm)],[f385,f616])).
% 14.96/2.56 fof(f618,plain,(
% 14.96/2.56 sQ4_spl|~sQ0_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f617,f539,f498])).
% 14.96/2.56 fof(f634,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(tuple_client_B_in_3(X0))|~pred_attacker(tuple_client_B_in_2(X1))|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f613,f293])).
% 14.96/2.56 fof(f638,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(tuple_client_B_in_2(X1))|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 14.96/2.56 inference(resolution,[status(thm)],[f389,f634])).
% 14.96/2.56 fof(f668,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X1),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))|~pred_attacker(X2))),
% 14.96/2.56 inference(resolution,[status(thm)],[f638,f393])).
% 14.96/2.56 fof(f679,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))),
% 14.96/2.56 inference(resolution,[status(thm)],[f668,f375])).
% 14.96/2.56 fof(f706,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(constr_ecb_enc_2(X0,X1,constr_pkey(X2)))|~pred_attacker(X2)|pred_attacker(tuple_2(X0,X1)))),
% 14.96/2.56 inference(paramodulation,[status(thm)],[f281,f363])).
% 14.96/2.56 fof(f750,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(constr_ecb_enc_1(X0,X1))|~pred_attacker(constr_ecb_enc_1(X2,X1))|pred_attacker(constr_ecb_enc_2(X0,X2,X1)))),
% 14.96/2.56 inference(paramodulation,[status(thm)],[f285,f453])).
% 14.96/2.56 fof(f758,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(constr_ecb_enc_1(X0,X1))|pred_attacker(constr_ecb_enc_2(X0,X2,X1))|~pred_attacker(X2)|~pred_attacker(X1))),
% 14.96/2.56 inference(resolution,[status(thm)],[f750,f357])).
% 14.96/2.56 fof(f762,definition,(
% 14.96/2.56 ![X0]: (sQ22_spl <=> (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f763,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))|~sQ22_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f762])).
% 14.96/2.56 fof(f800,plain,(
% 14.96/2.56 ![X0,X1,X2,X3]: (~pred_attacker(constr_ecb_enc_3(X0,X1,X2,X3))|pred_attacker(constr_ecb_enc_1(X1,X3)))),
% 14.96/2.56 inference(paramodulation,[status(thm)],[f284,f448])).
% 14.96/2.56 fof(f846,plain,(
% 14.96/2.56 ![X0,X1,X2]: (pred_attacker(constr_ecb_enc_1(name_Nb(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))|~pred_attacker(X2)|~pred_attacker(X1))),
% 14.96/2.56 inference(resolution,[status(thm)],[f800,f679])).
% 14.96/2.56 fof(f849,definition,(
% 14.96/2.56 ![X0,X1]: (sQ24_spl <=> (pred_attacker(constr_ecb_enc_1(name_Nb(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))|~pred_attacker(X1)))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f850,plain,(
% 14.96/2.56 ![X0,X1]: (pred_attacker(constr_ecb_enc_1(name_Nb(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))|~pred_attacker(X1)|~sQ24_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f849])).
% 14.96/2.56 fof(f852,plain,(
% 14.96/2.56 sQ24_spl|sQ4_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f846,f849,f539])).
% 14.96/2.56 fof(f877,plain,(
% 14.96/2.56 ![X0]: (~pred_attacker(X0)|~sQ22_spl)),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f763,f312])).
% 14.96/2.56 fof(f878,plain,(
% 14.96/2.56 $false|~sQ22_spl),
% 14.96/2.56 inference(backward_subsumption_resolution,[status(thm)],[f473,f877])).
% 14.96/2.56 fof(f910,plain,(
% 14.96/2.56 ~sQ22_spl),
% 14.96/2.56 inference(contradiction_clause,[status(thm)],[f878])).
% 14.96/2.56 fof(f935,plain,(
% 14.96/2.56 ![X0,X1]: (pred_attacker(constr_ecb_enc_1(name_Nb(X0),constr_tuple_2_get_1_bitstring(X1)))|~pred_attacker(constr_sign(X1,name_skS))|~sQ24_spl)),
% 14.96/2.56 inference(paramodulation,[status(thm)],[f278,f850])).
% 14.96/2.56 fof(f1000,plain,(
% 14.96/2.56 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|~pred_table(tuple_keys(X1,X2))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X1,X2),name_skS))))),
% 14.96/2.56 inference(resolution,[status(thm)],[f330,f492])).
% 14.96/2.56 fof(f1001,definition,(
% 14.96/2.56 ![X1,X2]: (sQ27_spl <=> (~pred_attacker(X1)|~pred_table(tuple_keys(X1,X2))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X1,X2),name_skS)))))),
% 14.96/2.56 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 14.96/2.56 fof(f1002,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_table(tuple_keys(X0,X1))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))|~sQ27_spl)),
% 14.96/2.56 inference(component_clause,[status(thm)],[f1001])).
% 14.96/2.56 fof(f1004,plain,(
% 14.96/2.56 sQ4_spl|sQ27_spl),
% 14.96/2.56 inference(split_clause,[status(thm)],[f1000,f539,f1001])).
% 14.96/2.56 fof(f1335,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|~pred_table(tuple_keys(X0,X1))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~sQ27_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f1002,f328])).
% 14.96/2.56 fof(f1339,plain,(
% 14.96/2.56 ![X0,X1]: (~pred_attacker(X0)|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|~sQ27_spl)),
% 14.96/2.56 inference(resolution,[status(thm)],[f1335,f494])).
% 14.96/2.56 fof(f1354,plain,(
% 14.96/2.56 ![X0,X1]: (pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|~sQ27_spl)),
% 14.96/2.56 inference(forward_subsumption_resolution,[status(thm)],[f1339,f341])).
% 14.96/2.58 fof(f1583,definition,(
% 14.96/2.58 ![X0,X1]: (sQ81_spl <=> (~pred_attacker(X0)|pred_attacker(tuple_2(name_Nb(X1),X0))))),
% 14.96/2.58 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 14.96/2.58 fof(f1584,plain,(
% 14.96/2.58 ![X0,X1]: (~pred_attacker(X0)|pred_attacker(tuple_2(name_Nb(X1),X0))|~sQ81_spl)),
% 14.96/2.58 inference(component_clause,[status(thm)],[f1583])).
% 14.96/2.58 fof(f2313,plain,(
% 14.96/2.58 ![X0,X1]: (pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|~sQ27_spl)),
% 14.96/2.58 inference(resolution,[status(thm)],[f1354,f338])).
% 14.96/2.58 fof(f2494,plain,(
% 14.96/2.58 ![X0,X1,X2]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(tuple_2(X0,X1))))|~sQ27_spl|~sQ24_spl)),
% 14.96/2.58 inference(resolution,[status(thm)],[f2313,f935])).
% 14.96/2.58 fof(f2522,plain,(
% 14.96/2.58 ![X0,X1,X2]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_enc_1(name_Nb(X2),X1))|~sQ27_spl|~sQ24_spl)),
% 14.96/2.58 inference(forward_demodulation,[status(thm)],[f287,f2494])).
% 14.96/2.58 fof(f2532,definition,(
% 14.96/2.58 ![X0]: (sQ164_spl <=> (X0=name_B|X0=name_A|~pred_attacker(X0)))),
% 14.96/2.58 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 14.96/2.58 fof(f2533,plain,(
% 14.96/2.58 ![X0]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~sQ164_spl)),
% 14.96/2.58 inference(component_clause,[status(thm)],[f2532])).
% 14.96/2.58 fof(f2577,plain,(
% 14.96/2.58 constr_CONST_4=name_B|constr_CONST_4=name_A|~sQ164_spl),
% 14.96/2.58 inference(resolution,[status(thm)],[f2533,f422])).
% 14.96/2.58 fof(f2783,definition,(
% 14.96/2.58 sQ181_spl <=> (constr_CONST_4=name_B)),
% 14.96/2.58 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 14.96/2.58 fof(f2784,plain,(
% 14.96/2.58 constr_CONST_4=name_B|~sQ181_spl),
% 14.96/2.58 inference(component_clause,[status(thm)],[f2783])).
% 14.96/2.58 fof(f2786,definition,(
% 14.96/2.58 sQ182_spl <=> (constr_CONST_4=name_A)),
% 14.96/2.58 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 14.96/2.58 fof(f2787,plain,(
% 14.96/2.58 constr_CONST_4=name_A|~sQ182_spl),
% 14.96/2.58 inference(component_clause,[status(thm)],[f2786])).
% 14.96/2.58 fof(f2789,plain,(
% 14.96/2.58 sQ181_spl|sQ182_spl|~sQ164_spl),
% 14.96/2.58 inference(split_clause,[status(thm)],[f2577,f2783,f2786,f2532])).
% 14.96/2.58 fof(f3048,plain,(
% 14.96/2.58 $false|~sQ181_spl),
% 14.96/2.58 inference(forward_subsumption_resolution,[status(thm)],[f2784,f241])).
% 14.96/2.58 fof(f3049,plain,(
% 14.96/2.58 ~sQ181_spl),
% 14.96/2.58 inference(contradiction_clause,[status(thm)],[f3048])).
% 14.96/2.58 fof(f3064,plain,(
% 14.96/2.58 $false|~sQ182_spl),
% 14.96/2.58 inference(forward_subsumption_resolution,[status(thm)],[f2787,f240])).
% 14.96/2.58 fof(f3065,plain,(
% 14.96/2.58 ~sQ182_spl),
% 14.96/2.58 inference(contradiction_clause,[status(thm)],[f3064])).
% 14.96/2.58 fof(f3538,plain,(
% 14.96/2.58 ![X0,X1,X2,X3]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_ecb_enc_2(name_Nb(X2),X3,X1))|~pred_attacker(X3)|~pred_attacker(X1)|~sQ27_spl|~sQ24_spl)),
% 14.96/2.58 inference(resolution,[status(thm)],[f2522,f758])).
% 14.96/2.58 fof(f3561,definition,(
% 14.96/2.58 ![X1,X2,X3]: (sQ298_spl <=> (~pred_attacker(X1)|pred_attacker(constr_ecb_enc_2(name_Nb(X2),X3,X1))|~pred_attacker(X3)|~pred_attacker(X1)))),
% 14.96/2.58 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 14.96/2.58 fof(f3562,plain,(
% 14.96/2.58 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(constr_ecb_enc_2(name_Nb(X1),X2,X0))|~pred_attacker(X2)|~pred_attacker(X0)|~sQ298_spl)),
% 14.96/2.58 inference(component_clause,[status(thm)],[f3561])).
% 14.96/2.58 fof(f3564,plain,(
% 14.96/2.58 sQ164_spl|sQ298_spl|~sQ27_spl|~sQ24_spl),
% 14.96/2.58 inference(split_clause,[status(thm)],[f3538,f2532,f3561,f1001,f849])).
% 14.96/2.58 fof(f3569,plain,(
% 14.96/2.58 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(constr_ecb_enc_2(name_Nb(X1),X2,X0))|~pred_attacker(X2)|~sQ298_spl)),
% 14.96/2.58 inference(duplicate_literals_removal,[status(thm)],[f3562])).
% 14.96/2.58 fof(f3576,plain,(
% 14.96/2.58 ![X0,X1,X2]: (~pred_attacker(constr_pkey(X0))|~pred_attacker(X1)|~pred_attacker(X0)|pred_attacker(tuple_2(name_Nb(X2),X1))|~sQ298_spl)),
% 14.96/2.58 inference(resolution,[status(thm)],[f3569,f706])).
% 14.96/2.58 fof(f3585,plain,(
% 14.96/2.58 sQ22_spl|sQ81_spl|~sQ298_spl),
% 14.96/2.58 inference(split_clause,[status(thm)],[f3576,f762,f1583,f3561])).
% 14.96/2.58 fof(f3601,plain,(
% 14.96/2.58 ~pred_attacker(name_objective)|~sQ81_spl),
% 14.96/2.58 inference(resolution,[status(thm)],[f1584,f497])).
% 14.96/2.58 fof(f3604,plain,(
% 14.96/2.58 ~sQ7_spl|~sQ81_spl),
% 14.96/2.58 inference(split_clause,[status(thm)],[f3601,f558,f1583])).
% 14.96/2.58 fof(f3606,plain,(
% 14.96/2.58 $false),
% 14.96/2.58 inference(sat_refutation,[status(thm)],[f510,f545,f547,f571,f611,f615,f618,f852,f910,f1004,f2789,f3049,f3065,f3564,f3585,f3604])).
% 14.96/2.58 % SZS output end CNFRefutation for theBenchmark.p
% 15.29/2.61 % Elapsed time: 2.231512 seconds
% 15.29/2.61 % CPU time: 17.177667 seconds
% 15.29/2.61 % Total memory used: 244.048 MB
% 15.29/2.61 % Net memory used: 228.544 MB
%------------------------------------------------------------------------------