%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:08:36 PM UTC 2026
% Result : Theorem 3.29s 0.85s
% Output : CNFRefutation 3.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 45
% Syntax : Number of formulae : 169 ( 32 unt; 17 def)
% Number of atoms : 421 ( 38 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 476 ( 224 ~; 203 |; 15 &)
% ( 17 <=>; 17 =>; 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 : 33 ( 33 usr; 7 con; 0-4 aty)
% Number of variables : 222 ( 221 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,axiom,
name_A != name_I,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
name_B != name_I,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [VAR_K_44,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_44),constr_pkey(VAR_K_44)) = VAR_M_0X30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [VAR_K_38,VAR_X1_35,VAR_X2_36,VAR_X3_37] : constr_ecb_dec_3(constr_ecb_enc_3(VAR_X1_35,VAR_X2_36,VAR_X3_37,constr_pkey(VAR_K_38)),VAR_K_38) = tuple_3(VAR_X1_35,VAR_X2_36,VAR_X3_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [VAR_X0X30_16,VAR_X1_17] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_16,VAR_X1_17)) = VAR_X1_17,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [VAR_X_66,VAR_Y_67] : pred_eq_bitstring_bitstring(VAR_X_66,VAR_Y_67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [VAR_V_91] :
( pred_attacker(VAR_V_91)
=> pred_attacker(constr_pkey(VAR_V_91)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [VAR_V_115] :
( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_115))
=> pred_attacker(VAR_V_115) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [VAR_V_119,VAR_V_120X30] :
( ( pred_attacker(VAR_V_120X30)
& pred_attacker(VAR_V_119) )
=> pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_119,VAR_V_120X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,axiom,
! [VAR_V_130X30,VAR_V_131] :
( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_130X30,VAR_V_131))
=> pred_attacker(VAR_V_131) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [VAR_V_135,VAR_V_136] :
( ( pred_attacker(VAR_V_136)
& pred_attacker(VAR_V_135) )
=> pred_attacker(tuple_key_register_server_in_1(VAR_V_135,VAR_V_136)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [VAR_V_189,VAR_V_190X30] :
( ( pred_attacker(VAR_V_190X30)
& pred_attacker(VAR_V_189) )
=> pred_attacker(constr_ecb_dec_3(VAR_V_189,VAR_V_190X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [VAR_V_20X307] :
( pred_attacker(tuple_client_B_out_6(VAR_V_20X307))
=> pred_attacker(VAR_V_20X307) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
! [VAR_V_213] :
( pred_attacker(tuple_client_B_out_4(VAR_V_213))
=> pred_attacker(VAR_V_213) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [VAR_V_232] :
( pred_attacker(VAR_V_232)
=> pred_attacker(tuple_client_B_in_5(VAR_V_232)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [VAR_V_238] :
( pred_attacker(VAR_V_238)
=> pred_attacker(tuple_client_B_in_3(VAR_V_238)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [VAR_V_244] :
( pred_attacker(VAR_V_244)
=> pred_attacker(tuple_client_B_in_2(VAR_V_244)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
! [VAR_V_367,VAR_V_368,VAR_V_369] :
( pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369))
=> pred_attacker(VAR_V_368) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [VAR_V_377,VAR_V_378] :
( ( pred_attacker(VAR_V_378)
& pred_attacker(VAR_V_377) )
=> pred_attacker(tuple_2(VAR_V_377,VAR_V_378)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,axiom,
pred_attacker(name_I),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [VAR_V_397] : pred_attacker(name_new0x2Dname(VAR_V_397)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,axiom,
pred_attacker(tuple_client_A_out_1(name_A,name_I)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,axiom,
pred_attacker(tuple_client_B_out_1(name_B,name_A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,axiom,
! [VAR_0X40SID_688,VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687] :
( ( pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB))) )
=> pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,axiom,
! [VAR_0X40SID_718,VAR_ECB_ENC_NA_A_720X30,VAR_ECB_ENC_NB_719,VAR_SIGN_A_PKA_721] :
( ( pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB)))
& pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719))
& pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,axiom,
! [VAR_DST_760X30,VAR_PKDST_761,VAR_SRC_762] :
( ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30))
& pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761)) )
=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,axiom,
! [VAR_HOST_814,VAR_PK_815] :
( ( pred_attacker(tuple_key_register_server_in_1(VAR_HOST_814,VAR_PK_815))
& VAR_HOST_814 != name_A
& VAR_HOST_814 != name_B )
=> pred_table(tuple_keys(VAR_HOST_814,VAR_PK_815)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,conjecture,
! [VAR_V_823] : pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,negated_conjecture,
~ ! [VAR_V_823] : pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)),
inference(negated_conjecture,[status(cth)],[f196]) ).
fof(f249,plain,
name_A != name_I,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f255,plain,
name_B != name_I,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f278,plain,
! [X0,X1] : constr_checksign(constr_sign(X0,X1),constr_pkey(X1)) = X0,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f280,plain,
! [X0,X1,X2,X3] : constr_ecb_dec_3(constr_ecb_enc_3(X0,X1,X2,constr_pkey(X3)),X3) = tuple_3(X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f287,plain,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f293,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f311,plain,
! [VAR_V_91] :
( pred_attacker(constr_pkey(VAR_V_91))
| ~ pred_attacker(VAR_V_91) ),
inference(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f312,plain,
! [X0] :
( pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f327,plain,
! [VAR_V_115] :
( pred_attacker(VAR_V_115)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_115)) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f328,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(X0)) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f329,plain,
! [VAR_V_119,VAR_V_120X30] :
( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_119,VAR_V_120X30))
| ~ pred_attacker(VAR_V_120X30)
| ~ pred_attacker(VAR_V_119) ),
inference(pre_NNF_transformation,[status(thm)],[f115]) ).
fof(f330,plain,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f334,plain,
! [VAR_V_130X30,VAR_V_131] :
( pred_attacker(VAR_V_131)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_130X30,VAR_V_131)) ),
inference(pre_NNF_transformation,[status(thm)],[f117]) ).
fof(f335,plain,
! [VAR_V_131] :
( pred_attacker(VAR_V_131)
| ! [VAR_V_130X30] : ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_130X30,VAR_V_131)) ),
inference(miniscoping,[status(thm)],[f334]) ).
fof(f336,plain,
! [X0,X1] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f337,plain,
! [VAR_V_135,VAR_V_136] :
( pred_attacker(tuple_key_register_server_in_1(VAR_V_135,VAR_V_136))
| ~ pred_attacker(VAR_V_136)
| ~ pred_attacker(VAR_V_135) ),
inference(pre_NNF_transformation,[status(thm)],[f118]) ).
fof(f338,plain,
! [X0,X1] :
( pred_attacker(tuple_key_register_server_in_1(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f360,plain,
! [VAR_V_189,VAR_V_190X30] :
( pred_attacker(constr_ecb_dec_3(VAR_V_189,VAR_V_190X30))
| ~ pred_attacker(VAR_V_190X30)
| ~ pred_attacker(VAR_V_189) ),
inference(pre_NNF_transformation,[status(thm)],[f129]) ).
fof(f361,plain,
! [X0,X1] :
( pred_attacker(constr_ecb_dec_3(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f370,plain,
! [VAR_V_20X307] :
( pred_attacker(VAR_V_20X307)
| ~ pred_attacker(tuple_client_B_out_6(VAR_V_20X307)) ),
inference(pre_NNF_transformation,[status(thm)],[f134]) ).
fof(f371,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_6(X0)) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f374,plain,
! [VAR_V_213] :
( pred_attacker(VAR_V_213)
| ~ pred_attacker(tuple_client_B_out_4(VAR_V_213)) ),
inference(pre_NNF_transformation,[status(thm)],[f136]) ).
fof(f375,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_4(X0)) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f384,plain,
! [VAR_V_232] :
( pred_attacker(tuple_client_B_in_5(VAR_V_232))
| ~ pred_attacker(VAR_V_232) ),
inference(pre_NNF_transformation,[status(thm)],[f140]) ).
fof(f385,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f388,plain,
! [VAR_V_238] :
( pred_attacker(tuple_client_B_in_3(VAR_V_238))
| ~ pred_attacker(VAR_V_238) ),
inference(pre_NNF_transformation,[status(thm)],[f142]) ).
fof(f389,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f392,plain,
! [VAR_V_244] :
( pred_attacker(tuple_client_B_in_2(VAR_V_244))
| ~ pred_attacker(VAR_V_244) ),
inference(pre_NNF_transformation,[status(thm)],[f144]) ).
fof(f393,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f446,plain,
! [VAR_V_367,VAR_V_368,VAR_V_369] :
( pred_attacker(VAR_V_368)
| ~ pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369)) ),
inference(pre_NNF_transformation,[status(thm)],[f170]) ).
fof(f447,plain,
! [VAR_V_368] :
( pred_attacker(VAR_V_368)
| ! [VAR_V_367,VAR_V_369] : ~ pred_attacker(tuple_3(VAR_V_367,VAR_V_368,VAR_V_369)) ),
inference(miniscoping,[status(thm)],[f446]) ).
fof(f448,plain,
! [X0,X1,X2] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_3(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f452,plain,
! [VAR_V_377,VAR_V_378] :
( pred_attacker(tuple_2(VAR_V_377,VAR_V_378))
| ~ pred_attacker(VAR_V_378)
| ~ pred_attacker(VAR_V_377) ),
inference(pre_NNF_transformation,[status(thm)],[f172]) ).
fof(f453,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f452]) ).
fof(f466,plain,
pred_attacker(name_I),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f470,plain,
! [X0] : pred_attacker(name_new0x2Dname(X0)),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f476,plain,
pred_attacker(tuple_client_A_out_1(name_A,name_I)),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f483,plain,
pred_attacker(tuple_client_B_out_1(name_B,name_A)),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f484,plain,
! [VAR_0X40SID_688,VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB))) ),
inference(pre_NNF_transformation,[status(thm)],[f192]) ).
fof(f485,plain,
! [VAR_ECB_ENC_NA_A_686,VAR_SIGN_A_PKA_687] :
( ! [VAR_0X40SID_688] : pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB)),name_Nb(VAR_0X40SID_688),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_687))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_687,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_686))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_686,name_skB))) ),
inference(miniscoping,[status(thm)],[f484]) ).
fof(f486,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ 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_ecb_dec_2(X0,name_skB))) ),
inference(cnf_transformation,[status(thm)],[f485]) ).
fof(f487,plain,
! [VAR_0X40SID_718,VAR_ECB_ENC_NA_A_720X30,VAR_ECB_ENC_NB_719,VAR_SIGN_A_PKA_721] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719))
| ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB)) ),
inference(pre_NNF_transformation,[status(thm)],[f193]) ).
fof(f488,plain,
( pred_attacker(tuple_client_B_out_6(name_objective))
| ! [VAR_SIGN_A_PKA_721] :
( ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_721))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_721,constr_pkey(name_skS))))
| ! [VAR_ECB_ENC_NA_A_720X30] :
( ~ pred_attacker(tuple_client_B_in_3(VAR_ECB_ENC_NA_A_720X30))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(VAR_ECB_ENC_NA_A_720X30,name_skB)))
| ! [VAR_ECB_ENC_NB_719] :
( ~ pred_attacker(tuple_client_B_in_5(VAR_ECB_ENC_NB_719))
| ! [VAR_0X40SID_718] : ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_718),constr_ecb_dec_1(VAR_ECB_ENC_NB_719,name_skB)) ) ) ) ),
inference(miniscoping,[status(thm)],[f487]) ).
fof(f489,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_ecb_dec_2(X2,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB)) ),
inference(cnf_transformation,[status(thm)],[f488]) ).
fof(f490,plain,
! [VAR_DST_760X30,VAR_PKDST_761,VAR_SRC_762] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30))
| ~ pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761)) ),
inference(pre_NNF_transformation,[status(thm)],[f194]) ).
fof(f491,plain,
! [VAR_DST_760X30,VAR_PKDST_761] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_760X30,VAR_PKDST_761),name_skS)))
| ! [VAR_SRC_762] : ~ pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_762,VAR_DST_760X30))
| ~ pred_table(tuple_keys(VAR_DST_760X30,VAR_PKDST_761)) ),
inference(miniscoping,[status(thm)],[f490]) ).
fof(f492,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)],[f491]) ).
fof(f493,plain,
! [VAR_HOST_814,VAR_PK_815] :
( pred_table(tuple_keys(VAR_HOST_814,VAR_PK_815))
| ~ pred_attacker(tuple_key_register_server_in_1(VAR_HOST_814,VAR_PK_815))
| VAR_HOST_814 = name_A
| VAR_HOST_814 = name_B ),
inference(pre_NNF_transformation,[status(thm)],[f195]) ).
fof(f494,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)],[f493]) ).
fof(f495,plain,
? [VAR_V_823] : ~ pred_attacker(tuple_2(name_Nb(VAR_V_823),name_objective)),
inference(pre_NNF_transformation,[status(thm)],[f197]) ).
fof(f496,plain,
~ pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VAR_V_823,sK0_skl)],[f495]) ).
fof(f497,plain,
~ pred_attacker(tuple_2(name_Nb(sK0_skl),name_objective)),
inference(cnf_transformation,[status(thm)],[f496]) ).
fof(f498,definition,
! [X0,X1] :
( sQ0_spl
<=> ( ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f499,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB)) ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f501,definition,
! [X2] :
( sQ1_spl
<=> ( ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X2,name_skB))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f502,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X0,name_skB))) ),
inference(component_clause,[status(thm)],[f501]) ).
fof(f504,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(f505,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)],[f504]) ).
fof(f507,definition,
( sQ3_spl
<=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ3_spl
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,plain,
( sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f489,f498,f501,f504,f507]) ).
fof(f511,plain,
( ~ pred_attacker(name_objective)
| ~ pred_attacker(name_Nb(sK0_skl)) ),
inference(resolution,[status(thm)],[f453,f497]) ).
fof(f514,definition,
( sQ4_spl
<=> pred_attacker(name_Nb(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( sQ4_spl
| ~ pred_attacker(name_Nb(sK0_skl)) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f517,definition,
( sQ5_spl
<=> pred_attacker(name_objective) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( sQ5_spl
| ~ pred_attacker(name_objective) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f520,plain,
( ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f511,f514,f517]) ).
fof(f521,definition,
! [X0] :
( sQ6_spl
<=> ~ pred_attacker(X0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f522,plain,
! [X0] :
( ~ sQ6_spl
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f529,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f508,f522]) ).
fof(f530,plain,
( ~ sQ3_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f529]) ).
fof(f537,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(tuple_client_B_in_2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f505,f293]) ).
fof(f557,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f470,f569]) ).
fof(f569,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f537]) ).
fof(f570,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f557]) ).
fof(f571,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f293]) ).
fof(f572,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ 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)],[f486,f293]) ).
fof(f596,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f483,f613]) ).
fof(f613,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f571]) ).
fof(f614,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f596]) ).
fof(f615,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f293]) ).
fof(f616,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ pred_attacker(tuple_client_B_in_2(X1))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f572,f293]) ).
fof(f626,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f470,f638]) ).
fof(f638,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f385,f615]) ).
fof(f639,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f647,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X2),name_B,constr_tuple_2_get_1_bitstring(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)],[f278,f616]) ).
fof(f660,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X3),name_B,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)],[f287,f647]) ).
fof(f683,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(X0))
| pred_attacker(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X1),name_B,X2)) ),
inference(resolution,[status(thm)],[f375,f660]) ).
fof(f688,plain,
( ~ sQ3_spl
| pred_attacker(name_objective) ),
inference(resolution,[status(thm)],[f371,f508]) ).
fof(f694,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_3(X0,X1,X2))
| ~ pred_attacker(X3)
| ~ pred_attacker(constr_ecb_enc_3(X0,X1,X2,constr_pkey(X3))) ),
inference(paramodulation,[status(thm)],[f280,f361]) ).
fof(f802,definition,
! [X0] :
( sQ10_spl
<=> ( ~ pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f803,plain,
! [X0] :
( ~ sQ10_spl
| ~ pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f802]) ).
fof(f874,definition,
! [X3] :
( sQ18_spl
<=> ~ pred_attacker(tuple_client_B_in_3(X3)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f875,plain,
! [X0] :
( ~ sQ18_spl
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(component_clause,[status(thm)],[f874]) ).
fof(f905,plain,
! [X0] :
( ~ sQ18_spl
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f389,f875]) ).
fof(f906,plain,
( ~ sQ18_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f905,f521,f874]) ).
fof(f922,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_table(tuple_keys(X0,X1))
| X0 = name_A
| X0 = name_B ),
inference(resolution,[status(thm)],[f494,f338]) ).
fof(f929,plain,
! [X0] :
( ~ sQ10_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f803,f312]) ).
fof(f930,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)],[f492,f328]) ).
fof(f941,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f476,f929]) ).
fof(f963,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f941]) ).
fof(f1047,definition,
! [X1,X2] :
( sQ30_spl
<=> ( ~ pred_attacker(X2)
| ~ pred_attacker(constr_sign(tuple_2(X1,constr_pkey(X2)),name_skS)) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1048,plain,
! [X0,X1] :
( ~ sQ30_spl
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_sign(tuple_2(X0,constr_pkey(X1)),name_skS)) ),
inference(component_clause,[status(thm)],[f1047]) ).
fof(f1351,plain,
! [X0,X1,X2,X3] :
( ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,constr_pkey(X0)),name_skS)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| pred_attacker(tuple_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X2),name_B))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f694,f683]) ).
fof(f1354,definition,
! [X0,X3] :
( sQ50_spl
<=> ( ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X3,constr_pkey(X0)),name_skS)))
| ~ pred_attacker(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1355,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ pred_attacker(tuple_client_B_in_2(constr_sign(tuple_2(X1,constr_pkey(X0)),name_skS)))
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f1354]) ).
fof(f1357,definition,
! [X1,X2] :
( sQ51_spl
<=> ( ~ pred_attacker(tuple_client_B_in_3(X1))
| pred_attacker(tuple_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X2),name_B)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1358,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ pred_attacker(tuple_client_B_in_3(X0))
| pred_attacker(tuple_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),name_Nb(X1),name_B)) ),
inference(component_clause,[status(thm)],[f1357]) ).
fof(f1360,plain,
( sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1351,f1354,f1357]) ).
fof(f1377,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ pred_attacker(constr_sign(tuple_2(X1,constr_pkey(X0)),name_skS))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f1355,f393]) ).
fof(f1384,plain,
! [X0,X1,X2] :
( ~ sQ30_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)],[f930,f1048]) ).
fof(f1393,definition,
! [X0,X1] :
( sQ54_spl
<=> ( ~ pred_attacker(X1)
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1394,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ pred_attacker(X1)
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1397,plain,
! [X0,X1] :
( ~ sQ54_spl
| X1 = name_A
| X1 = name_B
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1394,f336]) ).
fof(f1398,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ pred_attacker(X0)
| ~ pred_attacker(X1)
| X0 = name_A
| X0 = name_B ),
inference(resolution,[status(thm)],[f1397,f330]) ).
fof(f1399,definition,
! [X0] :
( sQ55_spl
<=> ( ~ pred_attacker(X0)
| X0 = name_A
| X0 = name_B ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
! [X0] :
( ~ sQ55_spl
| ~ pred_attacker(X0)
| X0 = name_A
| X0 = name_B ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1402,plain,
( ~ sQ54_spl
| sQ6_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1398,f1399,f521,f1393]) ).
fof(f1468,plain,
( ~ sQ55_spl
| name_I = name_A
| name_I = name_B ),
inference(resolution,[status(thm)],[f1400,f466]) ).
fof(f1574,definition,
( sQ73_spl
<=> name_I = name_B ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1575,plain,
( ~ sQ73_spl
| name_I = name_B ),
inference(component_clause,[status(thm)],[f1574]) ).
fof(f1656,definition,
( sQ96_spl
<=> name_I = name_A ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1657,plain,
( ~ sQ96_spl
| name_I = name_A ),
inference(component_clause,[status(thm)],[f1656]) ).
fof(f1659,plain,
( ~ sQ55_spl
| sQ96_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1468,f1574,f1656,f1399]) ).
fof(f1725,plain,
( ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1575,f255]) ).
fof(f1726,plain,
~ sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1725]) ).
fof(f1729,plain,
( sQ5_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f519,f688]) ).
fof(f1730,plain,
( sQ5_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1729]) ).
fof(f1795,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_attacker(constr_pkey(X1))
| ~ pred_attacker(X0)
| X0 = name_A
| X0 = name_B ),
inference(resolution,[status(thm)],[f922,f1384]) ).
fof(f1797,plain,
( ~ sQ30_spl
| sQ10_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1795,f1393,f802,f1047]) ).
fof(f1799,plain,
( ~ sQ50_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1377,f1047,f1354]) ).
fof(f2017,plain,
( ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1657,f249]) ).
fof(f2018,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f2017]) ).
fof(f2238,plain,
! [X0,X1] :
( ~ sQ51_spl
| pred_attacker(name_Nb(X1))
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(resolution,[status(thm)],[f1358,f448]) ).
fof(f2241,definition,
! [X1] :
( sQ150_spl
<=> pred_attacker(name_Nb(X1)) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f2242,plain,
! [X0] :
( ~ sQ150_spl
| pred_attacker(name_Nb(X0)) ),
inference(component_clause,[status(thm)],[f2241]) ).
fof(f2244,plain,
( ~ sQ51_spl
| sQ150_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2238,f874,f2241,f1357]) ).
fof(f2247,plain,
( sQ4_spl
| ~ sQ150_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f516,f2242]) ).
fof(f2248,plain,
( sQ4_spl
| ~ sQ150_spl ),
inference(contradiction_clause,[status(thm)],[f2247]) ).
fof(f2249,plain,
$false,
inference(sat_refutation,[status(thm)],[f510,f520,f530,f570,f614,f639,f906,f963,f1360,f1402,f1659,f1726,f1730,f1797,f1799,f2018,f2244,f2248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:20:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 3.29/0.85 % Refutation found
% 3.29/0.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.29/0.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.29/0.88 % Elapsed time: 0.497763 seconds
% 3.29/0.88 % CPU time: 3.600281 seconds
% 3.29/0.88 % Total memory used: 158.104 MB
% 3.29/0.88 % Net memory used: 151.045 MB
%------------------------------------------------------------------------------