%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW960+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:08:35 PM UTC 2026
% Result : Theorem 0.93s 0.53s
% Output : CNFRefutation 0.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 47
% Syntax : Number of formulae : 180 ( 32 unt; 17 def)
% Number of atoms : 458 ( 37 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 522 ( 244 ~; 226 |; 16 &)
% ( 17 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 18 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 6 con; 0-2 aty)
% Number of variables : 260 ( 259 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f54,axiom,
name_A != name_objective,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
name_B != name_objective,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [VAR_K_18,VAR_M_17] : constr_adec(constr_aenc(VAR_M_17,constr_pkey(VAR_K_18)),VAR_K_18) = VAR_M_17,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [VAR_X0X30_11,VAR_X1_12] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [VAR_X0X30_9,VAR_X1_10X30] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_9,VAR_X1_10X30)) = VAR_X0X30_9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [VAR_X_36,VAR_Y_37] : pred_eq_bitstring_bitstring(VAR_X_36,VAR_Y_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [VAR_V_55] :
( pred_attacker(VAR_V_55)
=> pred_attacker(constr_pkey(VAR_V_55)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [VAR_V_66] :
( pred_attacker(tuple_out_2(VAR_V_66))
=> pred_attacker(VAR_V_66) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [VAR_V_79] :
( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_79))
=> pred_attacker(VAR_V_79) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [VAR_V_83,VAR_V_84] :
( ( pred_attacker(VAR_V_84)
& pred_attacker(VAR_V_83) )
=> pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_83,VAR_V_84)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [VAR_V_94,VAR_V_95] :
( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_94,VAR_V_95))
=> pred_attacker(VAR_V_95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [VAR_V_99,VAR_V_10X300X30] :
( ( pred_attacker(VAR_V_10X300X30)
& pred_attacker(VAR_V_99) )
=> pred_attacker(tuple_key_register_server_in_1(VAR_V_99,VAR_V_10X300X30)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [VAR_V_127] :
( pred_attacker(tuple_client_B_out_6(VAR_V_127))
=> pred_attacker(VAR_V_127) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [VAR_V_133] :
( pred_attacker(tuple_client_B_out_4(VAR_V_133))
=> pred_attacker(VAR_V_133) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [VAR_V_152] :
( pred_attacker(VAR_V_152)
=> pred_attacker(tuple_client_B_in_5(VAR_V_152)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [VAR_V_158] :
( pred_attacker(VAR_V_158)
=> pred_attacker(tuple_client_B_in_3(VAR_V_158)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [VAR_V_164] :
( pred_attacker(VAR_V_164)
=> pred_attacker(tuple_client_B_in_2(VAR_V_164)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [VAR_V_215,VAR_V_216] :
( ( pred_attacker(VAR_V_216)
& pred_attacker(VAR_V_215) )
=> pred_attacker(constr_aenc(VAR_V_215,VAR_V_216)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [VAR_V_219,VAR_V_220X30] :
( ( pred_attacker(VAR_V_220X30)
& pred_attacker(VAR_V_219) )
=> pred_attacker(constr_adec(VAR_V_219,VAR_V_220X30)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [VAR_V_227,VAR_V_228] :
( ( pred_attacker(VAR_V_228)
& pred_attacker(VAR_V_227) )
=> pred_attacker(tuple_2(VAR_V_227,VAR_V_228)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [VAR_V_238,VAR_V_239] :
( pred_attacker(tuple_2(VAR_V_238,VAR_V_239))
=> pred_attacker(VAR_V_239) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,axiom,
! [VAR_V_247] : pred_attacker(name_new0x2Dname(VAR_V_247)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,axiom,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,axiom,
pred_attacker(tuple_client_B_out_1(name_B,name_A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,axiom,
! [VAR_0X40SID_524,VAR_AENC_NA_A_522,VAR_SIGN_A_PKA_523] :
( ( pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523))
& 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_3(VAR_AENC_NA_A_522))
& 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_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)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,axiom,
! [VAR_0X40SID_546,VAR_AENC_NA_A_548,VAR_AENC_NB_547,VAR_SIGN_A_PKA_549] :
( ( pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549))
& 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_3(VAR_AENC_NA_A_548))
& 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_5(VAR_AENC_NB_547))
& pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,axiom,
! [VAR_DST_588,VAR_PKDST_589,VAR_SRC_590X30] :
( ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588))
& pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589)) )
=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [VAR_HOST_642,VAR_PK_643] :
( ( pred_attacker(tuple_key_register_server_in_1(VAR_HOST_642,VAR_PK_643))
& VAR_HOST_642 != name_A
& VAR_HOST_642 != name_B )
=> pred_table(tuple_keys(VAR_HOST_642,VAR_PK_643)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,conjecture,
! [VAR_V_651] : pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,negated_conjecture,
~ ! [VAR_V_651] : pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)),
inference(negated_conjecture,[status(cth)],[f169]) ).
fof(f224,plain,
name_A != name_objective,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f230,plain,
name_B != name_objective,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f249,plain,
! [X0,X1] : constr_adec(constr_aenc(X0,constr_pkey(X1)),X1) = X0,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f252,plain,
! [X0,X1] : constr_checksign(constr_sign(X0,X1),constr_pkey(X1)) = X0,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f253,plain,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f254,plain,
! [X0,X1] : constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f257,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f269,plain,
! [VAR_V_55] :
( pred_attacker(constr_pkey(VAR_V_55))
| ~ pred_attacker(VAR_V_55) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f270,plain,
! [X0] :
( pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f277,plain,
! [VAR_V_66] :
( pred_attacker(VAR_V_66)
| ~ pred_attacker(tuple_out_2(VAR_V_66)) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f278,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_out_2(X0)) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f285,plain,
! [VAR_V_79] :
( pred_attacker(VAR_V_79)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_79)) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f286,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(X0)) ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f287,plain,
! [VAR_V_83,VAR_V_84] :
( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_83,VAR_V_84))
| ~ pred_attacker(VAR_V_84)
| ~ pred_attacker(VAR_V_83) ),
inference(pre_NNF_transformation,[status(thm)],[f103]) ).
fof(f288,plain,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f292,plain,
! [VAR_V_94,VAR_V_95] :
( pred_attacker(VAR_V_95)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_94,VAR_V_95)) ),
inference(pre_NNF_transformation,[status(thm)],[f105]) ).
fof(f293,plain,
! [VAR_V_95] :
( pred_attacker(VAR_V_95)
| ! [VAR_V_94] : ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_94,VAR_V_95)) ),
inference(miniscoping,[status(thm)],[f292]) ).
fof(f294,plain,
! [X0,X1] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f295,plain,
! [VAR_V_99,VAR_V_10X300X30] :
( pred_attacker(tuple_key_register_server_in_1(VAR_V_99,VAR_V_10X300X30))
| ~ pred_attacker(VAR_V_10X300X30)
| ~ pred_attacker(VAR_V_99) ),
inference(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f296,plain,
! [X0,X1] :
( pred_attacker(tuple_key_register_server_in_1(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f312,plain,
! [VAR_V_127] :
( pred_attacker(VAR_V_127)
| ~ pred_attacker(tuple_client_B_out_6(VAR_V_127)) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f313,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_6(X0)) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f316,plain,
! [VAR_V_133] :
( pred_attacker(VAR_V_133)
| ~ pred_attacker(tuple_client_B_out_4(VAR_V_133)) ),
inference(pre_NNF_transformation,[status(thm)],[f116]) ).
fof(f317,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_4(X0)) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f326,plain,
! [VAR_V_152] :
( pred_attacker(tuple_client_B_in_5(VAR_V_152))
| ~ pred_attacker(VAR_V_152) ),
inference(pre_NNF_transformation,[status(thm)],[f120]) ).
fof(f327,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f330,plain,
! [VAR_V_158] :
( pred_attacker(tuple_client_B_in_3(VAR_V_158))
| ~ pred_attacker(VAR_V_158) ),
inference(pre_NNF_transformation,[status(thm)],[f122]) ).
fof(f331,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f334,plain,
! [VAR_V_164] :
( pred_attacker(tuple_client_B_in_2(VAR_V_164))
| ~ pred_attacker(VAR_V_164) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f335,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f364,plain,
! [VAR_V_215,VAR_V_216] :
( pred_attacker(constr_aenc(VAR_V_215,VAR_V_216))
| ~ pred_attacker(VAR_V_216)
| ~ pred_attacker(VAR_V_215) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f365,plain,
! [X0,X1] :
( pred_attacker(constr_aenc(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f366,plain,
! [VAR_V_219,VAR_V_220X30] :
( pred_attacker(constr_adec(VAR_V_219,VAR_V_220X30))
| ~ pred_attacker(VAR_V_220X30)
| ~ pred_attacker(VAR_V_219) ),
inference(pre_NNF_transformation,[status(thm)],[f139]) ).
fof(f367,plain,
! [X0,X1] :
( pred_attacker(constr_adec(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f373,plain,
! [VAR_V_227,VAR_V_228] :
( pred_attacker(tuple_2(VAR_V_227,VAR_V_228))
| ~ pred_attacker(VAR_V_228)
| ~ pred_attacker(VAR_V_227) ),
inference(pre_NNF_transformation,[status(thm)],[f145]) ).
fof(f374,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f378,plain,
! [VAR_V_238,VAR_V_239] :
( pred_attacker(VAR_V_239)
| ~ pred_attacker(tuple_2(VAR_V_238,VAR_V_239)) ),
inference(pre_NNF_transformation,[status(thm)],[f147]) ).
fof(f379,plain,
! [VAR_V_239] :
( pred_attacker(VAR_V_239)
| ! [VAR_V_238] : ~ pred_attacker(tuple_2(VAR_V_238,VAR_V_239)) ),
inference(miniscoping,[status(thm)],[f378]) ).
fof(f380,plain,
! [X0,X1] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_2(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f391,plain,
! [X0] : pred_attacker(name_new0x2Dname(X0)),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f395,plain,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f404,plain,
pred_attacker(tuple_client_B_out_1(name_B,name_A)),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f405,plain,
! [VAR_0X40SID_524,VAR_AENC_NA_A_522,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))))))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523))
| ~ 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_3(VAR_AENC_NA_A_522))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_522,name_skB))) ),
inference(pre_NNF_transformation,[status(thm)],[f165]) ).
fof(f406,plain,
! [VAR_AENC_NA_A_522,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))))))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_523))
| ~ 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_3(VAR_AENC_NA_A_522))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_522,name_skB))) ),
inference(miniscoping,[status(thm)],[f405]) ).
fof(f407,plain,
! [X0,X1,X2] :
( 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))))))
| ~ pred_attacker(tuple_client_B_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) ),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f408,plain,
! [VAR_0X40SID_546,VAR_AENC_NA_A_548,VAR_AENC_NB_547,VAR_SIGN_A_PKA_549] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549))
| ~ 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_3(VAR_AENC_NA_A_548))
| ~ 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_5(VAR_AENC_NB_547))
| ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB)) ),
inference(pre_NNF_transformation,[status(thm)],[f166]) ).
fof(f409,plain,
( pred_attacker(tuple_client_B_out_6(name_objective))
| ! [VAR_SIGN_A_PKA_549] :
( ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_549))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_549,constr_pkey(name_skS))))
| ! [VAR_AENC_NA_A_548] :
( ~ pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_548))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_548,name_skB)))
| ! [VAR_AENC_NB_547] :
( ~ pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_547))
| ! [VAR_0X40SID_546] : ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_546),constr_adec(VAR_AENC_NB_547,name_skB)) ) ) ) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f410,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X2,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f411,plain,
! [VAR_DST_588,VAR_PKDST_589,VAR_SRC_590X30] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588))
| ~ pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589)) ),
inference(pre_NNF_transformation,[status(thm)],[f167]) ).
fof(f412,plain,
! [VAR_DST_588,VAR_PKDST_589] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_588,VAR_PKDST_589),name_skS)))
| ! [VAR_SRC_590X30] : ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_590X30,VAR_DST_588))
| ~ pred_table(tuple_keys(VAR_DST_588,VAR_PKDST_589)) ),
inference(miniscoping,[status(thm)],[f411]) ).
fof(f413,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f414,plain,
! [VAR_HOST_642,VAR_PK_643] :
( pred_table(tuple_keys(VAR_HOST_642,VAR_PK_643))
| ~ pred_attacker(tuple_key_register_server_in_1(VAR_HOST_642,VAR_PK_643))
| VAR_HOST_642 = name_A
| VAR_HOST_642 = name_B ),
inference(pre_NNF_transformation,[status(thm)],[f168]) ).
fof(f415,plain,
! [X0,X1] :
( pred_table(tuple_keys(X0,X1))
| ~ pred_attacker(tuple_key_register_server_in_1(X0,X1))
| X0 = name_A
| X0 = name_B ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f416,plain,
? [VAR_V_651] : ~ pred_attacker(tuple_2(name_Nb(VAR_V_651),name_objective)),
inference(pre_NNF_transformation,[status(thm)],[f170]) ).
fof(f417,plain,
~ pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VAR_V_651,sK0_skl)],[f416]) ).
fof(f418,plain,
~ pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective)),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f419,definition,
! [X0,X1] :
( sQ0_spl
<=> ( ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f420,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ),
inference(component_clause,[status(thm)],[f419]) ).
fof(f422,definition,
! [X2] :
( sQ1_spl
<=> ( ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X2,name_skB))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f423,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,definition,
! [X3] :
( sQ2_spl
<=> ( ~ pred_attacker(tuple_client_B_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS)))) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f426,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(component_clause,[status(thm)],[f425]) ).
fof(f428,definition,
( sQ3_spl
<=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ3_spl
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,plain,
( sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f410,f419,f422,f425,f428]) ).
fof(f432,plain,
( ~ pred_attacker(name_objective)
| ~ pred_attacker(name_Nb(sK0_skl)) ),
inference(resolution,[status(thm)],[f374,f418]) ).
fof(f435,definition,
( sQ4_spl
<=> pred_attacker(name_Nb(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( sQ4_spl
| ~ pred_attacker(name_Nb(sK0_skl)) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f438,definition,
( sQ5_spl
<=> pred_attacker(name_objective) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ5_spl
| ~ pred_attacker(name_objective) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f441,plain,
( ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f432,f435,f438]) ).
fof(f442,definition,
! [X0] :
( sQ6_spl
<=> ~ pred_attacker(X0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f443,plain,
! [X0] :
( ~ sQ6_spl
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f450,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f429,f443]) ).
fof(f451,plain,
( ~ sQ3_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f450]) ).
fof(f458,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(tuple_client_B_in_2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f426,f257]) ).
fof(f472,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f391,f484]) ).
fof(f484,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f335,f458]) ).
fof(f485,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f472]) ).
fof(f486,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f257]) ).
fof(f487,plain,
! [X0,X1,X2] :
( 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))))))
| ~ pred_attacker(tuple_client_B_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f257]) ).
fof(f507,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f404,f524]) ).
fof(f524,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f331,f486]) ).
fof(f525,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f526,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f257]) ).
fof(f527,plain,
! [X0,X1,X2] :
( 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))))))
| ~ pred_attacker(tuple_client_B_in_2(X1))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f257]) ).
fof(f535,plain,
! [X0,X1,X2] :
( 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(X1))))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(X1,name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(paramodulation,[status(thm)],[f252,f527]) ).
fof(f537,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X3)),X2)))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X1,X2),name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(paramodulation,[status(thm)],[f253,f535]) ).
fof(f538,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(X0),name_Nb(X3)),X2)))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X1,X2),name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(constr_aenc(X0,constr_pkey(name_skB)))) ),
inference(paramodulation,[status(thm)],[f249,f537]) ).
fof(f546,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f391,f558]) ).
fof(f558,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f327,f526]) ).
fof(f559,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f546]) ).
fof(f597,plain,
! [X0,X1,X2,X3] :
( ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,X2),name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(constr_aenc(X0,constr_pkey(name_skB))))
| pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(X0),name_Nb(X1)),X2)) ),
inference(resolution,[status(thm)],[f317,f538]) ).
fof(f601,plain,
( ~ sQ3_spl
| pred_attacker(name_objective) ),
inference(resolution,[status(thm)],[f313,f429]) ).
fof(f609,plain,
! [X0,X1] :
( pred_attacker(X0)
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_aenc(X0,constr_pkey(X1))) ),
inference(paramodulation,[status(thm)],[f249,f367]) ).
fof(f624,plain,
! [X0,X1,X2,X3,X4] :
( ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X4,X2),name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(constr_aenc(tuple_2(X0,X3),constr_pkey(name_skB))))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X1)),X2)) ),
inference(paramodulation,[status(thm)],[f254,f597]) ).
fof(f634,plain,
pred_attacker(constr_pkey(name_skB)),
inference(resolution,[status(thm)],[f395,f278]) ).
fof(f636,plain,
! [X0,X1,X2,X3,X4] :
( ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X4,X3),name_skS)))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X2)),X3))
| ~ pred_attacker(constr_aenc(tuple_2(X0,X1),constr_pkey(name_skB))) ),
inference(resolution,[status(thm)],[f331,f624]) ).
fof(f652,plain,
! [X0,X1,X2] :
( pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(resolution,[status(thm)],[f413,f286]) ).
fof(f656,plain,
! [X0,X1,X2,X3,X4] :
( ~ pred_attacker(constr_pkey(name_skB))
| ~ pred_attacker(tuple_2(X0,X4))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,X2),name_skS)))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X1)),X2)) ),
inference(resolution,[status(thm)],[f636,f365]) ).
fof(f668,definition,
! [X0,X1,X2,X3,X4] :
( sQ12_spl
<=> ( ~ pred_attacker(tuple_2(X0,X4))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,X2),name_skS)))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X1)),X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f669,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ12_spl
| ~ pred_attacker(tuple_2(X0,X4))
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,X2),name_skS)))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X1)),X2)) ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f671,definition,
( sQ13_spl
<=> pred_attacker(constr_pkey(name_skB)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f673,plain,
( sQ13_spl
| ~ pred_attacker(constr_pkey(name_skB)) ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,plain,
( ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f656,f668,f671]) ).
fof(f676,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ12_spl
| ~ pred_attacker(constr_sign(tuple_2(X4,X2),name_skS))
| ~ pred_attacker(tuple_2(X0,X3))
| pred_attacker(constr_aenc(tuple_2(X0,name_Nb(X1)),X2)) ),
inference(resolution,[status(thm)],[f669,f335]) ).
fof(f696,plain,
! [X0,X1] :
( pred_table(tuple_keys(X0,X1))
| X0 = name_A
| X0 = name_B
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f296,f415]) ).
fof(f707,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ12_spl
| ~ pred_attacker(constr_sign(tuple_2(X4,constr_pkey(X0)),name_skS))
| ~ pred_attacker(tuple_2(X1,X3))
| pred_attacker(tuple_2(X1,name_Nb(X2)))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f609,f676]) ).
fof(f720,definition,
! [X0,X4] :
( sQ20_spl
<=> ( ~ pred_attacker(constr_sign(tuple_2(X4,constr_pkey(X0)),name_skS))
| ~ pred_attacker(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f721,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ pred_attacker(constr_sign(tuple_2(X1,constr_pkey(X0)),name_skS))
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,definition,
! [X1,X2,X3] :
( sQ21_spl
<=> ( ~ pred_attacker(tuple_2(X1,X3))
| pred_attacker(tuple_2(X1,name_Nb(X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f724,plain,
! [X0,X1,X2] :
( ~ sQ21_spl
| ~ pred_attacker(tuple_2(X0,X2))
| pred_attacker(tuple_2(X0,name_Nb(X1))) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f726,plain,
( ~ sQ12_spl
| sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f707,f720,f723,f668]) ).
fof(f727,definition,
! [X0] :
( sQ22_spl
<=> ( ~ pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f728,plain,
! [X0] :
( ~ sQ22_spl
| ~ pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f731,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f634]) ).
fof(f732,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f731]) ).
fof(f733,plain,
! [X0] :
( ~ sQ22_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f270]) ).
fof(f734,plain,
( ~ sQ3_spl
| ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f601,f733]) ).
fof(f756,plain,
( ~ sQ3_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f734]) ).
fof(f770,plain,
! [X0,X1,X2] :
( ~ sQ21_spl
| pred_attacker(name_Nb(X2))
| ~ pred_attacker(tuple_2(X0,X1)) ),
inference(resolution,[status(thm)],[f724,f380]) ).
fof(f771,definition,
! [X0,X1] :
( sQ23_spl
<=> ~ pred_attacker(tuple_2(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f772,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ pred_attacker(tuple_2(X0,X1)) ),
inference(component_clause,[status(thm)],[f771]) ).
fof(f774,definition,
! [X2] :
( sQ24_spl
<=> pred_attacker(name_Nb(X2)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f775,plain,
! [X0] :
( ~ sQ24_spl
| pred_attacker(name_Nb(X0)) ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f777,plain,
( ~ sQ21_spl
| sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f770,f771,f774,f723]) ).
fof(f778,plain,
( sQ4_spl
| ~ sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f437,f775]) ).
fof(f779,plain,
( sQ4_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f778]) ).
fof(f780,plain,
( sQ5_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f601]) ).
fof(f781,plain,
( sQ5_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f780]) ).
fof(f782,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f374,f772]) ).
fof(f783,plain,
( ~ sQ23_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f782,f442,f771]) ).
fof(f922,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,constr_pkey(X1))) ),
inference(resolution,[status(thm)],[f652,f721]) ).
fof(f926,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(constr_pkey(X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(X2)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(resolution,[status(thm)],[f922,f696]) ).
fof(f941,definition,
! [X0,X1] :
( sQ31_spl
<=> ( X1 = name_A
| X1 = name_B
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f942,plain,
! [X0,X1] :
( ~ sQ31_spl
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(component_clause,[status(thm)],[f941]) ).
fof(f944,plain,
( ~ sQ20_spl
| sQ22_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f926,f941,f727,f720]) ).
fof(f945,plain,
! [X0,X1] :
( ~ sQ31_spl
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f942,f294]) ).
fof(f960,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ pred_attacker(X0)
| ~ pred_attacker(X1)
| X0 = name_A
| X0 = name_B ),
inference(resolution,[status(thm)],[f945,f288]) ).
fof(f961,definition,
! [X0] :
( sQ34_spl
<=> ( ~ pred_attacker(X0)
| X0 = name_A
| X0 = name_B ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f962,plain,
! [X0] :
( ~ sQ34_spl
| ~ pred_attacker(X0)
| X0 = name_A
| X0 = name_B ),
inference(component_clause,[status(thm)],[f961]) ).
fof(f964,plain,
( ~ sQ31_spl
| sQ6_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f960,f961,f442,f941]) ).
fof(f976,plain,
( ~ sQ34_spl
| ~ pred_attacker(name_objective)
| name_objective = name_B ),
inference(resolution,[status(thm)],[f962,f224]) ).
fof(f1120,definition,
( sQ53_spl
<=> name_objective = name_B ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1121,plain,
( ~ sQ53_spl
| name_objective = name_B ),
inference(component_clause,[status(thm)],[f1120]) ).
fof(f1123,plain,
( ~ sQ34_spl
| ~ sQ5_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f976,f1120,f438,f961]) ).
fof(f1245,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1121,f230]) ).
fof(f1246,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1245]) ).
fof(f1247,plain,
$false,
inference(sat_refutation,[status(thm)],[f431,f441,f451,f485,f525,f559,f674,f726,f732,f756,f777,f779,f781,f783,f944,f964,f1123,f1246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW960+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 10:20:32 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.93/0.53 % Refutation found
% 0.93/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.93/0.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.93/0.54 % Elapsed time: 0.175909 seconds
% 0.93/0.54 % CPU time: 1.093199 seconds
% 0.93/0.54 % Total memory used: 126.932 MB
% 0.93/0.54 % Net memory used: 123.867 MB
%------------------------------------------------------------------------------