%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW968+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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:08:36 PM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 36
% Syntax : Number of formulae : 136 ( 19 unt; 13 def)
% Number of atoms : 392 ( 8 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 491 ( 235 ~; 209 |; 18 &)
% ( 13 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 14 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 6 con; 0-5 aty)
% Number of variables : 231 ( 231 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f81,axiom,
! [VAR_K_53,VAR_X0X30_51,VAR_X1_52] : constr_cbc_dec_2(constr_cbc_enc_2(VAR_X0X30_51,VAR_X1_52,VAR_K_53),VAR_K_53) = tuple_2(VAR_X0X30_51,VAR_X1_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [VAR_K_43,VAR_X0X30_39,VAR_X1_40X30,VAR_X2_41,VAR_X3_42] : constr_cbc_4_get_2_prefixes(constr_cbc_enc_4(VAR_X0X30_39,VAR_X1_40X30,VAR_X2_41,VAR_X3_42,VAR_K_43)) = constr_cbc_enc_2(VAR_X0X30_39,VAR_X1_40X30,VAR_K_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [VAR_K_0X30,VAR_M_0X30] : constr_dec(constr_enc(VAR_M_0X30,VAR_K_0X30),VAR_K_0X30) = VAR_M_0X30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [VAR_X0X30_13,VAR_X1_14] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_13,VAR_X1_14)) = VAR_X0X30_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [VAR_X_81,VAR_Y_82] : pred_eq_bitstring_bitstring(VAR_X_81,VAR_Y_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,axiom,
! [VAR_V_10X309] :
( pred_attacker(tuple_server_S_out_2(VAR_V_10X309))
=> pred_attacker(VAR_V_10X309) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [VAR_V_114,VAR_V_115,VAR_V_116] :
( ( pred_attacker(VAR_V_116)
& pred_attacker(VAR_V_115)
& pred_attacker(VAR_V_114) )
=> pred_attacker(tuple_server_S_in_1(VAR_V_114,VAR_V_115,VAR_V_116)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [VAR_V_148,VAR_V_149] :
( ( pred_attacker(VAR_V_149)
& pred_attacker(VAR_V_148) )
=> pred_attacker(constr_dec(VAR_V_148,VAR_V_149)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [VAR_V_172] :
( pred_attacker(tuple_client_A_out_9(VAR_V_172))
=> pred_attacker(VAR_V_172) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [VAR_V_196] :
( pred_attacker(tuple_client_A_out_10(VAR_V_196))
=> pred_attacker(VAR_V_196) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [VAR_V_224,VAR_V_225,VAR_V_226] :
( pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226))
=> pred_attacker(VAR_V_226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,axiom,
! [VAR_V_229] :
( pred_attacker(VAR_V_229)
=> pred_attacker(tuple_client_A_in_8(VAR_V_229)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [VAR_V_235] :
( pred_attacker(VAR_V_235)
=> pred_attacker(tuple_client_A_in_6(VAR_V_235)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [VAR_V_241] :
( pred_attacker(VAR_V_241)
=> pred_attacker(tuple_client_A_in_4(VAR_V_241)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [VAR_V_244] :
( pred_attacker(tuple_client_A_in_4(VAR_V_244))
=> pred_attacker(VAR_V_244) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [VAR_V_247] :
( pred_attacker(VAR_V_247)
=> pred_attacker(tuple_client_A_in_2(VAR_V_247)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [VAR_V_299] :
( pred_attacker(VAR_V_299)
=> pred_attacker(constr_cbc_4_get_2_prefixes(VAR_V_299)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [VAR_V_392,VAR_V_393] :
( ( pred_attacker(VAR_V_393)
& pred_attacker(VAR_V_392) )
=> pred_attacker(tuple_2(VAR_V_392,VAR_V_393)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [VAR_0X40SID_426] : pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(VAR_0X40SID_426))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [VAR_0X40SID_60X304,VAR_ENC_KAB_A0X27_60X306,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_ENC_NB_60X302,VAR_ENC_SUCC_NA0X27_60X305] :
( ( pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303))
& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302))
& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))
& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305))
& pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))) )
=> pred_attacker(tuple_client_A_out_9(name_objective1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,axiom,
! [VAR_0X40SID_622,VAR_ENC_KAB_A0X27_624,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_ENC_NB_620X30,VAR_ENC_SUCC_NA0X27_623] :
( ( pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621))
& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30))
& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))
& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623))
& pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))) )
=> pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,axiom,
! [VAR_0X40SID_758,VAR_A_755,VAR_B_756,VAR_NA_757] :
( pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757))
=> pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,conjecture,
pred_attacker(tuple_2(name_objective1,name_objective2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
~ pred_attacker(tuple_2(name_objective1,name_objective2)),
inference(negated_conjecture,[status(cth)],[f190]) ).
fof(f272,plain,
! [X0,X1,X2] : constr_cbc_dec_2(constr_cbc_enc_2(X0,X1,X2),X2) = tuple_2(X0,X1),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f275,plain,
! [X0,X1,X2,X3,X4] : constr_cbc_4_get_2_prefixes(constr_cbc_enc_4(X0,X1,X2,X3,X4)) = constr_cbc_enc_2(X0,X1,X4),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f280,plain,
! [X0,X1] : constr_dec(constr_enc(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f283,plain,
! [X0,X1] : constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f287,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f307,plain,
! [VAR_V_10X309] :
( pred_attacker(VAR_V_10X309)
| ~ pred_attacker(tuple_server_S_out_2(VAR_V_10X309)) ),
inference(pre_NNF_transformation,[status(thm)],[f107]) ).
fof(f308,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_server_S_out_2(X0)) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f309,plain,
! [VAR_V_114,VAR_V_115,VAR_V_116] :
( pred_attacker(tuple_server_S_in_1(VAR_V_114,VAR_V_115,VAR_V_116))
| ~ pred_attacker(VAR_V_116)
| ~ pred_attacker(VAR_V_115)
| ~ pred_attacker(VAR_V_114) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f310,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_server_S_in_1(X0,X1,X2))
| ~ pred_attacker(X2)
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f323,plain,
! [VAR_V_148,VAR_V_149] :
( pred_attacker(constr_dec(VAR_V_148,VAR_V_149))
| ~ pred_attacker(VAR_V_149)
| ~ pred_attacker(VAR_V_148) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f324,plain,
! [X0,X1] :
( pred_attacker(constr_dec(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f339,plain,
! [VAR_V_172] :
( pred_attacker(VAR_V_172)
| ~ pred_attacker(tuple_client_A_out_9(VAR_V_172)) ),
inference(pre_NNF_transformation,[status(thm)],[f122]) ).
fof(f340,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_out_9(X0)) ),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f355,plain,
! [VAR_V_196] :
( pred_attacker(VAR_V_196)
| ~ pred_attacker(tuple_client_A_out_10(VAR_V_196)) ),
inference(pre_NNF_transformation,[status(thm)],[f130]) ).
fof(f356,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_out_10(X0)) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f365,plain,
! [VAR_V_224,VAR_V_225,VAR_V_226] :
( pred_attacker(VAR_V_226)
| ~ pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226)) ),
inference(pre_NNF_transformation,[status(thm)],[f134]) ).
fof(f366,plain,
! [VAR_V_226] :
( pred_attacker(VAR_V_226)
| ! [VAR_V_224,VAR_V_225] : ~ pred_attacker(tuple_client_A_out_1(VAR_V_224,VAR_V_225,VAR_V_226)) ),
inference(miniscoping,[status(thm)],[f365]) ).
fof(f367,plain,
! [X0,X1,X2] :
( pred_attacker(X2)
| ~ pred_attacker(tuple_client_A_out_1(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f368,plain,
! [VAR_V_229] :
( pred_attacker(tuple_client_A_in_8(VAR_V_229))
| ~ pred_attacker(VAR_V_229) ),
inference(pre_NNF_transformation,[status(thm)],[f135]) ).
fof(f369,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_8(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f372,plain,
! [VAR_V_235] :
( pred_attacker(tuple_client_A_in_6(VAR_V_235))
| ~ pred_attacker(VAR_V_235) ),
inference(pre_NNF_transformation,[status(thm)],[f137]) ).
fof(f373,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_6(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f376,plain,
! [VAR_V_241] :
( pred_attacker(tuple_client_A_in_4(VAR_V_241))
| ~ pred_attacker(VAR_V_241) ),
inference(pre_NNF_transformation,[status(thm)],[f139]) ).
fof(f377,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [VAR_V_244] :
( pred_attacker(VAR_V_244)
| ~ pred_attacker(tuple_client_A_in_4(VAR_V_244)) ),
inference(pre_NNF_transformation,[status(thm)],[f140]) ).
fof(f379,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_in_4(X0)) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,plain,
! [VAR_V_247] :
( pred_attacker(tuple_client_A_in_2(VAR_V_247))
| ~ pred_attacker(VAR_V_247) ),
inference(pre_NNF_transformation,[status(thm)],[f141]) ).
fof(f381,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f402,plain,
! [VAR_V_299] :
( pred_attacker(constr_cbc_4_get_2_prefixes(VAR_V_299))
| ~ pred_attacker(VAR_V_299) ),
inference(pre_NNF_transformation,[status(thm)],[f152]) ).
fof(f403,plain,
! [X0] :
( pred_attacker(constr_cbc_4_get_2_prefixes(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f442,plain,
! [VAR_V_392,VAR_V_393] :
( pred_attacker(tuple_2(VAR_V_392,VAR_V_393))
| ~ pred_attacker(VAR_V_393)
| ~ pred_attacker(VAR_V_392) ),
inference(pre_NNF_transformation,[status(thm)],[f171]) ).
fof(f443,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f461,plain,
! [X0] : pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(X0))),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f470,plain,
! [VAR_0X40SID_60X304,VAR_ENC_KAB_A0X27_60X306,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_ENC_NB_60X302,VAR_ENC_SUCC_NA0X27_60X305] :
( pred_attacker(tuple_client_A_out_9(name_objective1))
| ~ pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303))
| ~ pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302))
| ~ pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))) ),
inference(pre_NNF_transformation,[status(thm)],[f186]) ).
fof(f471,plain,
( pred_attacker(tuple_client_A_out_9(name_objective1))
| ! [VAR_ENC_NA_B_ENC_KAB_A_60X303] :
( ~ pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_60X303))
| ! [VAR_0X40SID_60X304] :
( ~ pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_60X304),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_60X303,name_Kas)))
| ! [VAR_ENC_NB_60X302] :
( ~ pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_60X302))
| ! [VAR_ENC_KAB_A0X27_60X306] :
( ~ pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X306))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))
| ! [VAR_ENC_SUCC_NA0X27_60X305] :
( ~ pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_60X305))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_60X302,VAR_ENC_NA_B_ENC_KAB_A_60X303,VAR_0X40SID_60X304)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_60X305,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X306,name_Kas)))) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f470]) ).
fof(f472,plain,
! [X0,X1,X2,X3,X4] :
( pred_attacker(tuple_client_A_out_9(name_objective1))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(tuple_client_A_in_6(X4))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X3))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas)))) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f473,plain,
! [VAR_0X40SID_622,VAR_ENC_KAB_A0X27_624,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_ENC_NB_620X30,VAR_ENC_SUCC_NA0X27_623] :
( pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))))
| ~ pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621))
| ~ pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30))
| ~ pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))) ),
inference(pre_NNF_transformation,[status(thm)],[f187]) ).
fof(f474,plain,
! [VAR_ENC_KAB_A0X27_624] :
( pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))))
| ! [VAR_ENC_NA_B_ENC_KAB_A_621] :
( ~ pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_621))
| ! [VAR_0X40SID_622] :
( ~ pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_622),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_621,name_Kas)))
| ! [VAR_ENC_NB_620X30] :
( ~ pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_620X30))
| ~ pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_624))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))
| ! [VAR_ENC_SUCC_NA0X27_623] :
( ~ pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_623))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_620X30,VAR_ENC_NA_B_ENC_KAB_A_621,VAR_0X40SID_622)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_623,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_624,name_Kas)))) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f473]) ).
fof(f475,plain,
! [X0,X1,X2,X3,X4] :
( pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas)))))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(tuple_client_A_in_6(X4))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X3))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas)))) ),
inference(cnf_transformation,[status(thm)],[f474]) ).
fof(f479,plain,
! [VAR_0X40SID_758,VAR_A_755,VAR_B_756,VAR_NA_757] :
( pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas)))
| ~ pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757)) ),
inference(pre_NNF_transformation,[status(thm)],[f189]) ).
fof(f480,plain,
! [VAR_A_755,VAR_B_756,VAR_NA_757] :
( ! [VAR_0X40SID_758] : pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(VAR_NA_757,VAR_B_756,name_Kab_66(VAR_0X40SID_758),constr_cbc_enc_2(name_Kab_66(VAR_0X40SID_758),VAR_A_755,name_Kbs),name_Kas)))
| ~ pred_attacker(tuple_server_S_in_1(VAR_A_755,VAR_B_756,VAR_NA_757)) ),
inference(miniscoping,[status(thm)],[f479]) ).
fof(f481,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_server_S_out_2(constr_cbc_enc_4(X2,X1,name_Kab_66(X3),constr_cbc_enc_2(name_Kab_66(X3),X0,name_Kbs),name_Kas)))
| ~ pred_attacker(tuple_server_S_in_1(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f480]) ).
fof(f482,plain,
~ pred_attacker(tuple_2(name_objective1,name_objective2)),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f483,definition,
! [X0,X1,X2,X3,X4] :
( sQ0_spl
<=> ( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(tuple_client_A_in_6(X4))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X3))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas)))) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(tuple_client_A_in_6(X4))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X3))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(X0,X1,X2)),constr_cbc_dec_1(X3,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X4,name_Kas)))) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,definition,
( sQ1_spl
<=> pred_attacker(tuple_client_A_out_9(name_objective1)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( ~ sQ1_spl
| pred_attacker(tuple_client_A_out_9(name_objective1)) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f472,f483,f486]) ).
fof(f520,definition,
! [X1] :
( sQ3_spl
<=> ~ pred_attacker(X1) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f521,plain,
! [X0] :
( ~ sQ3_spl
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f520]) ).
fof(f529,definition,
! [X0] :
( sQ4_spl
<=> ( ~ pred_attacker(X0)
| ~ pred_attacker(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f530,plain,
! [X0] :
( ~ sQ4_spl
| ~ pred_attacker(X0)
| ~ pred_attacker(X0) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f533,plain,
! [X0,X1] :
( pred_attacker(X0)
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_enc(X0,X1)) ),
inference(paramodulation,[status(thm)],[f280,f324]) ).
fof(f534,plain,
! [X0] : pred_attacker(name_Na(X0)),
inference(resolution,[status(thm)],[f461,f367]) ).
fof(f547,plain,
( ~ pred_attacker(name_objective2)
| ~ pred_attacker(name_objective1) ),
inference(resolution,[status(thm)],[f443,f482]) ).
fof(f550,definition,
( sQ5_spl
<=> pred_attacker(name_objective1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ5_spl
| ~ pred_attacker(name_objective1) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,definition,
( sQ6_spl
<=> pred_attacker(name_objective2) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f556,plain,
( ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f547,f550,f553]) ).
fof(f568,plain,
( ~ sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f534,f521]) ).
fof(f582,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f568]) ).
fof(f587,plain,
! [X0,X1,X2,X3,X4] :
( pred_attacker(constr_cbc_enc_2(X0,X1,X4))
| ~ pred_attacker(constr_cbc_enc_4(X0,X1,X2,X3,X4)) ),
inference(paramodulation,[status(thm)],[f275,f403]) ).
fof(f621,plain,
! [X0,X1,X2,X3,X4] :
( pred_attacker(tuple_client_A_out_10(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X1,name_Kas)))))
| ~ pred_attacker(tuple_client_A_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X2))
| ~ pred_attacker(tuple_client_A_in_6(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f287]) ).
fof(f623,definition,
! [X0] :
( sQ8_spl
<=> ~ pred_attacker(tuple_client_A_in_8(X0)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f624,plain,
! [X0] :
( ~ sQ8_spl
| ~ pred_attacker(tuple_client_A_in_8(X0)) ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f629,definition,
! [X3] :
( sQ10_spl
<=> ~ pred_attacker(tuple_client_A_in_4(X3)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f630,plain,
! [X0] :
( ~ sQ10_spl
| ~ pred_attacker(tuple_client_A_in_4(X0)) ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f632,definition,
! [X4,X5] :
( sQ11_spl
<=> ( ~ pred_attacker(tuple_client_A_in_2(X4))
| ~ pred_eq_bitstring_bitstring(name_Na(X5),constr_tuple_4_get_0x30(constr_cbc_dec_4(X4,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X4,name_Kas))) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f633,plain,
! [X0,X1] :
( ~ sQ11_spl
| ~ pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X0,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X0,name_Kas))) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f636,plain,
! [X0,X1] :
( ~ sQ11_spl
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas))) ),
inference(forward_subsumption_resolution,[status(thm)],[f633,f287]) ).
fof(f646,plain,
! [X0,X1,X2,X3,X4] :
( ~ pred_attacker(tuple_client_A_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X2))
| ~ pred_attacker(tuple_client_A_in_6(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X1))
| pred_attacker(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))) ),
inference(resolution,[status(thm)],[f356,f621]) ).
fof(f648,definition,
! [X0] :
( sQ12_spl
<=> ( ~ pred_attacker(tuple_client_A_in_6(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))
| pred_attacker(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f649,plain,
! [X0] :
( ~ sQ12_spl
| ~ pred_attacker(tuple_client_A_in_6(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))
| pred_attacker(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,plain,
( sQ11_spl
| sQ10_spl
| sQ8_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f646,f648,f623,f629,f632]) ).
fof(f664,plain,
! [X0,X1,X2,X3] :
( ~ pred_attacker(tuple_server_S_in_1(X3,X1,X0))
| pred_attacker(constr_cbc_enc_4(X0,X1,name_Kab_66(X2),constr_cbc_enc_2(name_Kab_66(X2),X3,name_Kbs),name_Kas)) ),
inference(resolution,[status(thm)],[f308,f481]) ).
fof(f667,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_A_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(X2))
| ~ pred_attacker(tuple_client_A_in_6(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f484,f287]) ).
fof(f670,definition,
! [X1] :
( sQ13_spl
<=> ( ~ pred_attacker(tuple_client_A_in_6(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas))) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f671,plain,
! [X0] :
( ~ sQ13_spl
| ~ pred_attacker(tuple_client_A_in_6(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas))) ),
inference(component_clause,[status(thm)],[f670]) ).
fof(f681,plain,
! [X0] :
( ~ sQ10_spl
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f377,f630]) ).
fof(f682,plain,
( ~ sQ10_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f681,f520,f629]) ).
fof(f683,plain,
( ~ sQ0_spl
| sQ11_spl
| sQ10_spl
| sQ13_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f667,f623,f670,f629,f632,f483]) ).
fof(f686,plain,
! [X0] :
( ~ sQ8_spl
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f369,f624]) ).
fof(f687,plain,
( ~ sQ8_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f686,f520,f623]) ).
fof(f688,plain,
! [X0] :
( ~ sQ11_spl
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f636,f287]) ).
fof(f689,plain,
! [X0] :
( ~ sQ13_spl
| ~ pred_attacker(tuple_client_A_in_6(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f671,f287]) ).
fof(f690,plain,
! [X0] :
( ~ sQ11_spl
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f381,f688]) ).
fof(f691,plain,
( ~ sQ11_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f690,f520,f632]) ).
fof(f696,plain,
! [X0] :
( ~ sQ12_spl
| ~ pred_attacker(tuple_client_A_in_6(X0))
| pred_attacker(constr_enc(name_objective2,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f649,f287]) ).
fof(f698,plain,
! [X0] :
( ~ sQ13_spl
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f373,f689]) ).
fof(f699,plain,
( ~ sQ13_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f698,f520,f670]) ).
fof(f705,plain,
( ~ sQ1_spl
| pred_attacker(name_objective1) ),
inference(resolution,[status(thm)],[f487,f340]) ).
fof(f706,plain,
( ~ sQ1_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f552]) ).
fof(f707,plain,
( ~ sQ1_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f706]) ).
fof(f776,plain,
! [X0] :
( ~ sQ4_spl
| ~ pred_attacker(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f530]) ).
fof(f777,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f461,f776]) ).
fof(f793,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f777]) ).
fof(f932,plain,
! [X0] :
( ~ sQ12_spl
| pred_attacker(name_objective2)
| ~ pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_6(X0)) ),
inference(resolution,[status(thm)],[f696,f533]) ).
fof(f934,definition,
! [X0] :
( sQ24_spl
<=> ( ~ pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_6(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f935,plain,
! [X0] :
( ~ sQ24_spl
| ~ pred_attacker(constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_6(X0)) ),
inference(component_clause,[status(thm)],[f934]) ).
fof(f937,plain,
( ~ sQ12_spl
| sQ6_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f932,f934,f553,f648]) ).
fof(f940,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ pred_attacker(constr_tuple_2_get_0x30_bitstring(tuple_2(X0,X1)))
| ~ pred_attacker(tuple_client_A_in_6(constr_cbc_enc_2(X0,X1,name_Kas))) ),
inference(paramodulation,[status(thm)],[f272,f935]) ).
fof(f941,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_in_6(constr_cbc_enc_2(X0,X1,name_Kas))) ),
inference(forward_demodulation,[status(thm)],[f283,f940]) ).
fof(f953,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f941,f373]) ).
fof(f1021,plain,
! [X0,X1,X2] :
( pred_attacker(constr_cbc_enc_2(X2,X1,name_Kas))
| ~ pred_attacker(tuple_server_S_in_1(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f664,f587]) ).
fof(f1034,plain,
! [X0,X1,X2] :
( ~ pred_attacker(X0)
| ~ pred_attacker(X1)
| ~ pred_attacker(X2)
| pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas)) ),
inference(resolution,[status(thm)],[f1021,f310]) ).
fof(f1035,definition,
! [X0,X1] :
( sQ36_spl
<=> ( ~ pred_attacker(X0)
| ~ pred_attacker(X1)
| pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas)) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
! [X0,X1] :
( ~ sQ36_spl
| ~ pred_attacker(X0)
| ~ pred_attacker(X1)
| pred_attacker(constr_cbc_enc_2(X0,X1,name_Kas)) ),
inference(component_clause,[status(thm)],[f1035]) ).
fof(f1038,plain,
( sQ3_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1034,f1035,f520]) ).
fof(f1039,plain,
! [X0,X1] :
( ~ sQ36_spl
| ~ sQ24_spl
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1036,f953]) ).
fof(f1085,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ24_spl
| ~ pred_attacker(tuple_client_A_in_4(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f379,f1039]) ).
fof(f1142,plain,
( ~ sQ36_spl
| ~ sQ24_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f1085,f629,f934,f1035]) ).
fof(f1188,plain,
$false,
inference(sat_refutation,[status(thm)],[f489,f556,f582,f651,f682,f683,f687,f691,f699,f707,f793,f937,f1038,f1142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW968+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n010.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:21:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.44 % Elapsed time: 0.076751 seconds
% 0.13/0.44 % CPU time: 0.346437 seconds
% 0.13/0.44 % Total memory used: 77.636 MB
% 0.13/0.44 % Net memory used: 76.996 MB
%------------------------------------------------------------------------------