%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW960+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 : Tue Sep 29 01:38:06 PM UTC 2026
% Result : Theorem 3.08s 1.13s
% Output : Refutation 4.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 44
% Syntax : Number of formulae : 208 ( 45 unt; 14 def)
% Number of atoms : 533 ( 43 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 604 ( 279 ~; 273 |; 18 &)
% ( 14 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 15 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 9 con; 0-2 aty)
% Number of variables : 252 ( 0 sgn 251 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
constr_CONST_0x30 != name_A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f6,axiom,
constr_CONST_0x30 != name_B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f79,axiom,
! [X0,X1] : constr_adec(constr_aenc(X1,constr_pkey(X0)),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax78) ).
fof(f82,axiom,
! [X0,X1] : constr_checksign(constr_sign(X1,X0),constr_pkey(X0)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax81) ).
fof(f83,axiom,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax82) ).
fof(f87,axiom,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax86) ).
fof(f94,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(constr_pkey(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax93) ).
fof(f102,axiom,
! [X0] :
( pred_attacker(tuple_key_retrieval_server_out_2(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax101) ).
fof(f103,axiom,
! [X0,X1] :
( ( pred_attacker(X0)
& pred_attacker(X1) )
=> pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax102) ).
fof(f105,axiom,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
=> pred_attacker(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax104) ).
fof(f106,axiom,
! [X0,X1] :
( ( pred_attacker(X0)
& pred_attacker(X1) )
=> pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax105) ).
fof(f114,axiom,
! [X0] :
( pred_attacker(tuple_client_B_out_6(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax113) ).
fof(f116,axiom,
! [X0] :
( pred_attacker(tuple_client_B_out_4(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax115) ).
fof(f120,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_5(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax119) ).
fof(f122,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax121) ).
fof(f124,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_B_in_2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax123) ).
fof(f127,axiom,
! [X0] :
( pred_attacker(tuple_client_A_out_5(X0))
=> pred_attacker(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax126) ).
fof(f133,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_A_in_4(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax132) ).
fof(f135,axiom,
! [X0] :
( pred_attacker(X0)
=> pred_attacker(tuple_client_A_in_2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax134) ).
fof(f139,axiom,
! [X0,X1] :
( ( pred_attacker(X0)
& pred_attacker(X1) )
=> pred_attacker(constr_adec(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax138) ).
fof(f144,axiom,
pred_attacker(constr_CONST_0x30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax143) ).
fof(f145,axiom,
! [X0,X1] :
( ( pred_attacker(X0)
& pred_attacker(X1) )
=> pred_attacker(tuple_2(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax144) ).
fof(f153,axiom,
pred_attacker(name_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax152) ).
fof(f156,axiom,
pred_table(tuple_keys(name_A,constr_pkey(name_skA))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax155) ).
fof(f163,axiom,
! [X0,X1,X2] :
( ( pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_2_get_0x30(constr_adec(X1,name_skA)))
& pred_attacker(tuple_client_A_in_4(X1))
& pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
& pred_attacker(tuple_client_A_in_2(X2)) )
=> pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax162) ).
fof(f165,axiom,
! [X0,X1,X2] :
( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
& pred_attacker(tuple_client_B_in_3(X1))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_2(X2)) )
=> pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax164) ).
fof(f166,axiom,
! [X0,X1,X2,X3] :
( ( pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
& pred_attacker(tuple_client_B_in_5(X2))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
& pred_attacker(tuple_client_B_in_3(X1))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_2(X3)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax165) ).
fof(f167,axiom,
! [X0,X1,X2] :
( ( pred_table(tuple_keys(X0,X1))
& pred_attacker(tuple_key_retrieval_server_in_1(X2,X0)) )
=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax166) ).
fof(f168,axiom,
! [X0,X1] :
( ( X0 != name_B
& X0 != name_A
& pred_attacker(tuple_key_register_server_in_1(X0,X1)) )
=> pred_table(tuple_keys(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax167) ).
fof(f169,conjecture,
! [X0] : pred_attacker(tuple_2(name_Nb(X0),name_objective)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co0) ).
fof(f170,negated_conjecture,
~ ! [X0] : pred_attacker(tuple_2(name_Nb(X0),name_objective)),
inference(negated_conjecture,[status(cth)],[f169]) ).
fof(f178,plain,
! [X0] :
( pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f186,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_key_retrieval_server_out_2(X0)) ),
inference(ennf_transformation,[],[f102]) ).
fof(f187,plain,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(ennf_transformation,[],[f103]) ).
fof(f188,plain,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(flattening,[],[f187]) ).
fof(f190,plain,
! [X0,X1] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1)) ),
inference(ennf_transformation,[],[f105]) ).
fof(f191,plain,
! [X0,X1] :
( pred_attacker(tuple_key_register_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(ennf_transformation,[],[f106]) ).
fof(f192,plain,
! [X0,X1] :
( pred_attacker(tuple_key_register_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(flattening,[],[f191]) ).
fof(f201,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_6(X0)) ),
inference(ennf_transformation,[],[f114]) ).
fof(f203,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_4(X0)) ),
inference(ennf_transformation,[],[f116]) ).
fof(f208,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f120]) ).
fof(f210,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f212,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f124]) ).
fof(f215,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_out_5(X0)) ),
inference(ennf_transformation,[],[f127]) ).
fof(f222,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f133]) ).
fof(f224,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(ennf_transformation,[],[f135]) ).
fof(f230,plain,
! [X0,X1] :
( pred_attacker(constr_adec(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(ennf_transformation,[],[f139]) ).
fof(f231,plain,
! [X0,X1] :
( pred_attacker(constr_adec(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(flattening,[],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(ennf_transformation,[],[f145]) ).
fof(f233,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(flattening,[],[f232]) ).
fof(f242,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_2_get_0x30(constr_adec(X1,name_skA)))
| ~ pred_attacker(tuple_client_A_in_4(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_A_in_2(X2)) ),
inference(ennf_transformation,[],[f163]) ).
fof(f243,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_2_get_0x30(constr_adec(X1,name_skA)))
| ~ pred_attacker(tuple_client_A_in_4(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_A_in_2(X2)) ),
inference(flattening,[],[f242]) ).
fof(f244,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X2)) ),
inference(ennf_transformation,[],[f165]) ).
fof(f245,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X2)) ),
inference(flattening,[],[f244]) ).
fof(f246,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X3)) ),
inference(ennf_transformation,[],[f166]) ).
fof(f247,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X3)) ),
inference(flattening,[],[f246]) ).
fof(f248,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_table(tuple_keys(X0,X1))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0)) ),
inference(ennf_transformation,[],[f167]) ).
fof(f249,plain,
! [X0,X1,X2] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_table(tuple_keys(X0,X1))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0)) ),
inference(flattening,[],[f248]) ).
fof(f250,plain,
! [X0,X1] :
( pred_table(tuple_keys(X0,X1))
| name_B = X0
| name_A = X0
| ~ pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(ennf_transformation,[],[f168]) ).
fof(f251,plain,
! [X0,X1] :
( pred_table(tuple_keys(X0,X1))
| name_B = X0
| name_A = X0
| ~ pred_attacker(tuple_key_register_server_in_1(X0,X1)) ),
inference(flattening,[],[f250]) ).
fof(f252,plain,
? [X0] : ~ pred_attacker(tuple_2(name_Nb(X0),name_objective)),
inference(ennf_transformation,[],[f170]) ).
fof(f253,plain,
~ pred_attacker(tuple_2(name_Nb(sK0),name_objective)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f252]) ).
fof(f258,plain,
constr_CONST_0x30 != name_A,
inference(cnf_transformation,[],[f5]) ).
fof(f259,plain,
constr_CONST_0x30 != name_B,
inference(cnf_transformation,[],[f6]) ).
fof(f332,plain,
! [X0,X1] : constr_adec(constr_aenc(X1,constr_pkey(X0)),X0) = X1,
inference(cnf_transformation,[],[f79]) ).
fof(f335,plain,
! [X0,X1] : constr_checksign(constr_sign(X1,X0),constr_pkey(X0)) = X1,
inference(cnf_transformation,[],[f82]) ).
fof(f336,plain,
! [X0,X1] : constr_tuple_2_get_1_bitstring(tuple_2(X0,X1)) = X1,
inference(cnf_transformation,[],[f83]) ).
fof(f340,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[],[f87]) ).
fof(f347,plain,
! [X0] :
( pred_attacker(constr_pkey(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f178]) ).
fof(f355,plain,
! [X0] :
( ~ pred_attacker(tuple_key_retrieval_server_out_2(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f186]) ).
fof(f356,plain,
! [X0,X1] :
( pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(cnf_transformation,[],[f188]) ).
fof(f358,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,X1))
| pred_attacker(X1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f359,plain,
! [X0,X1] :
( pred_attacker(tuple_key_register_server_in_1(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(cnf_transformation,[],[f192]) ).
fof(f367,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_6(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f369,plain,
! [X0] :
( ~ pred_attacker(tuple_client_B_out_4(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f373,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f375,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f377,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f212]) ).
fof(f380,plain,
! [X0] :
( ~ pred_attacker(tuple_client_A_out_5(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[],[f215]) ).
fof(f386,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_4(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f388,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[],[f224]) ).
fof(f392,plain,
! [X0,X1] :
( pred_attacker(constr_adec(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(cnf_transformation,[],[f231]) ).
fof(f397,plain,
pred_attacker(constr_CONST_0x30),
inference(cnf_transformation,[],[f144]) ).
fof(f398,plain,
! [X0,X1] :
( pred_attacker(tuple_2(X0,X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(cnf_transformation,[],[f233]) ).
fof(f406,plain,
pred_attacker(name_A),
inference(cnf_transformation,[],[f153]) ).
fof(f408,plain,
pred_table(tuple_keys(name_A,constr_pkey(name_skA))),
inference(cnf_transformation,[],[f156]) ).
fof(f415,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_2_get_0x30(constr_adec(X1,name_skA)))
| ~ pred_attacker(tuple_client_A_in_4(X1))
| ~ pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_A_in_2(X2)) ),
inference(cnf_transformation,[],[f243]) ).
fof(f417,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X2,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X2)) ),
inference(cnf_transformation,[],[f245]) ).
fof(f418,plain,
! [X2,X3,X0,X1] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
| ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_2(X3)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f419,plain,
! [X2,X0,X1] :
( ~ pred_table(tuple_keys(X0,X1))
| pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X0,X1),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0)) ),
inference(cnf_transformation,[],[f249]) ).
fof(f420,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_key_register_server_in_1(X0,X1))
| name_B = X0
| name_A = X0
| pred_table(tuple_keys(X0,X1)) ),
inference(cnf_transformation,[],[f251]) ).
fof(f421,plain,
~ pred_attacker(tuple_2(name_Nb(sK0),name_objective)),
inference(cnf_transformation,[],[f253]) ).
fof(f423,definition,
( spl1_1
<=> ! [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_2(X3)) ) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f424,plain,
( ! [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_2(X3)) )
| ~ spl1_1 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f426,definition,
( spl1_2
<=> ! [X1] :
( ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f427,plain,
( ! [X1] :
( ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB))) )
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f429,definition,
( spl1_3
<=> ! [X2,X0] :
( ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
| ~ pred_attacker(tuple_client_B_in_5(X2)) ) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f430,plain,
( ! [X2,X0] :
( ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB))
| ~ pred_attacker(tuple_client_B_in_5(X2)) )
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f432,definition,
( spl1_4
<=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f434,plain,
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,plain,
( spl1_1
| spl1_2
| spl1_3
| spl1_4 ),
inference(avatar_split_clause,[],[f418,f432,f429,f426,f423]) ).
fof(f436,plain,
( ~ pred_attacker(name_Nb(sK0))
| ~ pred_attacker(name_objective) ),
inference(resolution,[],[f398,f421]) ).
fof(f440,definition,
( spl1_5
<=> pred_attacker(name_objective) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f444,definition,
( spl1_6
<=> pred_attacker(name_Nb(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
fof(f446,plain,
( ~ pred_attacker(name_Nb(sK0))
| spl1_6 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f447,plain,
( ~ spl1_5
| ~ spl1_6 ),
inference(avatar_split_clause,[],[f436,f444,f440]) ).
fof(f456,plain,
( ! [X0] :
( ~ pred_attacker(X0)
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) )
| ~ spl1_2 ),
inference(resolution,[],[f375,f427]) ).
fof(f457,plain,
( ! [X0] : ~ pred_attacker(X0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f456,f340]) ).
fof(f459,plain,
( $false
| ~ spl1_2 ),
inference(resolution,[],[f457,f397]) ).
fof(f503,plain,
~ spl1_2,
inference(avatar_contradiction_clause,[],[f459]) ).
fof(f504,plain,
( ! [X2] : ~ pred_attacker(tuple_client_B_in_5(X2))
| ~ spl1_3 ),
inference(forward_subsumption_resolution,[],[f430,f340]) ).
fof(f505,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_attacker(tuple_client_B_in_2(X2)) ),
inference(forward_subsumption_resolution,[],[f417,f340]) ).
fof(f506,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_client_B_in_2(X2))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X0)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS)))))) ),
inference(forward_subsumption_resolution,[],[f505,f340]) ).
fof(f507,plain,
( ! [X0] : ~ pred_attacker(X0)
| ~ spl1_3 ),
inference(resolution,[],[f504,f373]) ).
fof(f508,plain,
( $false
| ~ spl1_3 ),
inference(resolution,[],[f507,f397]) ).
fof(f552,plain,
~ spl1_3,
inference(avatar_contradiction_clause,[],[f508]) ).
fof(f553,plain,
( pred_attacker(name_objective)
| ~ spl1_4 ),
inference(resolution,[],[f434,f367]) ).
fof(f556,plain,
( ! [X3] : ~ pred_attacker(tuple_client_B_in_2(X3))
| ~ spl1_1 ),
inference(forward_subsumption_resolution,[],[f424,f340]) ).
fof(f558,plain,
( ! [X0] : ~ pred_attacker(X0)
| ~ spl1_1 ),
inference(forward_subsumption_resolution,[],[f377,f556]) ).
fof(f559,plain,
( $false
| ~ spl1_1 ),
inference(resolution,[],[f558,f397]) ).
fof(f603,plain,
~ spl1_1,
inference(avatar_contradiction_clause,[],[f559]) ).
fof(f604,plain,
( spl1_5
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f553,f432,f440]) ).
fof(f606,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))) ),
inference(resolution,[],[f377,f506]) ).
fof(f612,plain,
! [X0] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(name_A,constr_pkey(name_skA)),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,name_A)) ),
inference(resolution,[],[f408,f419]) ).
fof(f614,definition,
( spl1_7
<=> ! [X0] : ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,name_A)) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f615,plain,
( ! [X0] : ~ pred_attacker(tuple_key_retrieval_server_in_1(X0,name_A))
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f617,definition,
( spl1_8
<=> pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(name_A,constr_pkey(name_skA)),name_skS))) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f619,plain,
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(name_A,constr_pkey(name_skA)),name_skS)))
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f620,plain,
( spl1_7
| spl1_8 ),
inference(avatar_split_clause,[],[f612,f617,f614]) ).
fof(f697,plain,
! [X0,X1] :
( ~ pred_attacker(constr_aenc(X0,constr_pkey(X1)))
| pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(superposition,[],[f392,f332]) ).
fof(f700,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_eq_bitstring_bitstring(name_Na(X0),constr_tuple_2_get_0x30(constr_adec(X1,name_skA)))
| ~ pred_attacker(tuple_client_A_in_4(X1))
| ~ pred_attacker(tuple_client_A_in_2(X2)) ),
inference(forward_subsumption_resolution,[],[f415,f340]) ).
fof(f701,plain,
! [X2,X1] :
( ~ pred_attacker(tuple_client_A_in_4(X1))
| pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X1,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_attacker(tuple_client_A_in_2(X2)) ),
inference(forward_subsumption_resolution,[],[f700,f340]) ).
fof(f704,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X0,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ pred_attacker(X0) ),
inference(resolution,[],[f386,f701]) ).
fof(f713,plain,
! [X0,X1] :
( pred_table(tuple_keys(X0,X1))
| ~ pred_attacker(X1)
| name_B = X0
| name_A = X0
| ~ pred_attacker(X0) ),
inference(resolution,[],[f359,f420]) ).
fof(f720,plain,
( pred_attacker(constr_sign(tuple_2(name_A,constr_pkey(name_skA)),name_skS))
| ~ spl1_8 ),
inference(resolution,[],[f619,f355]) ).
fof(f731,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS))))))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(resolution,[],[f606,f375]) ).
fof(f740,plain,
! [X2,X0,X1] :
( ~ pred_attacker(X0)
| name_B = X1
| name_A = X1
| ~ pred_attacker(X1)
| pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X1,X0),name_skS)))
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X1)) ),
inference(resolution,[],[f713,f419]) ).
fof(f741,plain,
! [X2,X0,X1] :
( pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(X1,X0),name_skS)))
| name_B = X1
| name_A = X1
| ~ pred_attacker(X0)
| ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X1)) ),
inference(forward_subsumption_resolution,[],[f740,f358]) ).
fof(f742,plain,
! [X0,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(X0,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ pred_attacker(X0)
| ~ pred_attacker(X1) ),
inference(resolution,[],[f704,f388]) ).
fof(f749,definition,
( spl1_12
<=> ! [X0,X1] :
( ~ pred_attacker(constr_sign(tuple_2(X0,constr_pkey(X1)),name_skS))
| ~ pred_attacker(X1) ) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
fof(f750,plain,
( ! [X0,X1] :
( ~ pred_attacker(constr_sign(tuple_2(X0,constr_pkey(X1)),name_skS))
| ~ pred_attacker(X1) )
| ~ spl1_12 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f754,plain,
! [X2,X0,X1] :
( ~ pred_attacker(constr_sign(X0,name_skS))
| pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X1,name_skB)),name_Nb(X2)),constr_tuple_2_get_1_bitstring(X0))))
| ~ pred_attacker(X1) ),
inference(superposition,[],[f731,f335]) ).
fof(f760,plain,
! [X0,X1] :
( ~ pred_attacker(constr_aenc(X0,constr_pkey(name_skA)))
| pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(X0),constr_tuple_2_get_1_bitstring(constr_checksign(X1,constr_pkey(name_skS))))))
| ~ pred_attacker(X1) ),
inference(superposition,[],[f742,f332]) ).
fof(f787,plain,
! [X2,X0,X1] :
( ~ pred_attacker(tuple_key_retrieval_server_in_1(X2,X0))
| name_A = X0
| ~ pred_attacker(X1)
| name_B = X0
| pred_attacker(constr_sign(tuple_2(X0,X1),name_skS)) ),
inference(resolution,[],[f741,f355]) ).
fof(f845,plain,
( ! [X0] :
( ~ pred_attacker(X0)
| ~ pred_attacker(name_A) )
| ~ spl1_7 ),
inference(resolution,[],[f615,f356]) ).
fof(f846,plain,
( ! [X0] : ~ pred_attacker(X0)
| ~ spl1_7 ),
inference(forward_subsumption_resolution,[],[f845,f406]) ).
fof(f847,plain,
( $false
| ~ spl1_7 ),
inference(resolution,[],[f846,f397]) ).
fof(f948,plain,
~ spl1_7,
inference(avatar_contradiction_clause,[],[f847]) ).
fof(f953,plain,
( ! [X0,X1] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1)),constr_tuple_2_get_1_bitstring(tuple_2(name_A,constr_pkey(name_skA))))))
| ~ pred_attacker(X0) )
| ~ spl1_8 ),
inference(resolution,[],[f720,f754]) ).
fof(f955,plain,
( ! [X0,X1] :
( pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1)),constr_pkey(name_skA))))
| ~ pred_attacker(X0) )
| ~ spl1_8 ),
inference(forward_demodulation,[],[f953,f336]) ).
fof(f957,plain,
( ! [X0,X1] :
( pred_attacker(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1)),constr_pkey(name_skA)))
| ~ pred_attacker(X0) )
| ~ spl1_8 ),
inference(resolution,[],[f955,f369]) ).
fof(f984,plain,
! [X2,X0,X1] :
( name_A = X0
| ~ pred_attacker(X1)
| name_B = X0
| pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))
| ~ pred_attacker(X2)
| ~ pred_attacker(X0) ),
inference(resolution,[],[f787,f356]) ).
fof(f987,definition,
( spl1_23
<=> ! [X2] : ~ pred_attacker(X2) ),
introduced(definition,[new_symbols(definition,[spl1_23])],[avatar_definition]) ).
fof(f988,plain,
( ! [X2] : ~ pred_attacker(X2)
| ~ spl1_23 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f990,definition,
( spl1_24
<=> ! [X0,X1] :
( name_A = X0
| ~ pred_attacker(X0)
| pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))
| name_B = X0
| ~ pred_attacker(X1) ) ),
introduced(definition,[new_symbols(definition,[spl1_24])],[avatar_definition]) ).
fof(f991,plain,
( ! [X0,X1] :
( pred_attacker(constr_sign(tuple_2(X0,X1),name_skS))
| ~ pred_attacker(X0)
| name_A = X0
| name_B = X0
| ~ pred_attacker(X1) )
| ~ spl1_24 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f992,plain,
( spl1_23
| spl1_24 ),
inference(avatar_split_clause,[],[f984,f990,f987]) ).
fof(f993,plain,
( $false
| ~ spl1_23 ),
inference(resolution,[],[f988,f397]) ).
fof(f1110,plain,
~ spl1_23,
inference(avatar_contradiction_clause,[],[f993]) ).
fof(f1130,plain,
( ! [X2,X0,X1] :
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(X0,name_skB)),name_Nb(X1))),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_attacker(X2) )
| ~ spl1_8 ),
inference(resolution,[],[f957,f760]) ).
fof(f1133,plain,
( ! [X2,X0,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(name_Nb(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_attacker(X0)
| ~ pred_attacker(X2) )
| ~ spl1_8 ),
inference(forward_demodulation,[],[f1130,f336]) ).
fof(f1135,definition,
( spl1_27
<=> ! [X2,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(name_Nb(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_attacker(X2) ) ),
introduced(definition,[new_symbols(definition,[spl1_27])],[avatar_definition]) ).
fof(f1136,plain,
( ! [X2,X1] :
( pred_attacker(tuple_client_A_out_5(constr_aenc(name_Nb(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X2,constr_pkey(name_skS))))))
| ~ pred_attacker(X2) )
| ~ spl1_27 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1137,plain,
( spl1_23
| spl1_27
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f1133,f617,f1135,f987]) ).
fof(f1159,plain,
( ! [X0,X1] :
( pred_attacker(constr_aenc(name_Nb(X1),constr_tuple_2_get_1_bitstring(constr_checksign(X0,constr_pkey(name_skS)))))
| ~ pred_attacker(X0) )
| ~ spl1_27 ),
inference(resolution,[],[f1136,f380]) ).
fof(f1163,plain,
( ! [X0,X1] :
( pred_attacker(constr_aenc(name_Nb(X1),constr_tuple_2_get_1_bitstring(X0)))
| ~ pred_attacker(constr_sign(X0,name_skS)) )
| ~ spl1_27 ),
inference(superposition,[],[f1159,f335]) ).
fof(f1166,plain,
( ! [X2,X0,X1] :
( pred_attacker(constr_aenc(name_Nb(X1),X0))
| ~ pred_attacker(constr_sign(tuple_2(X2,X0),name_skS)) )
| ~ spl1_27 ),
inference(superposition,[],[f1163,f336]) ).
fof(f1173,plain,
( ! [X2,X0,X1] :
( ~ pred_attacker(constr_sign(tuple_2(X0,constr_pkey(X1)),name_skS))
| pred_attacker(name_Nb(X2))
| ~ pred_attacker(X1) )
| ~ spl1_27 ),
inference(resolution,[],[f1166,f697]) ).
fof(f1185,definition,
( spl1_30
<=> ! [X2] : pred_attacker(name_Nb(X2)) ),
introduced(definition,[new_symbols(definition,[spl1_30])],[avatar_definition]) ).
fof(f1186,plain,
( ! [X2] : pred_attacker(name_Nb(X2))
| ~ spl1_30 ),
inference(avatar_component_clause,[],[f1185]) ).
fof(f1187,plain,
( spl1_30
| spl1_12
| ~ spl1_27 ),
inference(avatar_split_clause,[],[f1173,f1135,f749,f1185]) ).
fof(f1201,plain,
( ! [X0,X1] :
( ~ pred_attacker(X0)
| name_A = X0
| name_B = X0
| ~ pred_attacker(constr_pkey(X1))
| ~ pred_attacker(X1) )
| ~ spl1_12
| ~ spl1_24 ),
inference(resolution,[],[f991,f750]) ).
fof(f1209,plain,
( ! [X0,X1] :
( ~ pred_attacker(X0)
| name_A = X0
| name_B = X0
| ~ pred_attacker(X1) )
| ~ spl1_12
| ~ spl1_24 ),
inference(forward_subsumption_resolution,[],[f1201,f347]) ).
fof(f1211,definition,
( spl1_31
<=> ! [X0] :
( ~ pred_attacker(X0)
| name_B = X0
| name_A = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1_31])],[avatar_definition]) ).
fof(f1212,plain,
( ! [X0] :
( ~ pred_attacker(X0)
| name_B = X0
| name_A = X0 )
| ~ spl1_31 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1225,plain,
( spl1_23
| spl1_31
| ~ spl1_12
| ~ spl1_24 ),
inference(avatar_split_clause,[],[f1209,f990,f749,f1211,f987]) ).
fof(f1226,plain,
( constr_CONST_0x30 = name_B
| constr_CONST_0x30 = name_A
| ~ spl1_31 ),
inference(resolution,[],[f1212,f397]) ).
fof(f1502,plain,
( constr_CONST_0x30 = name_A
| ~ spl1_31 ),
inference(forward_subsumption_resolution,[],[f1226,f259]) ).
fof(f1517,plain,
( $false
| ~ spl1_31 ),
inference(forward_subsumption_resolution,[],[f1502,f258]) ).
fof(f1518,plain,
~ spl1_31,
inference(avatar_contradiction_clause,[],[f1517]) ).
fof(f1520,plain,
( $false
| spl1_6
| ~ spl1_30 ),
inference(resolution,[],[f1186,f446]) ).
fof(f1521,plain,
( spl1_6
| ~ spl1_30 ),
inference(avatar_contradiction_clause,[],[f1520]) ).
cnf(s1,plain,
( spl1_1
| spl1_2
| spl1_3
| spl1_4 ),
inference(sat_conversion,[],[f435]) ).
cnf(s2,plain,
( ~ spl1_5
| ~ spl1_6 ),
inference(sat_conversion,[],[f447]) ).
cnf(s19,plain,
~ spl1_2,
inference(sat_conversion,[],[f503]) ).
cnf(s36,plain,
~ spl1_3,
inference(sat_conversion,[],[f552]) ).
cnf(s54,plain,
~ spl1_1,
inference(sat_conversion,[],[f603]) ).
cnf(s55,plain,
( ~ spl1_4
| spl1_5 ),
inference(sat_conversion,[],[f604]) ).
cnf(s57,plain,
( spl1_7
| spl1_8 ),
inference(sat_conversion,[],[f620]) ).
cnf(s112,plain,
~ spl1_7,
inference(sat_conversion,[],[f948]) ).
cnf(s115,plain,
( spl1_23
| spl1_24 ),
inference(sat_conversion,[],[f992]) ).
cnf(s145,plain,
~ spl1_23,
inference(sat_conversion,[],[f1110]) ).
cnf(s147,plain,
( ~ spl1_8
| spl1_23
| spl1_27 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s150,plain,
( spl1_12
| ~ spl1_27
| spl1_30 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s154,plain,
( ~ spl1_12
| spl1_23
| ~ spl1_24
| spl1_31 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s179,plain,
~ spl1_31,
inference(sat_conversion,[],[f1518]) ).
cnf(s180,plain,
( spl1_6
| ~ spl1_30 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s181,plain,
( ~ spl1_12
| spl1_23
| ~ spl1_24 ),
inference(rat,[],[s154,s179]) ).
cnf(s185,plain,
spl1_24,
inference(rat,[],[s115,s145]) ).
cnf(s189,plain,
~ spl1_12,
inference(rat,[],[s181,s145,s185]) ).
cnf(s194,plain,
spl1_8,
inference(rat,[],[s57,s112]) ).
cnf(s195,plain,
spl1_27,
inference(rat,[],[s147,s145,s194]) ).
cnf(s197,plain,
spl1_30,
inference(rat,[],[s150,s189,s195]) ).
cnf(s201,plain,
spl1_6,
inference(rat,[],[s180,s197]) ).
cnf(s204,plain,
~ spl1_5,
inference(rat,[],[s2,s201]) ).
cnf(s205,plain,
~ spl1_4,
inference(rat,[],[s55,s204]) ).
cnf(s206,plain,
$false,
inference(rat,[],[s1,s205,s36,s19,s54]) ).
fof(f1522,plain,
$false,
inference(avatar_sat_refutation,[],[s206]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW960+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n014.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 14:49:00 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.08/1.13 % (1824986)Detected formulas, will run a generic FOF schedule.
% 3.08/1.13 % (1825071)dis-21_1_sil=8000:lcm=predicate:random_seed=1717222005:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.08/1.13 % (1825071)Refutation not found, incomplete strategy
% 3.08/1.13 % (1825071)------------------------------
% 3.08/1.13 % (1825071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.13 % (1825071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.13 % (1825071)CaDiCaL version: 2.1.3
% 3.08/1.13 % (1825071)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.13 % (1825071)Time elapsed: 0.005 s
% 3.08/1.13 % (1825071)Peak memory usage: 88 MB
% 3.08/1.13 % (1825071)Instructions burned: 14 (million)
% 3.08/1.13 % (1825067)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1711591139:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.08/1.13 % (1825069)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=40472140:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.08/1.13 % (1825070)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=586372994:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.08/1.13 % (1825066)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2674580011:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.08/1.13 % (1825068)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2421028115:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.08/1.13 % (1825065)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=713210540:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.08/1.13 % (1825068)Refutation not found, incomplete strategy
% 3.08/1.13 % (1825068)------------------------------
% 3.08/1.13 % (1825068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.13 % (1825068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.13 % (1825068)CaDiCaL version: 2.1.3
% 3.08/1.13 % (1825068)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.13 % (1825068)Time elapsed: 0.002 s
% 3.08/1.13 % (1825068)Peak memory usage: 88 MB
% 3.08/1.13 % (1825068)Instructions burned: 1 (million)
% 3.08/1.13 % (1825069)Refutation not found, incomplete strategy
% 3.08/1.13 % (1825069)------------------------------
% 3.08/1.13 % (1825069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.13 % (1825069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.13 % (1825069)CaDiCaL version: 2.1.3
% 3.08/1.13 % (1825069)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.13 % (1825069)Time elapsed: 0.004 s
% 3.08/1.13 % (1825069)Peak memory usage: 88 MB
% 3.08/1.13 % (1825069)Instructions burned: 5 (million)
% 3.08/1.13 % (1825070)First to succeed.
% 3.08/1.13 % (1825070)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1824986"
% 3.08/1.13 % (1825071)------------------------------
% 3.08/1.13 % (1825071)------------------------------
% 3.08/1.13 % (1825079)lrs+10_1_sil=8000:sp=occurrence:random_seed=2816871024:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.08/1.13 % (1825079)Refutation not found, incomplete strategy
% 3.08/1.13 % (1825079)------------------------------
% 3.08/1.13 % (1825079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.13 % (1825079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.13 % (1825079)CaDiCaL version: 2.1.3
% 3.08/1.13 % (1825079)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.13 % (1825079)Time elapsed: 0.005 s
% 3.08/1.13 % (1825079)Peak memory usage: 88 MB
% 3.08/1.13 % (1825079)Instructions burned: 12 (million)
% 3.08/1.13 % (1825068)------------------------------
% 3.08/1.13 % (1825068)------------------------------
% 3.08/1.13 % (1825069)------------------------------
% 3.08/1.13 % (1825069)------------------------------
% 3.08/1.13 % (1825070)Refutation found. Thanks to Tanya!
% 3.08/1.13 % SZS status Theorem for theBenchmark
% 3.08/1.13 % SZS output start Proof for theBenchmark
% See solution above
% 4.00/1.33 % (1825070)------------------------------
% 4.00/1.33 % (1825070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.33 % (1825070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.33 % (1825070)CaDiCaL version: 2.1.3
% 4.00/1.33 % (1825070)Termination reason: Refutation
% 4.00/1.33 % (1825070)Time elapsed: 0.032 s
% 4.00/1.33 % (1825070)Peak memory usage: 90 MB
% 4.00/1.33 % (1825070)Instructions burned: 45 (million)
% 4.00/1.33 % (1825070)------------------------------
% 4.00/1.33 % (1825070)------------------------------
% 4.00/1.33 % (1824986)Success in time 0.476 s
% 4.00/1.33 % Vampire exiting
%------------------------------------------------------------------------------