%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW967+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:09:50 PM UTC 2026
% Result : Theorem 0.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW967+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.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:37 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f84,axiom,(
% 0.12/0.43 (! [VAR_X_81,VAR_Y_82] : pred_eq_bitstring_bitstring(VAR_X_81,VAR_Y_82) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f110,axiom,(
% 0.12/0.43 (! [VAR_V_172] :( pred_attacker(tuple_client_A_out_9(VAR_V_172))=> pred_attacker(VAR_V_172) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f120,axiom,(
% 0.12/0.43 (! [VAR_V_218,VAR_V_219,VAR_V_220X30] :( pred_attacker(tuple_client_A_out_1(VAR_V_218,VAR_V_219,VAR_V_220X30))=> pred_attacker(VAR_V_220X30) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f121,axiom,(
% 0.12/0.43 (! [VAR_V_223] :( pred_attacker(VAR_V_223)=> pred_attacker(tuple_client_A_in_8(VAR_V_223)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f123,axiom,(
% 0.12/0.43 (! [VAR_V_229] :( pred_attacker(VAR_V_229)=> pred_attacker(tuple_client_A_in_6(VAR_V_229)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f125,axiom,(
% 0.12/0.43 (! [VAR_V_235] :( pred_attacker(VAR_V_235)=> pred_attacker(tuple_client_A_in_4(VAR_V_235)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f127,axiom,(
% 0.12/0.43 (! [VAR_V_241] :( pred_attacker(VAR_V_241)=> pred_attacker(tuple_client_A_in_2(VAR_V_241)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f168,axiom,(
% 0.12/0.43 (! [VAR_0X40SID_420X30] : pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(VAR_0X40SID_420X30))) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f170,axiom,(
% 0.12/0.43 (! [VAR_0X40SID_523,VAR_ENC_NA_B_ENC_KAB_A_522,VAR_ENC_NB_521] :( ( pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_521))& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_523),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))& pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_522)) )=> pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_521,constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))),constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f171,axiom,(
% 0.12/0.43 (! [VAR_0X40SID_572,VAR_ENC_KAB_A0X27_569,VAR_ENC_NA_B_ENC_KAB_A_571,VAR_ENC_NB_570X30] :( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_569,name_Kas)))& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_569))& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_570X30))& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_571,name_Kas)))& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_572),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_571,name_Kas)))& pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_571)) )=> pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(VAR_ENC_NB_570X30,VAR_ENC_NA_B_ENC_KAB_A_571,VAR_0X40SID_572),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_569,name_Kas))))) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f172,axiom,(
% 0.12/0.43 (! [VAR_0X40SID_598,VAR_ENC_KAB_A0X27_60X300X30,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_ENC_NB_596,VAR_ENC_SUCC_NA0X27_599] :( ( pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_596,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_0X40SID_598)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_599,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas))))& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_599))& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas)))& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X300X30))& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_596))& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas)))& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_598),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas)))& pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_597)) )=> pred_attacker(tuple_client_A_out_9(name_objective)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f175,conjecture,(
% 0.12/0.43 pred_attacker(name_objective) ),
% 0.12/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f176,negated_conjecture,(
% 0.12/0.43 ~(pred_attacker(name_objective) )),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f175])).
% 0.12/0.43 fof(f260,plain,(
% 0.12/0.43 ![X0,X1]: (pred_eq_bitstring_bitstring(X0,X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f84])).
% 0.12/0.43 fof(f312,plain,(
% 0.12/0.43 ![VAR_V_172]: (~pred_attacker(tuple_client_A_out_9(VAR_V_172))|pred_attacker(VAR_V_172))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 0.12/0.43 fof(f313,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(tuple_client_A_out_9(X0))|pred_attacker(X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f312])).
% 0.12/0.43 fof(f334,plain,(
% 0.12/0.43 ![VAR_V_218,VAR_V_219,VAR_V_220X30]: (~pred_attacker(tuple_client_A_out_1(VAR_V_218,VAR_V_219,VAR_V_220X30))|pred_attacker(VAR_V_220X30))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 0.12/0.43 fof(f335,plain,(
% 0.12/0.43 ![VAR_V_220X30]: ((![VAR_V_218,VAR_V_219]: ~pred_attacker(tuple_client_A_out_1(VAR_V_218,VAR_V_219,VAR_V_220X30)))|pred_attacker(VAR_V_220X30))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f334])).
% 0.12/0.43 fof(f336,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_out_1(X0,X1,X2))|pred_attacker(X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f335])).
% 0.12/0.43 fof(f337,plain,(
% 0.12/0.43 ![VAR_V_223]: (~pred_attacker(VAR_V_223)|pred_attacker(tuple_client_A_in_8(VAR_V_223)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 0.12/0.43 fof(f338,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_8(X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f337])).
% 0.12/0.43 fof(f341,plain,(
% 0.12/0.43 ![VAR_V_229]: (~pred_attacker(VAR_V_229)|pred_attacker(tuple_client_A_in_6(VAR_V_229)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f123])).
% 0.12/0.43 fof(f342,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_6(X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f341])).
% 0.12/0.43 fof(f345,plain,(
% 0.12/0.43 ![VAR_V_235]: (~pred_attacker(VAR_V_235)|pred_attacker(tuple_client_A_in_4(VAR_V_235)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 0.12/0.43 fof(f346,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_4(X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f345])).
% 0.12/0.43 fof(f349,plain,(
% 0.12/0.43 ![VAR_V_241]: (~pred_attacker(VAR_V_241)|pred_attacker(tuple_client_A_in_2(VAR_V_241)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f127])).
% 0.12/0.43 fof(f350,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_client_A_in_2(X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f349])).
% 0.12/0.43 fof(f430,plain,(
% 0.12/0.43 ![X0]: (pred_attacker(tuple_client_A_out_1(name_A,name_B,name_Na(X0))))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f168])).
% 0.12/0.43 fof(f434,plain,(
% 0.12/0.43 ![VAR_0X40SID_523,VAR_ENC_NA_B_ENC_KAB_A_522,VAR_ENC_NB_521]: ((((~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_521))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_523),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_522)))|pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_521,constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))),constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f170])).
% 0.12/0.43 fof(f435,plain,(
% 0.12/0.43 ![VAR_ENC_NA_B_ENC_KAB_A_522,VAR_ENC_NB_521]: ((((~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_521))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))|(![VAR_0X40SID_523]: ~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_523),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_522)))|pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(VAR_ENC_NB_521,constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas)))),constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_522,name_Kas))))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f434])).
% 0.12/0.43 fof(f436,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(X0,constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(X1,name_Kas)))),constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(X1,name_Kas))))))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f435])).
% 0.12/0.43 fof(f437,plain,(
% 0.12/0.43 ![VAR_0X40SID_572,VAR_ENC_KAB_A0X27_569,VAR_ENC_NA_B_ENC_KAB_A_571,VAR_ENC_NB_570X30]: ((((((~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_569,name_Kas)))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_569)))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_570X30)))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_571,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_572),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_571,name_Kas))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_571)))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(VAR_ENC_NB_570X30,VAR_ENC_NA_B_ENC_KAB_A_571,VAR_0X40SID_572),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_569,name_Kas))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f171])).
% 0.12/0.43 fof(f438,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X0))|~pred_attacker(tuple_client_A_in_4(X1))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X2,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X3),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(X1,X2,X3),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas))))))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f437])).
% 0.12/0.43 fof(f439,plain,(
% 0.12/0.43 ![VAR_0X40SID_598,VAR_ENC_KAB_A0X27_60X300X30,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_ENC_NB_596,VAR_ENC_SUCC_NA0X27_599]: ((((((((~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_596,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_0X40SID_598)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_599,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_599)))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X300X30)))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_596)))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_598),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_597)))|pred_attacker(tuple_client_A_out_9(name_objective)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f172])).
% 0.12/0.43 fof(f440,plain,(
% 0.12/0.43 (![VAR_ENC_NA_B_ENC_KAB_A_597]: ((![VAR_0X40SID_598]: (((![VAR_ENC_NB_596]: ((![VAR_ENC_KAB_A0X27_60X300X30]: (((![VAR_ENC_SUCC_NA0X27_599]: (~pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_596,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_0X40SID_598)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_599,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas))))|~pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_599))))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas))))|~pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X300X30))))|~pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_596))))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas))))|~pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_598),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas)))))|~pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_597))))|pred_attacker(tuple_client_A_out_9(name_objective))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f439])).
% 0.12/0.43 fof(f441,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~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))))|~pred_attacker(tuple_client_A_in_8(X3))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X4,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X4))|~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_9(name_objective)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f440])).
% 0.12/0.43 fof(f448,plain,(
% 0.12/0.43 ~pred_attacker(name_objective)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f176])).
% 0.12/0.43 fof(f495,plain,(
% 0.12/0.43 ![X0]: (pred_attacker(name_Na(X0)))),
% 0.12/0.43 inference(resolution,[status(thm)],[f430,f336])).
% 0.12/0.43 fof(f501,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_5(constr_cbc_enc_1(tuple_succ(constr_cbc_dec_1(X0,constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(X2,name_Kas)))),constr_tuple_4_get_2_bitstring(constr_cbc_dec_4(X2,name_Kas))))))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f436,f260])).
% 0.12/0.43 fof(f504,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_6(X0))|~pred_attacker(tuple_client_A_in_4(X1))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X2,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X3),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(X1,X2,X3),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X0,name_Kas))))))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f438,f260])).
% 0.12/0.43 fof(f505,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X1,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(X0,X1,X2),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X3,name_Kas)))))|~pred_attacker(X3))),
% 0.12/0.43 inference(resolution,[status(thm)],[f504,f342])).
% 0.12/0.43 fof(f506,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(X0,X2,X1),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X3,name_Kas)))))|~pred_attacker(X3))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f505,f260])).
% 0.12/0.43 fof(f507,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_8(X0))|~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X1,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X1))|~pred_attacker(tuple_client_A_in_4(X2))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X3,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X4),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))|pred_attacker(tuple_client_A_out_9(name_objective)))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f441,f260])).
% 0.12/0.43 fof(f508,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(X0,name_Kas)))|~pred_attacker(tuple_client_A_in_6(X0))|~pred_attacker(tuple_client_A_in_4(X1))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X2,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X3),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_9(name_objective))|~pred_attacker(X4))),
% 0.12/0.43 inference(resolution,[status(thm)],[f507,f338])).
% 0.12/0.43 fof(f509,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_6(X0))|~pred_attacker(tuple_client_A_in_4(X1))|~pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(X2,name_Kas)))|~pred_eq_bitstring_bitstring(name_Na(X3),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_9(name_objective))|~pred_attacker(X4))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f508,f260])).
% 0.12/0.43 fof(f542,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_7(constr_cbc_enc_1(name_Na0x27(X0,X1,X2),constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(X3,name_Kas)))))|~pred_attacker(X3))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f506,f260])).
% 0.12/0.43 fof(f544,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_6(X0))|~pred_attacker(tuple_client_A_in_4(X1))|~pred_eq_bitstring_bitstring(name_Na(X2),constr_tuple_4_get_0x30(constr_cbc_dec_4(X3,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X3))|pred_attacker(tuple_client_A_out_9(name_objective))|~pred_attacker(X4))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f509,f260])).
% 0.12/0.43 fof(f545,plain,(
% 0.12/0.43 ![X0,X1,X2,X3,X4]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2))|pred_attacker(tuple_client_A_out_9(name_objective))|~pred_attacker(X3)|~pred_attacker(X4))),
% 0.12/0.43 inference(resolution,[status(thm)],[f544,f342])).
% 0.12/0.43 fof(f546,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1))|pred_attacker(tuple_client_A_out_9(name_objective))|~pred_attacker(X2)|~pred_attacker(X3))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f545,f260])).
% 0.12/0.43 fof(f560,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1))|~pred_attacker(X2)|~pred_attacker(X3)|pred_attacker(name_objective))),
% 0.12/0.43 inference(resolution,[status(thm)],[f546,f313])).
% 0.12/0.43 fof(f561,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1))|~pred_attacker(X2)|~pred_attacker(X3))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f560,f448])).
% 0.12/0.43 fof(f562,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1))|~pred_attacker(X2))),
% 0.12/0.43 inference(backward_subsumption_resolution,[status(thm)],[f542,f561])).
% 0.12/0.43 fof(f566,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_eq_bitstring_bitstring(name_Na(X1),constr_tuple_4_get_0x30(constr_cbc_dec_4(X2,name_Kas)))|~pred_attacker(tuple_client_A_in_2(X2)))),
% 0.12/0.43 inference(backward_subsumption_resolution,[status(thm)],[f501,f562])).
% 0.12/0.43 fof(f568,plain,(
% 0.12/0.43 ![X0,X1]: (~pred_attacker(tuple_client_A_in_4(X0))|~pred_attacker(tuple_client_A_in_2(X1)))),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f566,f260])).
% 0.12/0.43 fof(f569,plain,(
% 0.12/0.43 ![X0,X1]: (~pred_attacker(tuple_client_A_in_2(X0))|~pred_attacker(X1))),
% 0.12/0.43 inference(resolution,[status(thm)],[f568,f346])).
% 0.12/0.43 fof(f570,plain,(
% 0.12/0.43 ![X0]: (~pred_attacker(X0))),
% 0.12/0.43 inference(backward_subsumption_resolution,[status(thm)],[f350,f569])).
% 0.12/0.43 fof(f575,plain,(
% 0.12/0.43 $false),
% 0.12/0.43 inference(backward_subsumption_resolution,[status(thm)],[f495,f570])).
% 0.12/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.082681 seconds
% 0.12/0.45 % CPU time: 0.366102 seconds
% 0.12/0.45 % Total memory used: 59.993 MB
% 0.12/0.45 % Net memory used: 59.341 MB
%------------------------------------------------------------------------------