%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW966+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 : n018.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 136.98s 18.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW966+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n018.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 10:22:43 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.53 % Drodi V4.1.1
% 136.98/18.03 % Refutation found
% 136.98/18.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 136.98/18.03 % SZS output start CNFRefutation for theBenchmark
% 136.98/18.03 fof(f65,axiom,(
% 136.98/18.03 name_A != name_I ),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.03 fof(f71,axiom,(
% 136.98/18.03 name_B != name_I ),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.03 fof(f92,axiom,(
% 136.98/18.03 (! [VAR_K_24,VAR_M_23] : constr_adec(constr_aenc(VAR_M_23,constr_pkey(VAR_K_24)),VAR_K_24) = VAR_M_23 )),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.03 fof(f94,axiom,(
% 136.98/18.03 (! [VAR_K_20X30,VAR_M_19] : constr_getmess(constr_sign(VAR_M_19,VAR_K_20X30)) = VAR_M_19 )),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.03 fof(f95,axiom,(
% 136.98/18.03 (! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30 )),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.03 fof(f96,axiom,(
% 136.98/18.03 (! [VAR_X_18] : constr_xor(VAR_X_18,VAR_X_18) = constr_ZERO )),
% 136.98/18.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f97,axiom,(
% 136.98/18.04 (! [VAR_X_17] : constr_xor(VAR_X_17,constr_ZERO) = VAR_X_17 )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f98,axiom,(
% 136.98/18.04 (! [VAR_X_15,VAR_Y_16] : constr_xor(VAR_X_15,VAR_Y_16) = constr_xor(VAR_Y_16,VAR_X_15) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f99,axiom,(
% 136.98/18.04 (! [VAR_X_13,VAR_Y_14,VAR_Z_0X30] : constr_xor(VAR_X_13,constr_xor(VAR_Y_14,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_13,VAR_Y_14),VAR_Z_0X30) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f100,axiom,(
% 136.98/18.04 (! [VAR_X0X30_11,VAR_X1_12] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12 )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f101,axiom,(
% 136.98/18.04 (! [VAR_X0X30_9,VAR_X1_10X30] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_9,VAR_X1_10X30)) = VAR_X0X30_9 )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f104,axiom,(
% 136.98/18.04 (! [VAR_X_42,VAR_Y_43] : pred_eq_bitstring_bitstring(VAR_X_42,VAR_Y_43) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f112,axiom,(
% 136.98/18.04 (! [VAR_V_65] :( pred_attacker(VAR_V_65)=> pred_attacker(constr_pkey(VAR_V_65)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f114,axiom,(
% 136.98/18.04 (! [VAR_V_70X30] :( pred_attacker(tuple_out_3(VAR_V_70X30))=> pred_attacker(VAR_V_70X30) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f116,axiom,(
% 136.98/18.04 (! [VAR_V_76] :( pred_attacker(tuple_out_2(VAR_V_76))=> pred_attacker(VAR_V_76) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f118,axiom,(
% 136.98/18.04 (! [VAR_V_82] :( pred_attacker(tuple_out_1(VAR_V_82))=> pred_attacker(VAR_V_82) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f120,axiom,(
% 136.98/18.04 (! [VAR_V_89] :( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_89))=> pred_attacker(VAR_V_89) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f121,axiom,(
% 136.98/18.04 (! [VAR_V_93,VAR_V_94] :( ( pred_attacker(VAR_V_93)& pred_attacker(VAR_V_94) )=> pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_93,VAR_V_94)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f124,axiom,(
% 136.98/18.04 (! [VAR_V_10X309,VAR_V_110X30] :( ( pred_attacker(VAR_V_10X309)& pred_attacker(VAR_V_110X30) )=> pred_attacker(tuple_key_register_server_in_1(VAR_V_10X309,VAR_V_110X30)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f127,axiom,(
% 136.98/18.04 (! [VAR_V_124] :( pred_attacker(VAR_V_124)=> pred_attacker(constr_getmess(VAR_V_124)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f132,axiom,(
% 136.98/18.04 (! [VAR_V_137] :( pred_attacker(tuple_client_B_out_6(VAR_V_137))=> pred_attacker(VAR_V_137) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f134,axiom,(
% 136.98/18.04 (! [VAR_V_143] :( pred_attacker(tuple_client_B_out_4(VAR_V_143))=> pred_attacker(VAR_V_143) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f138,axiom,(
% 136.98/18.04 (! [VAR_V_162] :( pred_attacker(VAR_V_162)=> pred_attacker(tuple_client_B_in_5(VAR_V_162)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f140,axiom,(
% 136.98/18.04 (! [VAR_V_168] :( pred_attacker(VAR_V_168)=> pred_attacker(tuple_client_B_in_3(VAR_V_168)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f142,axiom,(
% 136.98/18.04 (! [VAR_V_174] :( pred_attacker(VAR_V_174)=> pred_attacker(tuple_client_B_in_2(VAR_V_174)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f156,axiom,(
% 136.98/18.04 (! [VAR_V_225,VAR_V_226] :( ( pred_attacker(VAR_V_225)& pred_attacker(VAR_V_226) )=> pred_attacker(constr_aenc(VAR_V_225,VAR_V_226)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f157,axiom,(
% 136.98/18.04 (! [VAR_V_229,VAR_V_230X30] :( ( pred_attacker(VAR_V_229)& pred_attacker(VAR_V_230X30) )=> pred_attacker(constr_adec(VAR_V_229,VAR_V_230X30)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f164,axiom,(
% 136.98/18.04 (! [VAR_V_237,VAR_V_238] :( ( pred_attacker(VAR_V_237)& pred_attacker(VAR_V_238) )=> pred_attacker(tuple_2(VAR_V_237,VAR_V_238)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f166,axiom,(
% 136.98/18.04 (! [VAR_V_248,VAR_V_249] :( pred_attacker(tuple_2(VAR_V_248,VAR_V_249))=> pred_attacker(VAR_V_249) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f170,axiom,(
% 136.98/18.04 pred_attacker(name_I) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f171,axiom,(
% 136.98/18.04 pred_attacker(name_B) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f174,axiom,(
% 136.98/18.04 (! [VAR_V_257] : pred_attacker(name_new0x2Dname(VAR_V_257)) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f176,axiom,(
% 136.98/18.04 pred_table(tuple_keys(name_B,constr_pkey(name_skB))) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f177,axiom,(
% 136.98/18.04 pred_attacker(tuple_out_1(constr_pkey(name_skA))) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f178,axiom,(
% 136.98/18.04 pred_attacker(tuple_out_2(constr_pkey(name_skB))) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f179,axiom,(
% 136.98/18.04 pred_attacker(tuple_out_3(constr_pkey(name_skS))) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f180,axiom,(
% 136.98/18.04 pred_attacker(tuple_client_A_out_1(name_A,name_I)) ),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f184,axiom,(
% 136.98/18.04 (! [VAR_0X40SID_554,VAR_AENC_NA_A_552,VAR_SIGN_A_PKA_553] :( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_552,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_552))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_553)) )=> pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_552,name_skB)),name_B),name_Nb(VAR_0X40SID_554)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS)))))) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f185,axiom,(
% 136.98/18.04 (! [VAR_0X40SID_578,VAR_AENC_NA_A_580X30,VAR_AENC_NB_579,VAR_SIGN_A_PKA_581] :( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_578),constr_adec(VAR_AENC_NB_579,name_skB))& pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_579))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_580X30,name_skB)))& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_580X30))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_581,constr_pkey(name_skS))))& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_581)) )=> pred_attacker(tuple_client_B_out_6(name_objective)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f186,axiom,(
% 136.98/18.04 (! [VAR_DST_620X30,VAR_PKDST_621,VAR_SRC_622] :( ( pred_table(tuple_keys(VAR_DST_620X30,VAR_PKDST_621))& pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_622,VAR_DST_620X30)) )=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_620X30,VAR_PKDST_621),name_skS))) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f187,axiom,(
% 136.98/18.04 (! [VAR_HOST_674,VAR_PK_675] :( ( VAR_HOST_674 != name_B& VAR_HOST_674 != name_A& pred_attacker(tuple_key_register_server_in_1(VAR_HOST_674,VAR_PK_675)) )=> pred_table(tuple_keys(VAR_HOST_674,VAR_PK_675)) ) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f188,conjecture,(
% 136.98/18.04 (! [VAR_V_683] : pred_attacker(tuple_2(name_Nb(VAR_V_683),name_objective)) )),
% 136.98/18.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 136.98/18.04 fof(f189,negated_conjecture,(
% 136.98/18.04 ~((! [VAR_V_683] : pred_attacker(tuple_2(name_Nb(VAR_V_683),name_objective)) ))),
% 136.98/18.04 inference(negated_conjecture,[status(cth)],[f188])).
% 136.98/18.04 fof(f254,plain,(
% 136.98/18.04 ~name_A=name_I),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f65])).
% 136.98/18.04 fof(f260,plain,(
% 136.98/18.04 ~name_B=name_I),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f71])).
% 136.98/18.04 fof(f281,plain,(
% 136.98/18.04 ![X0,X1]: (constr_adec(constr_aenc(X0,constr_pkey(X1)),X1)=X0)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f92])).
% 136.98/18.04 fof(f283,plain,(
% 136.98/18.04 ![X0,X1]: (constr_getmess(constr_sign(X0,X1))=X0)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f94])).
% 136.98/18.04 fof(f284,plain,(
% 136.98/18.04 ![X0,X1]: (constr_checksign(constr_sign(X0,X1),constr_pkey(X1))=X0)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f95])).
% 136.98/18.04 fof(f285,plain,(
% 136.98/18.04 ![X0]: (constr_xor(X0,X0)=constr_ZERO)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f96])).
% 136.98/18.04 fof(f286,plain,(
% 136.98/18.04 ![X0]: (constr_xor(X0,constr_ZERO)=X0)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f97])).
% 136.98/18.04 fof(f287,plain,(
% 136.98/18.04 ![X0,X1]: (constr_xor(X0,X1)=constr_xor(X1,X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f98])).
% 136.98/18.04 fof(f288,plain,(
% 136.98/18.04 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(constr_xor(X0,X1),X2))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f99])).
% 136.98/18.04 fof(f289,plain,(
% 136.98/18.04 ![X0,X1]: (constr_tuple_2_get_1_bitstring(tuple_2(X0,X1))=X1)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f100])).
% 136.98/18.04 fof(f290,plain,(
% 136.98/18.04 ![X0,X1]: (constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1))=X0)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f101])).
% 136.98/18.04 fof(f293,plain,(
% 136.98/18.04 ![X0,X1]: (pred_eq_bitstring_bitstring(X0,X1))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f104])).
% 136.98/18.04 fof(f307,plain,(
% 136.98/18.04 ![VAR_V_65]: (~pred_attacker(VAR_V_65)|pred_attacker(constr_pkey(VAR_V_65)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f112])).
% 136.98/18.04 fof(f308,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_pkey(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f307])).
% 136.98/18.04 fof(f311,plain,(
% 136.98/18.04 ![VAR_V_70X30]: (~pred_attacker(tuple_out_3(VAR_V_70X30))|pred_attacker(VAR_V_70X30))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 136.98/18.04 fof(f312,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_out_3(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f311])).
% 136.98/18.04 fof(f315,plain,(
% 136.98/18.04 ![VAR_V_76]: (~pred_attacker(tuple_out_2(VAR_V_76))|pred_attacker(VAR_V_76))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 136.98/18.04 fof(f316,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_out_2(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f315])).
% 136.98/18.04 fof(f319,plain,(
% 136.98/18.04 ![VAR_V_82]: (~pred_attacker(tuple_out_1(VAR_V_82))|pred_attacker(VAR_V_82))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 136.98/18.04 fof(f320,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_out_1(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f319])).
% 136.98/18.04 fof(f323,plain,(
% 136.98/18.04 ![VAR_V_89]: (~pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_89))|pred_attacker(VAR_V_89))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 136.98/18.04 fof(f324,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_key_retrieval_server_out_2(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f323])).
% 136.98/18.04 fof(f325,plain,(
% 136.98/18.04 ![VAR_V_93,VAR_V_94]: ((~pred_attacker(VAR_V_93)|~pred_attacker(VAR_V_94))|pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_93,VAR_V_94)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 136.98/18.04 fof(f326,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f325])).
% 136.98/18.04 fof(f333,plain,(
% 136.98/18.04 ![VAR_V_10X309,VAR_V_110X30]: ((~pred_attacker(VAR_V_10X309)|~pred_attacker(VAR_V_110X30))|pred_attacker(tuple_key_register_server_in_1(VAR_V_10X309,VAR_V_110X30)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 136.98/18.04 fof(f334,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_key_register_server_in_1(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f333])).
% 136.98/18.04 fof(f341,plain,(
% 136.98/18.04 ![VAR_V_124]: (~pred_attacker(VAR_V_124)|pred_attacker(constr_getmess(VAR_V_124)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f127])).
% 136.98/18.04 fof(f342,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_getmess(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f341])).
% 136.98/18.04 fof(f350,plain,(
% 136.98/18.04 ![VAR_V_137]: (~pred_attacker(tuple_client_B_out_6(VAR_V_137))|pred_attacker(VAR_V_137))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f132])).
% 136.98/18.04 fof(f351,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_client_B_out_6(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f350])).
% 136.98/18.04 fof(f354,plain,(
% 136.98/18.04 ![VAR_V_143]: (~pred_attacker(tuple_client_B_out_4(VAR_V_143))|pred_attacker(VAR_V_143))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f134])).
% 136.98/18.04 fof(f355,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_client_B_out_4(X0))|pred_attacker(X0))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f354])).
% 136.98/18.04 fof(f364,plain,(
% 136.98/18.04 ![VAR_V_162]: (~pred_attacker(VAR_V_162)|pred_attacker(tuple_client_B_in_5(VAR_V_162)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f138])).
% 136.98/18.04 fof(f365,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_5(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f364])).
% 136.98/18.04 fof(f368,plain,(
% 136.98/18.04 ![VAR_V_168]: (~pred_attacker(VAR_V_168)|pred_attacker(tuple_client_B_in_3(VAR_V_168)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 136.98/18.04 fof(f369,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_3(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f368])).
% 136.98/18.04 fof(f372,plain,(
% 136.98/18.04 ![VAR_V_174]: (~pred_attacker(VAR_V_174)|pred_attacker(tuple_client_B_in_2(VAR_V_174)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 136.98/18.04 fof(f373,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_in_2(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f372])).
% 136.98/18.04 fof(f402,plain,(
% 136.98/18.04 ![VAR_V_225,VAR_V_226]: ((~pred_attacker(VAR_V_225)|~pred_attacker(VAR_V_226))|pred_attacker(constr_aenc(VAR_V_225,VAR_V_226)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f156])).
% 136.98/18.04 fof(f403,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_aenc(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f402])).
% 136.98/18.04 fof(f404,plain,(
% 136.98/18.04 ![VAR_V_229,VAR_V_230X30]: ((~pred_attacker(VAR_V_229)|~pred_attacker(VAR_V_230X30))|pred_attacker(constr_adec(VAR_V_229,VAR_V_230X30)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f157])).
% 136.98/18.04 fof(f405,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_adec(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f404])).
% 136.98/18.04 fof(f412,plain,(
% 136.98/18.04 ![VAR_V_237,VAR_V_238]: ((~pred_attacker(VAR_V_237)|~pred_attacker(VAR_V_238))|pred_attacker(tuple_2(VAR_V_237,VAR_V_238)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f164])).
% 136.98/18.04 fof(f413,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_2(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f412])).
% 136.98/18.04 fof(f417,plain,(
% 136.98/18.04 ![VAR_V_248,VAR_V_249]: (~pred_attacker(tuple_2(VAR_V_248,VAR_V_249))|pred_attacker(VAR_V_249))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f166])).
% 136.98/18.04 fof(f418,plain,(
% 136.98/18.04 ![VAR_V_249]: ((![VAR_V_248]: ~pred_attacker(tuple_2(VAR_V_248,VAR_V_249)))|pred_attacker(VAR_V_249))),
% 136.98/18.04 inference(miniscoping,[status(thm)],[f417])).
% 136.98/18.04 fof(f419,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(tuple_2(X0,X1))|pred_attacker(X1))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f418])).
% 136.98/18.04 fof(f426,plain,(
% 136.98/18.04 pred_attacker(name_I)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f170])).
% 136.98/18.04 fof(f427,plain,(
% 136.98/18.04 pred_attacker(name_B)),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f171])).
% 136.98/18.04 fof(f430,plain,(
% 136.98/18.04 ![X0]: (pred_attacker(name_new0x2Dname(X0)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f174])).
% 136.98/18.04 fof(f432,plain,(
% 136.98/18.04 pred_table(tuple_keys(name_B,constr_pkey(name_skB)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f176])).
% 136.98/18.04 fof(f433,plain,(
% 136.98/18.04 pred_attacker(tuple_out_1(constr_pkey(name_skA)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f177])).
% 136.98/18.04 fof(f434,plain,(
% 136.98/18.04 pred_attacker(tuple_out_2(constr_pkey(name_skB)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f178])).
% 136.98/18.04 fof(f435,plain,(
% 136.98/18.04 pred_attacker(tuple_out_3(constr_pkey(name_skS)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f179])).
% 136.98/18.04 fof(f436,plain,(
% 136.98/18.04 pred_attacker(tuple_client_A_out_1(name_A,name_I))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f180])).
% 136.98/18.04 fof(f444,plain,(
% 136.98/18.04 ![VAR_0X40SID_554,VAR_AENC_NA_A_552,VAR_SIGN_A_PKA_553]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_552,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_552)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_553)))|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_552,name_skB)),name_B),name_Nb(VAR_0X40SID_554)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS)))))))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f184])).
% 136.98/18.04 fof(f445,plain,(
% 136.98/18.04 ![VAR_AENC_NA_A_552,VAR_SIGN_A_PKA_553]: ((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_552,name_skB)))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_552)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_553)))|(![VAR_0X40SID_554]: pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_552,name_skB)),name_B),name_Nb(VAR_0X40SID_554)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_553,constr_pkey(name_skS))))))))),
% 136.98/18.04 inference(miniscoping,[status(thm)],[f444])).
% 136.98/18.04 fof(f446,plain,(
% 136.98/18.04 ![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_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f445])).
% 136.98/18.04 fof(f447,plain,(
% 136.98/18.04 ![VAR_0X40SID_578,VAR_AENC_NA_A_580X30,VAR_AENC_NB_579,VAR_SIGN_A_PKA_581]: ((((((~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_578),constr_adec(VAR_AENC_NB_579,name_skB))|~pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_579)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_580X30,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_580X30)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_581,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_581)))|pred_attacker(tuple_client_B_out_6(name_objective)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f185])).
% 136.98/18.04 fof(f448,plain,(
% 136.98/18.04 (![VAR_SIGN_A_PKA_581]: (((![VAR_AENC_NA_A_580X30]: (((![VAR_AENC_NB_579]: ((![VAR_0X40SID_578]: ~pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_578),constr_adec(VAR_AENC_NB_579,name_skB)))|~pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_579))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_580X30,name_skB))))|~pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_580X30))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_581,constr_pkey(name_skS)))))|~pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_581))))|pred_attacker(tuple_client_B_out_6(name_objective))),
% 136.98/18.04 inference(miniscoping,[status(thm)],[f447])).
% 136.98/18.04 fof(f449,plain,(
% 136.98/18.04 ![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)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f448])).
% 136.98/18.04 fof(f450,plain,(
% 136.98/18.04 ![VAR_DST_620X30,VAR_PKDST_621,VAR_SRC_622]: ((~pred_table(tuple_keys(VAR_DST_620X30,VAR_PKDST_621))|~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_622,VAR_DST_620X30)))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_620X30,VAR_PKDST_621),name_skS))))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f186])).
% 136.98/18.04 fof(f451,plain,(
% 136.98/18.04 ![VAR_DST_620X30,VAR_PKDST_621]: ((~pred_table(tuple_keys(VAR_DST_620X30,VAR_PKDST_621))|(![VAR_SRC_622]: ~pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_622,VAR_DST_620X30))))|pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_620X30,VAR_PKDST_621),name_skS))))),
% 136.98/18.04 inference(miniscoping,[status(thm)],[f450])).
% 136.98/18.04 fof(f452,plain,(
% 136.98/18.04 ![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))))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f451])).
% 136.98/18.04 fof(f453,plain,(
% 136.98/18.04 ![VAR_HOST_674,VAR_PK_675]: (((VAR_HOST_674=name_B|VAR_HOST_674=name_A)|~pred_attacker(tuple_key_register_server_in_1(VAR_HOST_674,VAR_PK_675)))|pred_table(tuple_keys(VAR_HOST_674,VAR_PK_675)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f187])).
% 136.98/18.04 fof(f454,plain,(
% 136.98/18.04 ![X0,X1]: (X0=name_B|X0=name_A|~pred_attacker(tuple_key_register_server_in_1(X0,X1))|pred_table(tuple_keys(X0,X1)))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f453])).
% 136.98/18.04 fof(f455,plain,(
% 136.98/18.04 (?[VAR_V_683]: ~pred_attacker(tuple_2(name_Nb(VAR_V_683),name_objective)))),
% 136.98/18.04 inference(pre_NNF_transformation,[status(thm)],[f189])).
% 136.98/18.04 fof(f456,plain,(
% 136.98/18.04 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 136.98/18.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VAR_V_683,sK0_skl)],[f455])).
% 136.98/18.04 fof(f457,plain,(
% 136.98/18.04 ~pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective))),
% 136.98/18.04 inference(cnf_transformation,[status(thm)],[f456])).
% 136.98/18.04 fof(f458,definition,(
% 136.98/18.04 ![X0,X1]: (sQ0_spl <=> (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f459,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB))|~pred_attacker(tuple_client_B_in_5(X1))|~sQ0_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f458])).
% 136.98/18.04 fof(f461,definition,(
% 136.98/18.04 ![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))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f462,plain,(
% 136.98/18.04 ![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)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f461])).
% 136.98/18.04 fof(f464,definition,(
% 136.98/18.04 ![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))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f465,plain,(
% 136.98/18.04 ![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)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f464])).
% 136.98/18.04 fof(f467,definition,(
% 136.98/18.04 sQ3_spl <=> (pred_attacker(tuple_client_B_out_6(name_objective)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f468,plain,(
% 136.98/18.04 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ3_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f467])).
% 136.98/18.04 fof(f470,plain,(
% 136.98/18.04 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f449,f458,f461,f464,f467])).
% 136.98/18.04 fof(f471,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,tuple_client_B_out_6(name_objective)))|~sQ3_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f413,f468])).
% 136.98/18.04 fof(f472,plain,(
% 136.98/18.04 pred_attacker(tuple_2(tuple_client_B_out_6(name_objective),tuple_client_B_out_6(name_objective)))|~sQ3_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f471,f468])).
% 136.98/18.04 fof(f475,plain,(
% 136.98/18.04 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),
% 136.98/18.04 inference(resolution,[status(thm)],[f472,f471])).
% 136.98/18.04 fof(f480,plain,(
% 136.98/18.04 ![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)),
% 136.98/18.04 inference(resolution,[status(thm)],[f475,f413])).
% 136.98/18.04 fof(f494,plain,(
% 136.98/18.04 ![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)),
% 136.98/18.04 inference(resolution,[status(thm)],[f480,f419])).
% 136.98/18.04 fof(f499,definition,(
% 136.98/18.04 ![X0]: (sQ4_spl <=> (~pred_attacker(X0)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f500,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~sQ4_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f499])).
% 136.98/18.04 fof(f502,definition,(
% 136.98/18.04 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))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f503,plain,(
% 136.98/18.04 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),
% 136.98/18.04 inference(component_clause,[status(thm)],[f502])).
% 136.98/18.04 fof(f505,plain,(
% 136.98/18.04 sQ4_spl|sQ5_spl|~sQ3_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f494,f499,f502,f467])).
% 136.98/18.04 fof(f508,plain,(
% 136.98/18.04 ~pred_attacker(name_Nb(sK0_skl))|~pred_attacker(name_objective)),
% 136.98/18.04 inference(resolution,[status(thm)],[f457,f413])).
% 136.98/18.04 fof(f509,definition,(
% 136.98/18.04 sQ6_spl <=> (pred_attacker(name_Nb(sK0_skl)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f511,plain,(
% 136.98/18.04 ~pred_attacker(name_Nb(sK0_skl))|sQ6_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f509])).
% 136.98/18.04 fof(f512,definition,(
% 136.98/18.04 sQ7_spl <=> (pred_attacker(name_objective))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f514,plain,(
% 136.98/18.04 ~pred_attacker(name_objective)|sQ7_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f512])).
% 136.98/18.04 fof(f515,plain,(
% 136.98/18.04 ~sQ6_spl|~sQ7_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f508,f509,f512])).
% 136.98/18.04 fof(f524,plain,(
% 136.98/18.04 pred_attacker(tuple_client_B_out_6(name_objective))|~sQ5_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f503,f419])).
% 136.98/18.04 fof(f527,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_client_B_in_2(X0))|~sQ2_spl)),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f465,f293])).
% 136.98/18.04 fof(f530,plain,(
% 136.98/18.04 ![X0]: (X0=constr_xor(constr_ZERO,X0))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f286,f287])).
% 136.98/18.04 fof(f539,plain,(
% 136.98/18.04 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(X2,constr_xor(X0,X1)))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f287,f288])).
% 136.98/18.04 fof(f546,plain,(
% 136.98/18.04 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=constr_xor(constr_ZERO,X1))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f285,f288])).
% 136.98/18.04 fof(f617,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(constr_sign(X0,X1))|pred_attacker(X0))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f283,f342])).
% 136.98/18.04 fof(f618,plain,(
% 136.98/18.04 pred_attacker(name_objective)|~sQ5_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f351,f524])).
% 136.98/18.04 fof(f620,plain,(
% 136.98/18.04 $false|sQ7_spl|~sQ5_spl),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f618,f514])).
% 136.98/18.04 fof(f621,plain,(
% 136.98/18.04 sQ7_spl|~sQ5_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f620])).
% 136.98/18.04 fof(f629,plain,(
% 136.98/18.04 $false|~sQ4_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f430,f500])).
% 136.98/18.04 fof(f642,plain,(
% 136.98/18.04 ~sQ4_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f629])).
% 136.98/18.04 fof(f643,plain,(
% 136.98/18.04 ![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_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f446,f293])).
% 136.98/18.04 fof(f644,plain,(
% 136.98/18.04 ![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_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f643,f293])).
% 136.98/18.04 fof(f673,plain,(
% 136.98/18.04 $false|~sQ2_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f430,f686])).
% 136.98/18.04 fof(f686,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~sQ2_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f373,f527])).
% 136.98/18.04 fof(f687,plain,(
% 136.98/18.04 ~sQ2_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f673])).
% 136.98/18.04 fof(f688,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_client_B_in_5(X0))|~sQ0_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f459,f293])).
% 136.98/18.04 fof(f690,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,name_B)))),
% 136.98/18.04 inference(resolution,[status(thm)],[f427,f413])).
% 136.98/18.04 fof(f706,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(name_B))),
% 136.98/18.04 inference(resolution,[status(thm)],[f690,f419])).
% 136.98/18.04 fof(f709,definition,(
% 136.98/18.04 sQ13_spl <=> (pred_attacker(name_B))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f712,plain,(
% 136.98/18.04 sQ4_spl|sQ13_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f706,f499,f709])).
% 136.98/18.04 fof(f890,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(constr_aenc(X0,constr_pkey(X1)))|~pred_attacker(X1)|pred_attacker(X0))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f281,f405])).
% 136.98/18.04 fof(f1103,plain,(
% 136.98/18.04 pred_attacker(constr_pkey(name_skA))),
% 136.98/18.04 inference(resolution,[status(thm)],[f320,f433])).
% 136.98/18.04 fof(f1106,plain,(
% 136.98/18.04 pred_attacker(constr_pkey(name_skB))),
% 136.98/18.04 inference(resolution,[status(thm)],[f316,f434])).
% 136.98/18.04 fof(f1108,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_2(X0,constr_pkey(name_skB))))),
% 136.98/18.04 inference(resolution,[status(thm)],[f1106,f413])).
% 136.98/18.04 fof(f1109,plain,(
% 136.98/18.04 pred_attacker(constr_pkey(name_skS))),
% 136.98/18.04 inference(resolution,[status(thm)],[f312,f435])).
% 136.98/18.04 fof(f1125,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_pkey(name_skB)))),
% 136.98/18.04 inference(resolution,[status(thm)],[f1108,f419])).
% 136.98/18.04 fof(f1128,definition,(
% 136.98/18.04 sQ59_spl <=> (pred_attacker(constr_pkey(name_skB)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f1131,plain,(
% 136.98/18.04 sQ4_spl|sQ59_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f1125,f499,f1128])).
% 136.98/18.04 fof(f1200,plain,(
% 136.98/18.04 $false|~sQ0_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f1109,f1221])).
% 136.98/18.04 fof(f1221,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~sQ0_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f365,f688])).
% 136.98/18.04 fof(f1222,plain,(
% 136.98/18.04 ~sQ0_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f1200])).
% 136.98/18.04 fof(f1223,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_client_B_in_3(X0))|~sQ1_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f462,f293])).
% 136.98/18.04 fof(f1253,plain,(
% 136.98/18.04 ![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))))),
% 136.98/18.04 inference(resolution,[status(thm)],[f326,f452])).
% 136.98/18.04 fof(f1254,definition,(
% 136.98/18.04 ![X1,X2]: (sQ69_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)))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f1255,plain,(
% 136.98/18.04 ![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)))|~sQ69_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f1254])).
% 136.98/18.04 fof(f1257,plain,(
% 136.98/18.04 sQ4_spl|sQ69_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f1253,f499,f1254])).
% 136.98/18.04 fof(f1300,plain,(
% 136.98/18.04 $false|~sQ1_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f1103,f1316])).
% 136.98/18.04 fof(f1316,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~sQ1_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f369,f1223])).
% 136.98/18.04 fof(f1317,plain,(
% 136.98/18.04 ~sQ1_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f1300])).
% 136.98/18.04 fof(f1585,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(tuple_client_B_in_3(X1))|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))),
% 136.98/18.04 inference(resolution,[status(thm)],[f373,f644])).
% 136.98/18.04 fof(f1622,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))|~pred_attacker(X1))),
% 136.98/18.04 inference(resolution,[status(thm)],[f1585,f369])).
% 136.98/18.04 fof(f1706,plain,(
% 136.98/18.04 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=X1)),
% 136.98/18.04 inference(forward_demodulation,[status(thm)],[f530,f546])).
% 136.98/18.04 fof(f1755,plain,(
% 136.98/18.04 ![X0,X1]: (X0=name_B|X0=name_A|pred_table(tuple_keys(X0,X1))|~pred_attacker(X0)|~pred_attacker(X1))),
% 136.98/18.04 inference(resolution,[status(thm)],[f454,f334])).
% 136.98/18.04 fof(f1764,plain,(
% 136.98/18.04 ![X0,X1,X2]: (constr_xor(constr_xor(X0,X1),X2)=constr_xor(X1,constr_xor(X2,X0)))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f287,f539])).
% 136.98/18.04 fof(f2045,definition,(
% 136.98/18.04 ![X0]: (sQ93_spl <=> (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f2046,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_pkey(X0))|~sQ93_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f2045])).
% 136.98/18.04 fof(f2259,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(X1),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))|~pred_attacker(constr_aenc(X1,constr_pkey(name_skB))))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f281,f1622])).
% 136.98/18.04 fof(f2608,plain,(
% 136.98/18.04 ![X0,X1,X2]: (constr_xor(constr_xor(X0,X1),X2)=constr_xor(X0,constr_xor(X2,X1)))),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f287,f1764])).
% 136.98/18.04 fof(f3156,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|~pred_table(tuple_keys(X0,X1))|pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|~sQ69_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f1255,f324])).
% 136.98/18.04 fof(f3850,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(X1),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))|~pred_attacker(X1)|~pred_attacker(constr_pkey(name_skB)))),
% 136.98/18.04 inference(resolution,[status(thm)],[f2259,f403])).
% 136.98/18.04 fof(f3858,definition,(
% 136.98/18.04 ![X0,X1,X2]: (sQ129_spl <=> (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(X1),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))|~pred_attacker(X1)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f3859,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(X1),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))|~pred_attacker(X1)|~sQ129_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f3858])).
% 136.98/18.04 fof(f3861,plain,(
% 136.98/18.04 sQ129_spl|~sQ59_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f3850,f3858,f1128])).
% 136.98/18.04 fof(f3870,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|~sQ93_spl)),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f2046,f308])).
% 136.98/18.04 fof(f3871,plain,(
% 136.98/18.04 $false|~sQ93_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f436,f3870])).
% 136.98/18.04 fof(f3903,plain,(
% 136.98/18.04 ~sQ93_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f3871])).
% 136.98/18.04 fof(f7721,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(X1),name_B),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))|~sQ129_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f3859,f355])).
% 136.98/18.04 fof(f7728,plain,(
% 136.98/18.04 ![X0,X1,X2,X3]: (~pred_attacker(X0)|~pred_attacker(tuple_2(X1,X2))|pred_attacker(constr_aenc(tuple_2(constr_xor(X1,name_B),name_Nb(X3)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))|~sQ129_spl)),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f290,f7721])).
% 136.98/18.04 fof(f9507,plain,(
% 136.98/18.04 ![X0,X1,X2,X3,X4]: (~pred_attacker(X0)|~pred_attacker(tuple_2(constr_xor(X1,X2),X3))|pred_attacker(constr_aenc(tuple_2(constr_xor(X1,constr_xor(X2,name_B)),name_Nb(X4)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))|~sQ129_spl)),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f288,f7728])).
% 136.98/18.04 fof(f9519,definition,(
% 136.98/18.04 ![X0,X2]: (sQ136_spl <=> (~pred_attacker(X0)|pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f9520,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(X0)|pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X1)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))|~sQ136_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f9519])).
% 136.98/18.04 fof(f9766,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(constr_sign(X0,name_skS))|pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X1)),constr_tuple_2_get_1_bitstring(X0)))|~sQ136_spl)),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f284,f9520])).
% 136.98/18.04 fof(f14648,plain,(
% 136.98/18.04 ![X0,X1,X2,X3]: (~pred_attacker(X0)|~pred_attacker(tuple_2(constr_xor(constr_xor(X1,name_B),X1),X2))|pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X3)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))|~sQ129_spl)),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f285,f9507])).
% 136.98/18.04 fof(f14673,definition,(
% 136.98/18.04 ![X1,X2]: (sQ176_spl <=> (~pred_attacker(tuple_2(constr_xor(constr_xor(X1,name_B),X1),X2))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f14674,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(tuple_2(constr_xor(constr_xor(X0,name_B),X0),X1))|~sQ176_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f14673])).
% 136.98/18.04 fof(f14676,plain,(
% 136.98/18.04 sQ136_spl|sQ176_spl|~sQ129_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f14648,f9519,f14673,f3858])).
% 136.98/18.04 fof(f17836,plain,(
% 136.98/18.04 ~pred_attacker(name_B)|pred_attacker(constr_sign(tuple_2(name_B,constr_pkey(name_skB)),name_skS))|~sQ69_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f3156,f432])).
% 136.98/18.04 fof(f17839,definition,(
% 136.98/18.04 sQ191_spl <=> (pred_attacker(constr_sign(tuple_2(name_B,constr_pkey(name_skB)),name_skS)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f17840,plain,(
% 136.98/18.04 pred_attacker(constr_sign(tuple_2(name_B,constr_pkey(name_skB)),name_skS))|~sQ191_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f17839])).
% 136.98/18.04 fof(f17842,plain,(
% 136.98/18.04 ~sQ13_spl|sQ191_spl|~sQ69_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f17836,f709,f17839,f1254])).
% 136.98/18.04 fof(f18316,plain,(
% 136.98/18.04 pred_attacker(tuple_2(name_B,constr_pkey(name_skB)))|~sQ191_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f17840,f617])).
% 136.98/18.04 fof(f18437,definition,(
% 136.98/18.04 ![X0]: (sQ197_spl <=> (pred_attacker(tuple_2(constr_ZERO,name_Nb(X0)))))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f18438,plain,(
% 136.98/18.04 ![X0]: (pred_attacker(tuple_2(constr_ZERO,name_Nb(X0)))|~sQ197_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f18437])).
% 136.98/18.04 fof(f18839,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(tuple_2(constr_xor(X0,constr_xor(X0,name_B)),X1))|~sQ176_spl)),
% 136.98/18.04 inference(forward_demodulation,[status(thm)],[f2608,f14674])).
% 136.98/18.04 fof(f18840,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(tuple_2(name_B,X0))|~sQ176_spl)),
% 136.98/18.04 inference(forward_demodulation,[status(thm)],[f1706,f18839])).
% 136.98/18.04 fof(f18860,plain,(
% 136.98/18.04 $false|~sQ176_spl|~sQ191_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f18316,f18840])).
% 136.98/18.04 fof(f18971,plain,(
% 136.98/18.04 ~sQ176_spl|~sQ191_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f18860])).
% 136.98/18.04 fof(f19763,plain,(
% 136.98/18.04 ![X0]: (pred_attacker(name_Nb(X0))|~sQ197_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f18438,f419])).
% 136.98/18.04 fof(f19764,plain,(
% 136.98/18.04 $false|~sQ197_spl|sQ6_spl),
% 136.98/18.04 inference(backward_subsumption_resolution,[status(thm)],[f511,f19763])).
% 136.98/18.04 fof(f19765,plain,(
% 136.98/18.04 ~sQ197_spl|sQ6_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f19764])).
% 136.98/18.04 fof(f22915,plain,(
% 136.98/18.04 ![X0,X1,X2]: (~pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))|pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X2)),X1))|~sQ136_spl)),
% 136.98/18.04 inference(paramodulation,[status(thm)],[f289,f9766])).
% 136.98/18.04 fof(f22937,definition,(
% 136.98/18.04 ![X0]: (sQ252_spl <=> (~pred_attacker(X0)|X0=name_B|X0=name_A|~pred_attacker(X0)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f22938,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|X0=name_B|X0=name_A|~pred_attacker(X0)|~sQ252_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f22937])).
% 136.98/18.04 fof(f23378,plain,(
% 136.98/18.04 ![X0,X1,X2]: (pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X0)),X1))|~pred_attacker(X2)|~pred_table(tuple_keys(X2,X1))|~sQ136_spl|~sQ69_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f22915,f3156])).
% 136.98/18.04 fof(f23394,plain,(
% 136.98/18.04 ![X0,X1,X2]: (pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X0)),X1))|~pred_attacker(X2)|X2=name_B|X2=name_A|~pred_attacker(X2)|~pred_attacker(X1)|~sQ136_spl|~sQ69_spl)),
% 136.98/18.04 inference(resolution,[status(thm)],[f23378,f1755])).
% 136.98/18.04 fof(f23400,definition,(
% 136.98/18.04 ![X0,X1]: (sQ258_spl <=> (pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X0)),X1))|~pred_attacker(X1)))),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f23401,plain,(
% 136.98/18.04 ![X0,X1]: (pred_attacker(constr_aenc(tuple_2(constr_ZERO,name_Nb(X0)),X1))|~pred_attacker(X1)|~sQ258_spl)),
% 136.98/18.04 inference(component_clause,[status(thm)],[f23400])).
% 136.98/18.04 fof(f23403,plain,(
% 136.98/18.04 sQ258_spl|sQ252_spl|~sQ136_spl|~sQ69_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f23394,f23400,f22937,f9519,f1254])).
% 136.98/18.04 fof(f23404,plain,(
% 136.98/18.04 ![X0]: (~pred_attacker(X0)|X0=name_B|X0=name_A|~sQ252_spl)),
% 136.98/18.04 inference(duplicate_literals_removal,[status(thm)],[f22938])).
% 136.98/18.04 fof(f23608,plain,(
% 136.98/18.04 name_I=name_B|name_I=name_A|~sQ252_spl),
% 136.98/18.04 inference(resolution,[status(thm)],[f23404,f426])).
% 136.98/18.04 fof(f23737,definition,(
% 136.98/18.04 sQ292_spl <=> (name_I=name_B)),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f23738,plain,(
% 136.98/18.04 name_I=name_B|~sQ292_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f23737])).
% 136.98/18.04 fof(f23740,definition,(
% 136.98/18.04 sQ293_spl <=> (name_I=name_A)),
% 136.98/18.04 introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition])).
% 136.98/18.04 fof(f23741,plain,(
% 136.98/18.04 name_I=name_A|~sQ293_spl),
% 136.98/18.04 inference(component_clause,[status(thm)],[f23740])).
% 136.98/18.04 fof(f23743,plain,(
% 136.98/18.04 sQ292_spl|sQ293_spl|~sQ252_spl),
% 136.98/18.04 inference(split_clause,[status(thm)],[f23608,f23737,f23740,f22937])).
% 136.98/18.04 fof(f23823,plain,(
% 136.98/18.04 $false|~sQ292_spl),
% 136.98/18.04 inference(forward_subsumption_resolution,[status(thm)],[f23738,f260])).
% 136.98/18.04 fof(f23824,plain,(
% 136.98/18.04 ~sQ292_spl),
% 136.98/18.04 inference(contradiction_clause,[status(thm)],[f23823])).
% 136.98/18.04 fof(f23835,plain,(
% 136.98/18.04 ![X0,X1]: (~pred_attacker(constr_pkey(X0))|~pred_attacker(X0)|pred_attacker(tuple_2(constr_ZERO,name_Nb(X1)))|~sQ258_spl)),
% 136.98/18.07 inference(resolution,[status(thm)],[f23401,f890])).
% 136.98/18.07 fof(f23840,plain,(
% 136.98/18.07 sQ93_spl|sQ197_spl|~sQ258_spl),
% 136.98/18.07 inference(split_clause,[status(thm)],[f23835,f2045,f18437,f23400])).
% 136.98/18.07 fof(f23841,plain,(
% 136.98/18.07 $false|~sQ293_spl),
% 136.98/18.07 inference(forward_subsumption_resolution,[status(thm)],[f23741,f254])).
% 136.98/18.07 fof(f23842,plain,(
% 136.98/18.07 ~sQ293_spl),
% 136.98/18.07 inference(contradiction_clause,[status(thm)],[f23841])).
% 136.98/18.07 fof(f23843,plain,(
% 136.98/18.07 $false),
% 136.98/18.07 inference(sat_refutation,[status(thm)],[f470,f505,f515,f621,f642,f687,f712,f1131,f1222,f1257,f1317,f3861,f3903,f14676,f17842,f18971,f19765,f23403,f23743,f23824,f23840,f23842])).
% 136.98/18.07 % SZS output end CNFRefutation for theBenchmark.p
% 8.88/18.20 % Elapsed time: 17.687627 seconds
% 8.88/18.20 % CPU time: 139.465281 seconds
% 8.88/18.20 % Total memory used: 1.112 GB
% 8.88/18.20 % Net memory used: 1.032 GB
%------------------------------------------------------------------------------