%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 03:30:36 PM UTC 2026
% Result : Theorem 4.09s 16.27s
% Output : CNFRefutation 4.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 36
% Syntax : Number of formulae : 237 ( 52 unt; 0 def)
% Number of atoms : 586 ( 51 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 648 ( 299 ~; 309 |; 17 &)
% ( 0 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 8 con; 0-4 aty)
% Number of variables : 417 ( 0 sgn 416 !; 1 ?; 217 :)
% Comments :
%------------------------------------------------------------------------------
fof(f54,axiom,
name_A != name_objective,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax53) ).
fof(f60,axiom,
name_B != name_objective,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax59) ).
fof(f81,axiom,
! [X0,X1] : constr_checksign(constr_sign(X1,X0),constr_pkey(X0)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax80) ).
fof(f84,axiom,
! [X0,X1,X2] : constr_ecb_dec_2(constr_ecb_enc_2(X1,X2,constr_pkey(X0)),X0) = tuple_2(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax83) ).
fof(f85,axiom,
! [X0,X1] : constr_ecb_dec_1(constr_ecb_enc_1(X1,constr_pkey(X0)),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax84) ).
fof(f87,axiom,
! [X0,X1,X2,X3] : constr_ecb_enc_3(X1,X2,X3,X0) = tuple_3(constr_ecb_enc_1(X1,X0),constr_ecb_enc_1(X2,X0),constr_ecb_enc_1(X3,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax86) ).
fof(f88,axiom,
! [X0,X1,X2] : constr_ecb_enc_2(X1,X2,X0) = tuple_2(constr_ecb_enc_1(X1,X0),constr_ecb_enc_1(X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax87) ).
fof(f90,axiom,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax89) ).
fof(f96,axiom,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax95) ).
fof(f106,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(constr_pkey(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax105) ).
fof(f114,axiom,
! [X0] :
( pred_attacker(tuple_key_retrieval_server_out_2(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax113) ).
fof(f115,axiom,
! [X0,X1] :
( ( pred_attacker(X1)
& pred_attacker(X0) )
=> pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax114) ).
fof(f118,axiom,
! [X0,X1] :
( ( pred_attacker(X1)
& pred_attacker(X0) )
=> pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax117) ).
fof(f130,axiom,
! [X0,X1] :
( ( pred_attacker(X1)
& pred_attacker(X0) )
=> pred_attacker(constr_ecb_dec_2(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax129) ).
fof(f131,axiom,
! [X0,X1] :
( ( pred_attacker(X1)
& pred_attacker(X0) )
=> pred_attacker(constr_ecb_dec_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax130) ).
fof(f134,axiom,
! [X0] :
( pred_attacker(tuple_client_B_out_6(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax133) ).
fof(f136,axiom,
! [X0] :
( pred_attacker(tuple_client_B_out_4(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax135) ).
fof(f140,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_5(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax139) ).
fof(f142,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_3(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax141) ).
fof(f144,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax143) ).
fof(f149,axiom,
! [X0] :
( pred_attacker(tuple_client_A_out_3(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax148) ).
fof(f155,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_A_in_2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax154) ).
fof(f170,axiom,
! [X0,X1,X2] :
( pred_attacker(tuple_3(X0,X1,X2))
=> pred_attacker(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax169) ).
fof(f171,axiom,
! [X0,X1,X2] :
( pred_attacker(tuple_3(X0,X1,X2))
=> pred_attacker(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax170) ).
fof(f172,axiom,
! [X0,X1] :
( ( pred_attacker(X1)
& pred_attacker(X0) )
=> pred_attacker(tuple_2(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax171) ).
fof(f173,axiom,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax172) ).
fof(f174,axiom,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
=> pred_attacker(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax173) ).
fof(f177,axiom,
pred_attacker(name_c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax176) ).
fof(f179,axiom,
pred_attacker(name_B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax178) ).
fof(f184,axiom,
pred_table(tuple_keys(name_B,constr_pkey(name_skB))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax183) ).
fof(f189,axiom,
! [X0,X1] :
( ( pred_attacker(tuple_client_A_in_2(X1))
& pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS)))) )
=> pred_attacker(tuple_client_A_out_3(constr_ecb_enc_2(name_Na(X0),name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax188) ).
fof(f192,axiom,
! [X0,X1,X2] :
( ( pred_attacker(tuple_client_B_in_2(X2))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_3(X1))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB))) )
=> pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X0),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax191) ).
fof(f193,axiom,
! [X0,X1,X2,X3] :
( ( 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(X1))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
& pred_attacker(tuple_client_B_in_5(X2))
& pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X2,name_skB)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax192) ).
fof(f194,axiom,
! [X0,X1,X2] :
( ( pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
& pred_table(tuple_keys(X0,X1)) )
=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax193) ).
fof(f195,axiom,
! [X0,X1] :
( ( pred_attacker(tuple_key_register_server_in_1(X0,X1))
& X0 != name_A
& X0 != name_B )
=> pred_table(tuple_keys(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax194) ).
fof(f196,conjecture,
! [X0] : pred_attacker(tuple_2(name_Nb(X0),name_objective)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co0) ).
fof(f197,negated_conjecture,
~ ! [X0] : pred_attacker(tuple_2(name_Nb(X0),name_objective)),
inference(negated_conjecture,[status(cth)],[f196]) ).
fof(f198,plain,
? [X0] : ~ pred_attacker(tuple_2(name_Nb(X0),name_objective)),
inference(ennf_transformation,[],[f197]) ).
fof(f199,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_2(X0,X1))
| pred_attacker(X1) ),
inference(ennf_transformation,[],[f174]) ).
fof(f200,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_2(X0,X1))
| pred_attacker(X0) ),
inference(ennf_transformation,[],[f173]) ).
fof(f201,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_2(X0,X1)) ),
inference(ennf_transformation,[],[f172]) ).
fof(f202,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_2(X0,X1)) ),
inference(flattening,[],[f201]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( ~ 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(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X2,name_skB))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(ennf_transformation,[],[f193]) ).
fof(f204,plain,
! [X0,X1,X2,X3] :
( ~ 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(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X2,name_skB))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(flattening,[],[f203]) ).
fof(f205,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_B_in_2(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X0),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
inference(ennf_transformation,[],[f192]) ).
fof(f206,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_B_in_2(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X0),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(constr_pkey(X0)) ),
inference(ennf_transformation,[],[f106]) ).
fof(f210,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_2(X0,X1)) ),
inference(ennf_transformation,[],[f130]) ).
fof(f211,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_2(X0,X1)) ),
inference(flattening,[],[f210]) ).
fof(f212,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_1(X0,X1)) ),
inference(ennf_transformation,[],[f131]) ).
fof(f213,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_1(X0,X1)) ),
inference(flattening,[],[f212]) ).
fof(f216,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_6(X0))
| pred_attacker(X0) ),
inference(ennf_transformation,[],[f134]) ).
fof(f219,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_5(X0)) ),
inference(ennf_transformation,[],[f140]) ).
fof(f221,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_3(X0)) ),
inference(ennf_transformation,[],[f142]) ).
fof(f223,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_2(X0)) ),
inference(ennf_transformation,[],[f144]) ).
fof(f228,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_4(X0))
| pred_attacker(X0) ),
inference(ennf_transformation,[],[f136]) ).
fof(f230,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,X1))
| pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))) ),
inference(ennf_transformation,[],[f194]) ).
fof(f231,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,X1))
| pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))) ),
inference(flattening,[],[f230]) ).
fof(f238,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_3(X0,X1,X2))
| pred_attacker(X2) ),
inference(ennf_transformation,[],[f171]) ).
fof(f239,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_3(X0,X1,X2))
| pred_attacker(X1) ),
inference(ennf_transformation,[],[f170]) ).
fof(f247,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_key_register_server_in_1(X0,X1))
| name_A = X0
| name_B = X0
| pred_table(tuple_keys(X0,X1)) ),
inference(ennf_transformation,[],[f195]) ).
fof(f248,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_key_register_server_in_1(X0,X1))
| name_A = X0
| name_B = X0
| pred_table(tuple_keys(X0,X1)) ),
inference(flattening,[],[f247]) ).
fof(f249,plain,
! [X0] :
( ~ pred_attacker(tuple_key_retrieval_server_out_2(X0))
| pred_attacker(X0) ),
inference(ennf_transformation,[],[f114]) ).
fof(f253,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(ennf_transformation,[],[f115]) ).
fof(f254,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(flattening,[],[f253]) ).
fof(f263,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_A_in_2(X0)) ),
inference(ennf_transformation,[],[f155]) ).
fof(f264,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| pred_attacker(tuple_client_A_out_3(constr_ecb_enc_2(name_Na(X0),name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))) ),
inference(ennf_transformation,[],[f189]) ).
fof(f265,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| pred_attacker(tuple_client_A_out_3(constr_ecb_enc_2(name_Na(X0),name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))) ),
inference(flattening,[],[f264]) ).
fof(f268,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(ennf_transformation,[],[f118]) ).
fof(f269,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(flattening,[],[f268]) ).
fof(f270,plain,
! [X0] :
( ~ pred_attacker(tuple_client_A_out_3(X0))
| pred_attacker(X0) ),
inference(ennf_transformation,[],[f149]) ).
fof(f272,plain,
~ pred_attacker(tuple_2(name_Nb(sK0),name_objective)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f198]) ).
fof(f273,plain,
~ pred_attacker(tuple_2(name_Nb(sK0),name_objective)),
inference(cnf_transformation,[],[f272]) ).
fof(f279,plain,
name_B != name_objective,
inference(cnf_transformation,[],[f60]) ).
fof(f280,plain,
name_A != name_objective,
inference(cnf_transformation,[],[f54]) ).
fof(f286,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_2(X0,X1))
| pred_attacker(X1) ),
inference(cnf_transformation,[],[f199]) ).
fof(f287,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_2(X0,X1))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f288,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_2(X0,X1)) ),
inference(cnf_transformation,[],[f202]) ).
fof(f289,plain,
! [X2,X3,X0,X1] :
( ~ 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(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X2,name_skB))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(cnf_transformation,[],[f204]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_client_B_in_2(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| pred_attacker(tuple_client_B_out_4(constr_ecb_enc_3(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),name_Nb(X0),name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
inference(cnf_transformation,[],[f206]) ).
fof(f321,plain,
pred_attacker(name_c),
inference(cnf_transformation,[],[f177]) ).
fof(f338,plain,
pred_attacker(name_B),
inference(cnf_transformation,[],[f179]) ).
fof(f366,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[],[f96]) ).
fof(f367,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(constr_pkey(X0)) ),
inference(cnf_transformation,[],[f207]) ).
fof(f369,plain,
! [X0,X1] : constr_checksign(constr_sign(X1,X0),constr_pkey(X0)) = X1,
inference(cnf_transformation,[],[f81]) ).
fof(f370,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_2(X0,X1)) ),
inference(cnf_transformation,[],[f211]) ).
fof(f371,plain,
! [X2,X0,X1] : constr_ecb_dec_2(constr_ecb_enc_2(X1,X2,constr_pkey(X0)),X0) = tuple_2(X1,X2),
inference(cnf_transformation,[],[f84]) ).
fof(f372,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_ecb_dec_1(X0,X1)) ),
inference(cnf_transformation,[],[f213]) ).
fof(f373,plain,
! [X0,X1] : constr_ecb_dec_1(constr_ecb_enc_1(X1,constr_pkey(X0)),X0) = X1,
inference(cnf_transformation,[],[f85]) ).
fof(f378,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_6(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f216]) ).
fof(f381,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_5(X0)) ),
inference(cnf_transformation,[],[f219]) ).
fof(f383,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_3(X0)) ),
inference(cnf_transformation,[],[f221]) ).
fof(f385,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_2(X0)) ),
inference(cnf_transformation,[],[f223]) ).
fof(f387,plain,
! [X2,X3,X0,X1] : constr_ecb_enc_3(X1,X2,X3,X0) = tuple_3(constr_ecb_enc_1(X1,X0),constr_ecb_enc_1(X2,X0),constr_ecb_enc_1(X3,X0)),
inference(cnf_transformation,[],[f87]) ).
fof(f390,plain,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
inference(cnf_transformation,[],[f90]) ).
fof(f393,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_4(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f395,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| ~ pred_table(tuple_keys(X0,X1))
| pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))) ),
inference(cnf_transformation,[],[f231]) ).
fof(f398,plain,
! [X2,X0,X1] : constr_ecb_enc_2(X1,X2,X0) = tuple_2(constr_ecb_enc_1(X1,X0),constr_ecb_enc_1(X2,X0)),
inference(cnf_transformation,[],[f88]) ).
fof(f400,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_3(X0,X1,X2))
| pred_attacker(X2) ),
inference(cnf_transformation,[],[f238]) ).
fof(f401,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_3(X0,X1,X2))
| pred_attacker(X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f406,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_key_register_server_in_1(X0,X1))
| name_A = X0
| name_B = X0
| pred_table(tuple_keys(X0,X1)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f407,plain,
pred_table(tuple_keys(name_B,constr_pkey(name_skB))),
inference(cnf_transformation,[],[f184]) ).
fof(f409,plain,
! [X0] :
( ~ pred_attacker(tuple_key_retrieval_server_out_2(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f413,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(cnf_transformation,[],[f254]) ).
fof(f425,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_A_in_2(X0)) ),
inference(cnf_transformation,[],[f263]) ).
fof(f426,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| pred_attacker(tuple_client_A_out_3(constr_ecb_enc_2(name_Na(X0),name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))) ),
inference(cnf_transformation,[],[f265]) ).
fof(f429,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(cnf_transformation,[],[f269]) ).
fof(f430,plain,
! [X0] :
( ~ pred_attacker(tuple_client_A_out_3(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f270]) ).
fof(f432,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_client_B_in_2(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))) ),
inference(definition_unfolding,[],[f290,f387]) ).
fof(f433,plain,
! [X2,X0,X1] : tuple_2(X1,X2) = constr_ecb_dec_2(tuple_2(constr_ecb_enc_1(X1,constr_pkey(X0)),constr_ecb_enc_1(X2,constr_pkey(X0))),X0),
inference(definition_unfolding,[],[f371,f398]) ).
fof(f437,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X1,constr_pkey(name_skS))))
| pred_attacker(tuple_client_A_out_3(tuple_2(constr_ecb_enc_1(name_Na(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))) ),
inference(definition_unfolding,[],[f426,f398]) ).
tcf(c_49,negated_conjecture,
~ pred_attacker(tuple_2(name_Nb(sK0),name_objective)),
inference(cnf_transformation,[],[f273]) ).
tcf(c_55,plain,
name_objective != name_B,
inference(cnf_transformation,[],[f279]) ).
tcf(c_56,plain,
name_objective != name_A,
inference(cnf_transformation,[],[f280]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_2(X0,X1)) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_2(X0,X1)) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(tuple_client_B_in_3(X3))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X3,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_Nb(X1),constr_ecb_dec_1(X2,name_skB))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(cnf_transformation,[],[f432]) ).
tcf(c_97,plain,
pred_attacker(name_c),
inference(cnf_transformation,[],[f321]) ).
tcf(c_114,plain,
pred_attacker(name_B),
inference(cnf_transformation,[],[f338]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[],[f366]) ).
tcf(c_143,plain,
! [X0: $i] :
( pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] : constr_checksign(constr_sign(X0,X1),constr_pkey(X1)) = X0,
inference(cnf_transformation,[],[f369]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_dec_2(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i] : constr_ecb_dec_2(tuple_2(constr_ecb_enc_1(X0,constr_pkey(X1)),constr_ecb_enc_1(X2,constr_pkey(X1))),X1) = tuple_2(X0,X2),
inference(cnf_transformation,[],[f433]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_dec_1(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i] : constr_ecb_dec_1(constr_ecb_enc_1(X0,constr_pkey(X1)),X1) = X0,
inference(cnf_transformation,[],[f373]) ).
tcf(c_154,plain,
! [X0: $i] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_6(X0)) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_157,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f381]) ).
tcf(c_159,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_161,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
inference(cnf_transformation,[],[f390]) ).
tcf(c_168,plain,
! [X0: $i] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_4(X0)) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X1,X2),name_skS)))
| ~ pred_table(tuple_keys(X1,X2))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(X2)
| ~ pred_attacker(tuple_3(X0,X1,X2)) ),
inference(cnf_transformation,[],[f400]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_3(X0,X1,X2)) ),
inference(cnf_transformation,[],[f401]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i] :
( pred_table(tuple_keys(X0,X1))
| ( X0 = name_A )
| ( X0 = name_B )
| ~ pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(cnf_transformation,[],[f406]) ).
tcf(c_181,plain,
pred_table(tuple_keys(name_B,constr_pkey(name_skB))),
inference(cnf_transformation,[],[f407]) ).
tcf(c_183,plain,
! [X0: $i] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(X0)) ),
inference(cnf_transformation,[],[f409]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_key_retrieval_server_in_1(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f413]) ).
tcf(c_199,plain,
! [X0: $i] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f425]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_client_A_out_3(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(cnf_transformation,[],[f437]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_key_register_server_in_1(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f429]) ).
tcf(c_204,plain,
! [X0: $i] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_out_3(X0)) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_274,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(prop_impl_just,[status(thm)],[c_161]) ).
tcf(c_302,plain,
! [X0: $i] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(prop_impl_just,[status(thm)],[c_199]) ).
tcf(c_571,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_in_3(X3))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X3,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_Nb(X1),constr_ecb_dec_1(X2,name_skB))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(bin_hyper_res,[status(thm)],[c_65,c_274]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X1,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X1,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(bin_hyper_res,[status(thm)],[c_66,c_274]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_client_A_out_3(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(X0)
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(bin_hyper_res,[status(thm)],[c_200,c_302]) ).
tcf(c_597,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_client_A_out_3(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_573,c_142]) ).
tcf(c_598,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(X3)
| ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_ecb_dec_2(X2,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_ecb_dec_1(X1,name_skB)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_571,c_142]) ).
tcf(c_600,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))
| ~ pred_attacker(X1)
| ~ 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(backward_subsumption_resolution,[status(thm)],[c_572,c_142]) ).
tcf(c_1029,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_600,c_142]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(X2)
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_attacker(tuple_client_B_in_5(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_598,c_142,c_142]) ).
tcf(c_1434,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(prop_impl_just,[status(thm)],[c_159]) ).
tcf(c_1446,plain,
! [X0: $i] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(prop_impl_just,[status(thm)],[c_157]) ).
tcf(c_1488,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_client_A_out_3(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))))
| ~ pred_attacker(X0) ),
inference(prop_impl_just,[status(thm)],[c_597]) ).
tcf(c_1727,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_4(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(bin_hyper_res,[status(thm)],[c_1029,c_1434]) ).
tcf(c_1729,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(X2)
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(bin_hyper_res,[status(thm)],[c_1072,c_1446]) ).
tcf(c_2544,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ pred_attacker(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1729]) ).
tcf(c_2545,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_1729]) ).
tcf(c_2546,plain,
( iPr_def_11
| iPr_def_10
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1729]) ).
tcf(c_4647,plain,
~ iPr_def_10,
inference(superposition,[status(thm)],[c_97,c_2544]) ).
tcf(c_4661,plain,
( iPr_def_11
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(global_subsumption_just,[status(thm)],[c_2546,c_2546,c_4647]) ).
tcf(c_4675,plain,
( iPr_def_11
| pred_attacker(name_objective) ),
inference(superposition,[status(thm)],[c_4661,c_154]) ).
tcf(c_4727,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_3(constr_ecb_enc_1(constr_tuple_2_get_0x30_bitstring(constr_ecb_dec_2(X0,name_skB)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))),constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_1727,c_168]) ).
tcf(c_4806,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_1488,c_204]) ).
tcf(c_4827,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_159,c_2545]) ).
tcf(c_4839,plain,
~ iPr_def_11,
inference(superposition,[status(thm)],[c_97,c_4827]) ).
tcf(c_4869,plain,
pred_attacker(name_objective),
inference(backward_subsumption_resolution,[status(thm)],[c_4675,c_4839]) ).
tcf(c_4894,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4727,c_174]) ).
tcf(c_4909,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X2),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS)))))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4727,c_175]) ).
tcf(c_4956,plain,
( ~ pred_attacker(name_objective)
| ~ pred_attacker(name_Nb(sK0)) ),
inference(superposition,[status(thm)],[c_64,c_49]) ).
tcf(c_4960,plain,
~ pred_attacker(name_Nb(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_4956,c_4869]) ).
tcf(c_4983,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(X0,X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_2(constr_ecb_enc_1(X0,constr_pkey(X1)),constr_ecb_enc_1(X2,constr_pkey(X1)))) ),
inference(superposition,[status(thm)],[c_147,c_146]) ).
tcf(c_4993,plain,
! [X0: $i,X1: $i] :
( pred_attacker(X0)
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(superposition,[status(thm)],[c_149,c_148]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_attacker(X2)
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_187,c_170]) ).
tcf(c_5158,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_4894]) ).
tcf(c_5171,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,constr_tuple_2_get_1_bitstring(X0)))
| ~ pred_attacker(constr_sign(X0,name_skS)) ),
inference(superposition,[status(thm)],[c_145,c_5158]) ).
tcf(c_5179,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,X1))
| ~ pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(superposition,[status(thm)],[c_165,c_5171]) ).
tcf(c_5325,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_4909]) ).
tcf(c_5341,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(X0)),constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(X0))))
| ~ pred_attacker(constr_sign(X0,name_skS)) ),
inference(superposition,[status(thm)],[c_145,c_4806]) ).
tcf(c_5344,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4806,c_63]) ).
tcf(c_5345,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4806,c_62]) ).
tcf(c_5367,plain,
! [X0: $i,X1: $i] :
( pred_table(tuple_keys(X1,X0))
| ( X1 = name_A )
| ( X1 = name_B )
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_203,c_180]) ).
tcf(c_5422,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,constr_tuple_2_get_1_bitstring(X0)))
| ~ pred_attacker(constr_sign(X0,name_skS)) ),
inference(superposition,[status(thm)],[c_145,c_5345]) ).
tcf(c_5430,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,X1))
| ~ pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(superposition,[status(thm)],[c_165,c_5422]) ).
tcf(c_5447,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X1),constr_tuple_2_get_1_bitstring(X0)))
| ~ pred_attacker(constr_sign(X0,name_skS)) ),
inference(superposition,[status(thm)],[c_145,c_5325]) ).
tcf(c_5455,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X2),X1))
| ~ pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(superposition,[status(thm)],[c_165,c_5447]) ).
tcf(c_5463,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X1),constr_tuple_2_get_1_bitstring(X0)))
| ~ pred_attacker(constr_sign(X0,name_skS)) ),
inference(superposition,[status(thm)],[c_145,c_5344]) ).
tcf(c_5471,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X2),X1))
| ~ pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(superposition,[status(thm)],[c_165,c_5463]) ).
tcf(c_5807,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X2),X1),constr_ecb_enc_1(name_A,X1)))
| ~ pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(superposition,[status(thm)],[c_165,c_5341]) ).
tcf(c_6037,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(X2,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_ecb_enc_1(X2,constr_pkey(X1)))
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(superposition,[status(thm)],[c_64,c_4983]) ).
tcf(c_6099,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_4869,c_5060]) ).
tcf(c_6131,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6099,c_183]) ).
tcf(c_6144,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X2),X1),constr_ecb_enc_1(name_A,X1)))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6131,c_5807]) ).
tcf(c_6145,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X2),X1))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6131,c_5471]) ).
tcf(c_6146,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X2),X1))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6131,c_5455]) ).
tcf(c_6147,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,X1))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6131,c_5430]) ).
tcf(c_6148,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,X1))
| ~ pred_attacker(X0)
| ~ pred_table(tuple_keys(X0,X1)) ),
inference(superposition,[status(thm)],[c_6131,c_5179]) ).
tcf(c_6222,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,X0))
| ( X1 = name_A )
| ( X1 = name_B )
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_5367,c_6147]) ).
tcf(c_6240,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,X0))
| ( X1 = name_A )
| ( X1 = name_B )
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_5367,c_6148]) ).
tcf(c_6258,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X2),X0))
| ( X1 = name_A )
| ( X1 = name_B )
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_5367,c_6145]) ).
tcf(c_6292,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X2),X0))
| ( X1 = name_A )
| ( X1 = name_B )
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_5367,c_6146]) ).
tcf(c_6409,plain,
! [X0: $i] :
( pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X0),constr_pkey(name_skB)),constr_ecb_enc_1(name_A,constr_pkey(name_skB))))
| ~ pred_attacker(name_B) ),
inference(superposition,[status(thm)],[c_181,c_6144]) ).
tcf(c_6412,plain,
! [X0: $i] : pred_attacker(tuple_2(constr_ecb_enc_1(name_Na(X0),constr_pkey(name_skB)),constr_ecb_enc_1(name_A,constr_pkey(name_skB)))),
inference(forward_subsumption_resolution,[status(thm)],[c_6409,c_114]) ).
tcf(c_6828,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,X0))
| ( name_objective = name_A )
| ( name_objective = name_B )
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_6222]) ).
tcf(c_6869,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_A,X0))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6828,c_56,c_55]) ).
tcf(c_6880,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(X0,name_A))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_pkey(X1))
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(superposition,[status(thm)],[c_6869,c_6037]) ).
tcf(c_6995,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(X0,name_A))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6880,c_143]) ).
tcf(c_7006,plain,
! [X0: $i] :
( pred_attacker(tuple_2(name_A,name_A))
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_pkey(X0)) ),
inference(superposition,[status(thm)],[c_6869,c_6995]) ).
tcf(c_7025,plain,
! [X0: $i] :
( pred_attacker(tuple_2(name_A,name_A))
| ~ pred_attacker(X0) ),
inference(global_subsumption_just,[status(thm)],[c_7006,c_143,c_7006]) ).
tcf(c_7107,plain,
pred_attacker(tuple_2(name_A,name_A)),
inference(superposition,[status(thm)],[c_6412,c_7025]) ).
tcf(c_7271,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,X0))
| ( name_objective = name_A )
| ( name_objective = name_B )
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_6240]) ).
tcf(c_7316,plain,
! [X0: $i] :
( pred_attacker(constr_ecb_enc_1(name_B,X0))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7271,c_56,c_55]) ).
tcf(c_7328,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(X0,name_B))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_pkey(X1))
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(superposition,[status(thm)],[c_7316,c_6037]) ).
tcf(c_7898,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(X0,name_B))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7328,c_143]) ).
tcf(c_7909,plain,
! [X0: $i] :
( pred_attacker(tuple_2(name_B,name_B))
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_pkey(X0)) ),
inference(superposition,[status(thm)],[c_7316,c_7898]) ).
tcf(c_7932,plain,
! [X0: $i] :
( pred_attacker(tuple_2(name_B,name_B))
| ~ pred_attacker(X0) ),
inference(global_subsumption_just,[status(thm)],[c_7909,c_143,c_7909]) ).
tcf(c_8025,plain,
pred_attacker(tuple_2(name_B,name_B)),
inference(superposition,[status(thm)],[c_7107,c_7932]) ).
tcf(c_8487,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X1),X0))
| ( name_objective = name_A )
| ( name_objective = name_B )
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_6258]) ).
tcf(c_8542,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Na(X1),X0))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8487,c_56,c_55]) ).
tcf(c_8555,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(X0,name_Na(X2)))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_pkey(X1))
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(superposition,[status(thm)],[c_8542,c_6037]) ).
tcf(c_9015,plain,
! [X0: $i,X1: $i,X2: $i] :
( pred_attacker(tuple_2(X0,name_Na(X2)))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_ecb_enc_1(X0,constr_pkey(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8555,c_143]) ).
tcf(c_9026,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(name_B,name_Na(X1)))
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_pkey(X0)) ),
inference(superposition,[status(thm)],[c_7316,c_9015]) ).
tcf(c_9027,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(name_A,name_Na(X1)))
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_pkey(X0)) ),
inference(superposition,[status(thm)],[c_6869,c_9015]) ).
tcf(c_9340,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(name_B,name_Na(X1)))
| ~ pred_attacker(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9026,c_143,c_9026]) ).
tcf(c_9443,plain,
! [X0: $i] : pred_attacker(tuple_2(name_B,name_Na(X0))),
inference(superposition,[status(thm)],[c_8025,c_9340]) ).
tcf(c_9451,plain,
! [X0: $i,X1: $i] :
( pred_attacker(tuple_2(name_A,name_Na(X1)))
| ~ pred_attacker(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9027,c_143,c_9027]) ).
tcf(c_9559,plain,
! [X0: $i] : pred_attacker(tuple_2(name_A,name_Na(X0))),
inference(superposition,[status(thm)],[c_9443,c_9451]) ).
tcf(c_9862,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X1),X0))
| ( name_objective = name_A )
| ( name_objective = name_B )
| ~ pred_attacker(X0) ),
inference(superposition,[status(thm)],[c_4869,c_6292]) ).
tcf(c_9927,plain,
! [X0: $i,X1: $i] :
( pred_attacker(constr_ecb_enc_1(name_Nb(X1),X0))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9862,c_56,c_55]) ).
tcf(c_9942,plain,
! [X0: $i,X1: $i] :
( pred_attacker(name_Nb(X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_pkey(X0)) ),
inference(superposition,[status(thm)],[c_9927,c_4993]) ).
tcf(c_10083,plain,
! [X0: $i,X1: $i] :
( pred_attacker(name_Nb(X1))
| ~ pred_attacker(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9942,c_143,c_9942]) ).
tcf(c_10193,plain,
! [X0: $i] : pred_attacker(name_Nb(X0)),
inference(superposition,[status(thm)],[c_9559,c_10083]) ).
tcf(c_10196,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_4960,c_10193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.44 % CPULimit : 300
% 0.08/15.44 % WCLimit : 300
% 0.08/15.44 % DateTime : Thu Sep 24 23:20:27 UTC 2026
% 0.08/15.45 % CPUTime :
% 0.08/15.45 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/15.49 Running first-order theorem proving
% 0.08/15.49 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/15.50
% 0.33/15.50 % ======== iProver multi-core TPTP/SMT =========
% 0.33/15.50
% 0.33/15.50 % Detected problem language: tptp
% 0.33/15.51 % Proving...
% 4.09/16.27 % SZS status Started for theBenchmark.p
% 4.09/16.27 % SZS status Theorem for theBenchmark.p
% 4.09/16.27
% 4.09/16.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.09/16.27
% 4.09/16.27 % ------ iProver source info
% 4.09/16.27
% 4.09/16.27 % git: date: 2026-07-19 20:42:38 +0200
% 4.09/16.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.09/16.27 % git: non_committed_changes: false
% 4.09/16.27
% 4.09/16.27 % ------ Parsing...
% 4.09/16.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.09/16.27
% 4.09/16.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 4.09/16.27
% 4.09/16.27 % ------ Preprocessing... gs_s sp: 3 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.09/16.27
% 4.09/16.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.09/16.27 % ------ Proving...
% 4.09/16.27 % ------ Problem Properties
% 4.09/16.27
% 4.09/16.27 %
% 4.09/16.27 % clauses 158
% 4.09/16.27 % conjectures 1
% 4.09/16.27 % EPR 88
% 4.09/16.27 % Horn 156
% 4.09/16.27 % unary 101
% 4.09/16.27 % binary 40
% 4.09/16.27 % lits 237
% 4.09/16.27 % lits eq 91
% 4.09/16.27 % fd_pure 0
% 4.09/16.27 % fd_pseudo 0
% 4.09/16.27 % fd_cond 1
% 4.09/16.27 % fd_pseudo_cond 0
% 4.09/16.27 % AC symbols 0
% 4.09/16.27
% 4.09/16.27 % ------ Schedule dynamic 5 is on
% 4.09/16.27
% 4.09/16.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.09/16.27
% 4.09/16.27
% 4.09/16.27 % ------
% 4.09/16.27 % Current options:
% 4.09/16.27 % ------
% 4.09/16.27
% 4.09/16.27
% 4.09/16.27 %
% 4.09/16.27
% 4.09/16.27 % ------ Proving...
% 4.09/16.27 %
% 4.09/16.27
% 4.09/16.27 % SZS status Theorem for theBenchmark.p
% 4.09/16.27
% 4.09/16.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.09/16.28
% 4.09/16.28
%------------------------------------------------------------------------------