%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW960+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 : n016.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 1.03s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW960+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.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 10:25:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 1.03/0.71 % Refutation found
% 1.03/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.03/0.71 % SZS output start CNFRefutation for theBenchmark
% 1.03/0.71 fof(f43,axiom,(
% 1.03/0.71 constr_CONST_4 != name_A ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f44,axiom,(
% 1.03/0.71 constr_CONST_4 != name_B ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f79,axiom,(
% 1.03/0.71 (! [VAR_K_18,VAR_M_17] : constr_adec(constr_aenc(VAR_M_17,constr_pkey(VAR_K_18)),VAR_K_18) = VAR_M_17 )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f82,axiom,(
% 1.03/0.71 (! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30 )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f83,axiom,(
% 1.03/0.71 (! [VAR_X0X30_11,VAR_X1_12] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12 )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f87,axiom,(
% 1.03/0.71 (! [VAR_X_36,VAR_Y_37] : pred_eq_bitstring_bitstring(VAR_X_36,VAR_Y_37) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f94,axiom,(
% 1.03/0.71 (! [VAR_V_55] :( pred_attacker(VAR_V_55)=> pred_attacker(constr_pkey(VAR_V_55)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f102,axiom,(
% 1.03/0.71 (! [VAR_V_79] :( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_79))=> pred_attacker(VAR_V_79) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f103,axiom,(
% 1.03/0.71 (! [VAR_V_83,VAR_V_84] :( ( pred_attacker(VAR_V_83)& pred_attacker(VAR_V_84) )=> pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_83,VAR_V_84)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f106,axiom,(
% 1.03/0.71 (! [VAR_V_99,VAR_V_10X300X30] :( ( pred_attacker(VAR_V_99)& pred_attacker(VAR_V_10X300X30) )=> pred_attacker(tuple_key_register_server_in_1(VAR_V_99,VAR_V_10X300X30)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f107,axiom,(
% 1.03/0.71 (! [VAR_V_10X307,VAR_V_10X308] :( pred_attacker(tuple_key_register_server_in_1(VAR_V_10X307,VAR_V_10X308))=> pred_attacker(VAR_V_10X307) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f114,axiom,(
% 1.03/0.71 (! [VAR_V_127] :( pred_attacker(tuple_client_B_out_6(VAR_V_127))=> pred_attacker(VAR_V_127) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f116,axiom,(
% 1.03/0.71 (! [VAR_V_133] :( pred_attacker(tuple_client_B_out_4(VAR_V_133))=> pred_attacker(VAR_V_133) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f120,axiom,(
% 1.03/0.71 (! [VAR_V_152] :( pred_attacker(VAR_V_152)=> pred_attacker(tuple_client_B_in_5(VAR_V_152)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f122,axiom,(
% 1.03/0.71 (! [VAR_V_158] :( pred_attacker(VAR_V_158)=> pred_attacker(tuple_client_B_in_3(VAR_V_158)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f124,axiom,(
% 1.03/0.71 (! [VAR_V_164] :( pred_attacker(VAR_V_164)=> pred_attacker(tuple_client_B_in_2(VAR_V_164)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f139,axiom,(
% 1.03/0.71 (! [VAR_V_219,VAR_V_220X30] :( ( pred_attacker(VAR_V_219)& pred_attacker(VAR_V_220X30) )=> pred_attacker(constr_adec(VAR_V_219,VAR_V_220X30)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f140,axiom,(
% 1.03/0.71 pred_attacker(constr_CONST_4) ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f145,axiom,(
% 1.03/0.71 (! [VAR_V_227,VAR_V_228] :( ( pred_attacker(VAR_V_227)& pred_attacker(VAR_V_228) )=> pred_attacker(tuple_2(VAR_V_227,VAR_V_228)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f147,axiom,(
% 1.03/0.71 (! [VAR_V_238,VAR_V_239] :( pred_attacker(tuple_2(VAR_V_238,VAR_V_239))=> pred_attacker(VAR_V_239) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f150,axiom,(
% 1.03/0.71 pred_attacker(name_c) ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f151,axiom,(
% 1.03/0.71 pred_attacker(name_I) ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f153,axiom,(
% 1.03/0.71 pred_attacker(name_A) ),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f165,axiom,(
% 1.03/0.71 (! [VAR_0X40SID_524,VAR_AENC_NA_A_522,VAR_SIGN_A_PKA_523] :( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_522,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_522))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523)) )=> pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_522,name_skB)),name_Nb(VAR_0X40SID_524)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS)))))) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f166,axiom,(
% 1.03/0.71 (! [VAR_0X40SID_546,VAR_AENC_NA_A_548,VAR_AENC_NB_547,VAR_SIGN_A_PKA_549] :( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB))& pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_547))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_548,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_548))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_549,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549)) )=> pred_attacker(tuple_client_B_out_6(name_objective)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f167,axiom,(
% 1.03/0.71 (! [VAR_DST_588,VAR_PKDST_589,VAR_SRC_590X30] :( ( pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589))& pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588)) )=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS))) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f168,axiom,(
% 1.03/0.71 (! [VAR_HOST_642,VAR_PK_643] :( ( VAR_HOST_642 != name_B& VAR_HOST_642 != name_A& pred_attacker(tuple_key_register_server_in_1(VAR_HOST_642,VAR_PK_643)) )=> pred_table(tuple_keys(VAR_HOST_642,VAR_PK_643)) ) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f169,conjecture,(
% 1.03/0.71 (! [VAR_V_651] : pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)) )),
% 1.03/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.71 fof(f170,negated_conjecture,(
% 1.03/0.71 ~((! [VAR_V_651] : pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)) ))),
% 1.03/0.71 inference(negated_conjecture,[status(cth)],[f169])).
% 1.03/0.71 fof(f213,plain,(
% 1.03/0.71 ~constr_CONST_4=name_A),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f43])).
% 1.03/0.71 fof(f214,plain,(
% 1.03/0.71 ~constr_CONST_4=name_B),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f44])).
% 1.03/0.71 fof(f249,plain,(
% 1.03/0.71 ![X0,X1]: (constr_adec(constr_aenc(X0,constr_pkey(X1)),X1)=X0)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f79])).
% 1.03/0.71 fof(f252,plain,(
% 1.03/0.71 ![X0,X1]: (constr_checksign(constr_sign(X0,X1),constr_pkey(X1))=X0)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f82])).
% 1.03/0.71 fof(f253,plain,(
% 1.03/0.71 ![X0,X1]: (constr_tuple_2_get_1_bitstring(tuple_2(X0,X1))=X1)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f83])).
% 1.03/0.71 fof(f257,plain,(
% 1.03/0.71 ![X0,X1]: (pred_eq_bitstring_bitstring(X0,X1))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f87])).
% 1.03/0.71 fof(f269,plain,(
% 1.03/0.71 ![VAR_V_55]: (~pred_attacker(VAR_V_55)|pred_attacker(constr_pkey(VAR_V_55)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 1.03/0.71 fof(f270,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_pkey(X0)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f269])).
% 1.03/0.71 fof(f285,plain,(
% 1.03/0.71 ![VAR_V_79]: (~pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_79))|pred_attacker(VAR_V_79))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f102])).
% 1.03/0.71 fof(f286,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(tuple_key_retrieval_server_out_2(X0))|pred_attacker(X0))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f285])).
% 1.03/0.71 fof(f287,plain,(
% 1.03/0.71 ![VAR_V_83,VAR_V_84]: ((~pred_attacker(VAR_V_83)|~pred_attacker(VAR_V_84))|pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_83,VAR_V_84)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 1.03/0.71 fof(f288,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f287])).
% 1.03/0.71 fof(f295,plain,(
% 1.03/0.71 ![VAR_V_99,VAR_V_10X300X30]: ((~pred_attacker(VAR_V_99)|~pred_attacker(VAR_V_10X300X30))|pred_attacker(tuple_key_register_server_in_1(VAR_V_99,VAR_V_10X300X30)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 1.03/0.71 fof(f296,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_register_server_in_1(X0,X1)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f295])).
% 1.03/0.71 fof(f297,plain,(
% 1.03/0.71 ![VAR_V_10X307,VAR_V_10X308]: (~pred_attacker(tuple_key_register_server_in_1(VAR_V_10X307,VAR_V_10X308))|pred_attacker(VAR_V_10X307))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 1.03/0.71 fof(f298,plain,(
% 1.03/0.71 ![VAR_V_10X307]: ((![VAR_V_10X308]: ~pred_attacker(tuple_key_register_server_in_1(VAR_V_10X307,VAR_V_10X308)))|pred_attacker(VAR_V_10X307))),
% 1.03/0.71 inference(miniscoping,[status(thm)],[f297])).
% 1.03/0.71 fof(f299,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(tuple_key_register_server_in_1(X0,X1))|pred_attacker(X0))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f298])).
% 1.03/0.71 fof(f312,plain,(
% 1.03/0.71 ![VAR_V_127]: (~pred_attacker(tuple_client_B_out_6(VAR_V_127))|pred_attacker(VAR_V_127))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 1.03/0.71 fof(f313,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(tuple_client_B_out_6(X0))|pred_attacker(X0))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f312])).
% 1.03/0.71 fof(f316,plain,(
% 1.03/0.71 ![VAR_V_133]: (~pred_attacker(tuple_client_B_out_4(VAR_V_133))|pred_attacker(VAR_V_133))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 1.03/0.71 fof(f317,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(tuple_client_B_out_4(X0))|pred_attacker(X0))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f316])).
% 1.03/0.71 fof(f326,plain,(
% 1.03/0.71 ![VAR_V_152]: (~pred_attacker(VAR_V_152)|pred_attacker(tuple_client_B_in_5(VAR_V_152)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 1.03/0.71 fof(f327,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_5(X0)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f326])).
% 1.03/0.71 fof(f330,plain,(
% 1.03/0.71 ![VAR_V_158]: (~pred_attacker(VAR_V_158)|pred_attacker(tuple_client_B_in_3(VAR_V_158)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f122])).
% 1.03/0.71 fof(f331,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_3(X0)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f330])).
% 1.03/0.71 fof(f334,plain,(
% 1.03/0.71 ![VAR_V_164]: (~pred_attacker(VAR_V_164)|pred_attacker(tuple_client_B_in_2(VAR_V_164)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 1.03/0.71 fof(f335,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_2(X0)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f334])).
% 1.03/0.71 fof(f366,plain,(
% 1.03/0.71 ![VAR_V_219,VAR_V_220X30]: ((~pred_attacker(VAR_V_219)|~pred_attacker(VAR_V_220X30))|pred_attacker(constr_adec(VAR_V_219,VAR_V_220X30)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f139])).
% 1.03/0.71 fof(f367,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_adec(X0,X1)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f366])).
% 1.03/0.71 fof(f368,plain,(
% 1.03/0.71 pred_attacker(constr_CONST_4)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f140])).
% 1.03/0.71 fof(f373,plain,(
% 1.03/0.71 ![VAR_V_227,VAR_V_228]: ((~pred_attacker(VAR_V_227)|~pred_attacker(VAR_V_228))|pred_attacker(tuple_2(VAR_V_227,VAR_V_228)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f145])).
% 1.03/0.71 fof(f374,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_2(X0,X1)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f373])).
% 1.03/0.71 fof(f378,plain,(
% 1.03/0.71 ![VAR_V_238,VAR_V_239]: (~pred_attacker(tuple_2(VAR_V_238,VAR_V_239))|pred_attacker(VAR_V_239))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f147])).
% 1.03/0.71 fof(f379,plain,(
% 1.03/0.71 ![VAR_V_239]: ((![VAR_V_238]: ~pred_attacker(tuple_2(VAR_V_238,VAR_V_239)))|pred_attacker(VAR_V_239))),
% 1.03/0.71 inference(miniscoping,[status(thm)],[f378])).
% 1.03/0.71 fof(f380,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(tuple_2(X0,X1))|pred_attacker(X1))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f379])).
% 1.03/0.71 fof(f386,plain,(
% 1.03/0.71 pred_attacker(name_c)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f150])).
% 1.03/0.71 fof(f387,plain,(
% 1.03/0.71 pred_attacker(name_I)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f151])).
% 1.03/0.71 fof(f389,plain,(
% 1.03/0.71 pred_attacker(name_A)),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f153])).
% 1.03/0.71 fof(f405,plain,(
% 1.03/0.71 ![VAR_0X40SID_524,VAR_AENC_NA_A_522,VAR_SIGN_A_PKA_523]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_522,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_522)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523)))|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_522,name_skB)),name_Nb(VAR_0X40SID_524)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS)))))))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f165])).
% 1.03/0.71 fof(f406,plain,(
% 1.03/0.71 ![VAR_AENC_NA_A_522,VAR_SIGN_A_PKA_523]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_522,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_522)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523)))|(![VAR_0X40SID_524]: pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_522,name_skB)),name_Nb(VAR_0X40SID_524)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_523,constr_pkey(name_skS))))))))),
% 1.03/0.71 inference(miniscoping,[status(thm)],[f405])).
% 1.03/0.71 fof(f407,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(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_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f406])).
% 1.03/0.71 fof(f408,plain,(
% 1.03/0.71 ![VAR_0X40SID_546,VAR_AENC_NA_A_548,VAR_AENC_NB_547,VAR_SIGN_A_PKA_549]: ((((((~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB))|~pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_547)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_548,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_548)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_549,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549)))|pred_attacker(tuple_client_B_out_6(name_objective)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f166])).
% 1.03/0.71 fof(f409,plain,(
% 1.03/0.71 (![VAR_SIGN_A_PKA_549]: (((![VAR_AENC_NA_A_548]: (((![VAR_AENC_NB_547]: ((![VAR_0X40SID_546]: ~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB)))|~pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_547))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_548,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_548))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_549,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549))))|pred_attacker(tuple_client_B_out_6(name_objective))),
% 1.03/0.71 inference(miniscoping,[status(thm)],[f408])).
% 1.03/0.71 fof(f410,plain,(
% 1.03/0.71 ![X0,X1,X2,X3]: (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(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)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f409])).
% 1.03/0.71 fof(f411,plain,(
% 1.03/0.71 ![VAR_DST_588,VAR_PKDST_589,VAR_SRC_590X30]: ((~pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589))|~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588)))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS))))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f167])).
% 1.03/0.71 fof(f412,plain,(
% 1.03/0.71 ![VAR_DST_588,VAR_PKDST_589]: ((~pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589))|(![VAR_SRC_590X30]: ~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588))))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS))))),
% 1.03/0.71 inference(miniscoping,[status(thm)],[f411])).
% 1.03/0.71 fof(f413,plain,(
% 1.03/0.71 ![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))))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f412])).
% 1.03/0.71 fof(f414,plain,(
% 1.03/0.71 ![VAR_HOST_642,VAR_PK_643]: (((VAR_HOST_642=name_B|VAR_HOST_642=name_A)|~pred_attacker(tuple_key_register_server_in_1(VAR_HOST_642,VAR_PK_643)))|pred_table(tuple_keys(VAR_HOST_642,VAR_PK_643)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f168])).
% 1.03/0.71 fof(f415,plain,(
% 1.03/0.71 ![X0,X1]: (X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|pred_table(tuple_keys(X0,X1)))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f414])).
% 1.03/0.71 fof(f416,plain,(
% 1.03/0.71 (?[VAR_V_651]: ~pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)))),
% 1.03/0.71 inference(pre_NNF_transformation,[status(thm)],[f170])).
% 1.03/0.71 fof(f417,plain,(
% 1.03/0.71 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 1.03/0.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VAR_V_651,sK0_skl)],[f416])).
% 1.03/0.71 fof(f418,plain,(
% 1.03/0.71 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 1.03/0.71 inference(cnf_transformation,[status(thm)],[f417])).
% 1.03/0.71 fof(f419,definition,(
% 1.03/0.71 ![X0,X1]: (sQ0_spl <=> (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f420,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))|~sQ0_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f419])).
% 1.03/0.71 fof(f422,definition,(
% 1.03/0.71 ![X2]: (sQ1_spl <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X2,name_skB)))|~pred_attacker(tuple_client_B_in_3(X2))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f423,plain,(
% 1.03/0.71 ![X0]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB)))|~pred_attacker(tuple_client_B_in_3(X0))|~sQ1_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f422])).
% 1.03/0.71 fof(f425,definition,(
% 1.03/0.71 ![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))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f426,plain,(
% 1.03/0.71 ![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)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f425])).
% 1.03/0.71 fof(f428,definition,(
% 1.03/0.71 sQ3_spl <=> (pred_attacker(tuple_client_B_out_6(name_objective)))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f429,plain,(
% 1.03/0.71 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ3_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f428])).
% 1.03/0.71 fof(f431,plain,(
% 1.03/0.71 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f410,f419,f422,f425,f428])).
% 1.03/0.71 fof(f432,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,tuple_client_B_out_6(name_objective)))|~sQ3_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f374,f429])).
% 1.03/0.71 fof(f434,plain,(
% 1.03/0.71 pred_attacker(tuple_2(name_I,tuple_client_B_out_6(name_objective)))|~sQ3_spl),
% 1.03/0.71 inference(resolution,[status(thm)],[f387,f432])).
% 1.03/0.71 fof(f447,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,tuple_2(name_I,tuple_client_B_out_6(name_objective))))|~sQ3_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f434,f374])).
% 1.03/0.71 fof(f460,definition,(
% 1.03/0.71 ![X0]: (sQ4_spl <=> (~pred_attacker(X0)))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f461,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~sQ4_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f460])).
% 1.03/0.71 fof(f469,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(name_I,tuple_client_B_out_6(name_objective)))|~sQ3_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f447,f380])).
% 1.03/0.71 fof(f473,definition,(
% 1.03/0.71 sQ5_spl <=> (pred_attacker(tuple_2(name_I,tuple_client_B_out_6(name_objective))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f474,plain,(
% 1.03/0.71 pred_attacker(tuple_2(name_I,tuple_client_B_out_6(name_objective)))|~sQ5_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f473])).
% 1.03/0.71 fof(f476,plain,(
% 1.03/0.71 sQ4_spl|sQ5_spl|~sQ3_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f469,f460,f473,f428])).
% 1.03/0.71 fof(f477,plain,(
% 1.03/0.71 $false|~sQ4_spl),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f389,f461])).
% 1.03/0.71 fof(f480,plain,(
% 1.03/0.71 ~sQ4_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f477])).
% 1.03/0.71 fof(f482,plain,(
% 1.03/0.71 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ5_spl),
% 1.03/0.71 inference(resolution,[status(thm)],[f474,f380])).
% 1.03/0.71 fof(f483,plain,(
% 1.03/0.71 ~pred_attacker(name_Nb(sK0_skl))|~pred_attacker(name_objective)),
% 1.03/0.71 inference(resolution,[status(thm)],[f374,f418])).
% 1.03/0.71 fof(f486,definition,(
% 1.03/0.71 sQ6_spl <=> (pred_attacker(name_Nb(sK0_skl)))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f488,plain,(
% 1.03/0.71 ~pred_attacker(name_Nb(sK0_skl))|sQ6_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f486])).
% 1.03/0.71 fof(f489,definition,(
% 1.03/0.71 sQ7_spl <=> (pred_attacker(name_objective))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f491,plain,(
% 1.03/0.71 ~pred_attacker(name_objective)|sQ7_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f489])).
% 1.03/0.71 fof(f492,plain,(
% 1.03/0.71 ~sQ6_spl|~sQ7_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f483,f486,f489])).
% 1.03/0.71 fof(f504,plain,(
% 1.03/0.71 pred_attacker(name_objective)|~sQ5_spl),
% 1.03/0.71 inference(resolution,[status(thm)],[f313,f482])).
% 1.03/0.71 fof(f507,plain,(
% 1.03/0.71 $false|~sQ5_spl|sQ7_spl),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f491,f504])).
% 1.03/0.71 fof(f508,plain,(
% 1.03/0.71 ~sQ5_spl|sQ7_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f507])).
% 1.03/0.71 fof(f537,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS))))|~sQ2_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f335,f426])).
% 1.03/0.71 fof(f587,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~sQ2_spl)),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f537,f257])).
% 1.03/0.71 fof(f588,plain,(
% 1.03/0.71 sQ4_spl|~sQ2_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f587,f460,f425])).
% 1.03/0.71 fof(f589,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(tuple_client_B_in_3(X0))|~sQ1_spl)),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f423,f257])).
% 1.03/0.71 fof(f590,plain,(
% 1.03/0.71 ![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_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f407,f257])).
% 1.03/0.71 fof(f591,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~sQ1_spl)),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f331,f589])).
% 1.03/0.71 fof(f592,plain,(
% 1.03/0.71 sQ4_spl|~sQ1_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f591,f460,f422])).
% 1.03/0.71 fof(f593,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(tuple_client_B_in_5(X0))|~sQ0_spl)),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f420,f257])).
% 1.03/0.71 fof(f594,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~sQ0_spl)),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f327,f593])).
% 1.03/0.71 fof(f595,plain,(
% 1.03/0.71 sQ4_spl|~sQ0_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f594,f460,f419])).
% 1.03/0.71 fof(f598,plain,(
% 1.03/0.71 ![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_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f590,f257])).
% 1.03/0.71 fof(f603,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(tuple_client_B_in_2(X1))|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 1.03/0.71 inference(resolution,[status(thm)],[f331,f598])).
% 1.03/0.71 fof(f610,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(constr_aenc(X0,constr_pkey(X1)))|~pred_attacker(X1)|pred_attacker(X0))),
% 1.03/0.71 inference(paramodulation,[status(thm)],[f249,f367])).
% 1.03/0.71 fof(f621,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))|~pred_attacker(X2))),
% 1.03/0.71 inference(resolution,[status(thm)],[f603,f335])).
% 1.03/0.71 fof(f647,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))),
% 1.03/0.71 inference(resolution,[status(thm)],[f621,f317])).
% 1.03/0.71 fof(f652,definition,(
% 1.03/0.71 ![X0]: (sQ19_spl <=> (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f653,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))|~sQ19_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f652])).
% 1.03/0.71 fof(f709,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(constr_sign(X1,name_skS))|pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(X1))))),
% 1.03/0.71 inference(paramodulation,[status(thm)],[f252,f647])).
% 1.03/0.71 fof(f750,definition,(
% 1.03/0.71 ![X0,X3]: (sQ31_spl <=> (~pred_attacker(X0)|pred_attacker(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X3)))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f751,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|pred_attacker(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1)))|~sQ31_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f750])).
% 1.03/0.71 fof(f758,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_attacker(X0)|pred_attacker(name_Nb(X1))|~sQ31_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f751,f380])).
% 1.03/0.71 fof(f761,definition,(
% 1.03/0.71 ![X1]: (sQ33_spl <=> (pred_attacker(name_Nb(X1))))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f762,plain,(
% 1.03/0.71 ![X0]: (pred_attacker(name_Nb(X0))|~sQ33_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f761])).
% 1.03/0.71 fof(f764,plain,(
% 1.03/0.71 sQ4_spl|sQ33_spl|~sQ31_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f758,f460,f761,f750])).
% 1.03/0.71 fof(f769,plain,(
% 1.03/0.71 ![X0]: (~pred_attacker(X0)|~sQ19_spl)),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f653,f270])).
% 1.03/0.71 fof(f779,plain,(
% 1.03/0.71 $false|~sQ19_spl),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f386,f769])).
% 1.03/0.71 fof(f799,plain,(
% 1.03/0.71 ~sQ19_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f779])).
% 1.03/0.71 fof(f918,plain,(
% 1.03/0.71 $false|~sQ33_spl|sQ6_spl),
% 1.03/0.71 inference(backward_subsumption_resolution,[status(thm)],[f488,f762])).
% 1.03/0.71 fof(f919,plain,(
% 1.03/0.71 ~sQ33_spl|sQ6_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f918])).
% 1.03/0.71 fof(f1000,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_table(tuple_keys(X0,X1))|~pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)))),
% 1.03/0.71 inference(resolution,[status(thm)],[f413,f286])).
% 1.03/0.71 fof(f1018,plain,(
% 1.03/0.71 ![X0,X1,X2]: (~pred_table(tuple_keys(X0,X1))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~pred_attacker(X2)|~pred_attacker(X0))),
% 1.03/0.71 inference(resolution,[status(thm)],[f1000,f288])).
% 1.03/0.71 fof(f1019,definition,(
% 1.03/0.71 ![X0,X1]: (sQ40_spl <=> (~pred_table(tuple_keys(X0,X1))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~pred_attacker(X0)))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f1020,plain,(
% 1.03/0.71 ![X0,X1]: (~pred_table(tuple_keys(X0,X1))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~pred_attacker(X0)|~sQ40_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f1019])).
% 1.03/0.71 fof(f1022,plain,(
% 1.03/0.71 sQ40_spl|sQ4_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f1018,f1019,f460])).
% 1.03/0.71 fof(f1025,plain,(
% 1.03/0.71 ![X0,X1]: (pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~pred_attacker(X0)|X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|~sQ40_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f1020,f415])).
% 1.03/0.71 fof(f1034,plain,(
% 1.03/0.71 ![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))|~sQ40_spl)),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1025,f299])).
% 1.03/0.71 fof(f1123,plain,(
% 1.03/0.71 ![X0,X1]: (pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|~sQ40_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f1034,f296])).
% 1.03/0.71 fof(f1138,plain,(
% 1.03/0.71 ![X0,X1,X2,X3]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X2,name_skB)),name_Nb(X3)),constr_tuple_2_get_1_bitstring(tuple_2(X0,X1))))|~sQ40_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f1123,f709])).
% 1.03/0.71 fof(f1145,plain,(
% 1.03/0.71 ![X0,X1,X2,X3]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(X1)|~pred_attacker(X2)|pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X2,name_skB)),name_Nb(X3)),X1))|~sQ40_spl)),
% 1.03/0.71 inference(forward_demodulation,[status(thm)],[f253,f1138])).
% 1.03/0.71 fof(f1177,definition,(
% 1.03/0.71 ![X1]: (sQ52_spl <=> (X1=name_B|X1=name_A|~pred_attacker(X1)))),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f1178,plain,(
% 1.03/0.71 ![X0]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~sQ52_spl)),
% 1.03/0.71 inference(component_clause,[status(thm)],[f1177])).
% 1.03/0.71 fof(f1192,plain,(
% 1.03/0.71 ![X0,X1,X2,X3]: (X0=name_B|X0=name_A|~pred_attacker(X0)|~pred_attacker(constr_pkey(X1))|~pred_attacker(X2)|~pred_attacker(X1)|pred_attacker(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X2,name_skB)),name_Nb(X3)))|~sQ40_spl)),
% 1.03/0.71 inference(resolution,[status(thm)],[f1145,f610])).
% 1.03/0.71 fof(f1199,plain,(
% 1.03/0.71 sQ52_spl|sQ19_spl|sQ31_spl|~sQ40_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f1192,f1177,f652,f750,f1019])).
% 1.03/0.71 fof(f1252,plain,(
% 1.03/0.71 constr_CONST_4=name_B|constr_CONST_4=name_A|~sQ52_spl),
% 1.03/0.71 inference(resolution,[status(thm)],[f1178,f368])).
% 1.03/0.71 fof(f1385,definition,(
% 1.03/0.71 sQ67_spl <=> (constr_CONST_4=name_B)),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f1386,plain,(
% 1.03/0.71 constr_CONST_4=name_B|~sQ67_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f1385])).
% 1.03/0.71 fof(f1388,definition,(
% 1.03/0.71 sQ68_spl <=> (constr_CONST_4=name_A)),
% 1.03/0.71 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 1.03/0.71 fof(f1389,plain,(
% 1.03/0.71 constr_CONST_4=name_A|~sQ68_spl),
% 1.03/0.71 inference(component_clause,[status(thm)],[f1388])).
% 1.03/0.71 fof(f1391,plain,(
% 1.03/0.71 sQ67_spl|sQ68_spl|~sQ52_spl),
% 1.03/0.71 inference(split_clause,[status(thm)],[f1252,f1385,f1388,f1177])).
% 1.03/0.71 fof(f1580,plain,(
% 1.03/0.71 $false|~sQ67_spl),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1386,f214])).
% 1.03/0.71 fof(f1581,plain,(
% 1.03/0.71 ~sQ67_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f1580])).
% 1.03/0.71 fof(f1596,plain,(
% 1.03/0.71 $false|~sQ68_spl),
% 1.03/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1389,f213])).
% 1.03/0.71 fof(f1597,plain,(
% 1.03/0.71 ~sQ68_spl),
% 1.03/0.71 inference(contradiction_clause,[status(thm)],[f1596])).
% 1.03/0.71 fof(f1598,plain,(
% 2.23/0.72 $false),
% 2.23/0.72 inference(sat_refutation,[status(thm)],[f431,f476,f480,f492,f508,f588,f592,f595,f764,f799,f919,f1022,f1199,f1391,f1581,f1597])).
% 2.23/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 1.39/0.75 % Elapsed time: 0.370801 seconds
% 1.39/0.75 % CPU time: 2.565735 seconds
% 1.39/0.75 % Total memory used: 155.121 MB
% 1.39/0.75 % Net memory used: 149.482 MB
%------------------------------------------------------------------------------