%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV014-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:49:56 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV014-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 08:24:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 0.08/0.43 % Refutation found
% 0.08/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.43 fof(f1,axiom,(
% 0.08/0.43 party_of_protocol(a) ),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f2,axiom,(
% 0.08/0.43 message(sent(a,b,pair(a,an_a_nonce))) ),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f5,axiom,(
% 0.08/0.43 party_of_protocol(b) ),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f6,axiom,(
% 0.08/0.43 fresh_to_b(an_a_nonce) ),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f7,axiom,(
% 0.08/0.43 (![B,A]: (( message(sent(b,t,triple(b,generate_b_nonce(B),encrypt(triple(A,B,generate_expiration_time(B)),bt))))| ~ fresh_to_b(B)| ~ message(sent(A,b,pair(A,B))) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f8,axiom,(
% 0.08/0.43 (![A,B]: (( b_stored(pair(A,B))| ~ fresh_to_b(B)| ~ message(sent(A,b,pair(A,B))) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f9,axiom,(
% 0.08/0.43 (![B,A,C]: (( b_holds(key(B,A))| ~ b_stored(pair(A,C))| ~ message(sent(A,b,pair(encrypt(triple(A,B,generate_expiration_time(C)),bt),encrypt(generate_b_nonce(C),B)))) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f12,axiom,(
% 0.08/0.43 party_of_protocol(t) ),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f14,axiom,(
% 0.08/0.43 (![C,A,B]: (( intruder_message(C)| ~ message(sent(A,B,C)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f15,axiom,(
% 0.08/0.43 (![A,B]: (( intruder_message(A)| ~ intruder_message(pair(A,B)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f16,axiom,(
% 0.08/0.43 (![B,A]: (( intruder_message(B)| ~ intruder_message(pair(A,B)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f18,axiom,(
% 0.08/0.43 (![B,A,C]: (( intruder_message(B)| ~ intruder_message(triple(A,B,C)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f19,axiom,(
% 0.08/0.43 (![C,A,B]: (( intruder_message(C)| ~ intruder_message(triple(A,B,C)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f24,axiom,(
% 0.08/0.43 (![A,B]: (( intruder_message(pair(A,B))| ~ intruder_message(B)| ~ intruder_message(A) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f28,axiom,(
% 0.08/0.43 (![B,C,A]: (( message(sent(B,C,A))| ~ intruder_message(A)| ~ party_of_protocol(C)| ~ party_of_protocol(B) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f29,axiom,(
% 0.08/0.43 (![A,B]: (( intruder_holds(key(A,B))| ~ intruder_message(A)| ~ party_of_protocol(B) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f30,axiom,(
% 0.08/0.43 (![A,B,C]: (( intruder_message(encrypt(A,B))| ~ intruder_holds(key(B,C))| ~ intruder_message(A)| ~ party_of_protocol(C) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f34,negated_conjecture,(
% 0.08/0.43 (![A]: (( ~ b_holds(key(A,a))| ~ intruder_holds(key(A,b)) ) ))),
% 0.08/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.43 fof(f35,plain,(
% 0.08/0.43 party_of_protocol(a)),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.43 fof(f36,plain,(
% 0.08/0.43 message(sent(a,b,pair(a,an_a_nonce)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.43 fof(f40,plain,(
% 0.08/0.43 party_of_protocol(b)),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f5])).
% 0.08/0.43 fof(f41,plain,(
% 0.08/0.43 fresh_to_b(an_a_nonce)),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.43 fof(f42,plain,(
% 0.08/0.43 ![X0,X1]: (message(sent(b,t,triple(b,generate_b_nonce(X0),encrypt(triple(X1,X0,generate_expiration_time(X0)),bt))))|~fresh_to_b(X0)|~message(sent(X1,b,pair(X1,X0))))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f7])).
% 0.08/0.43 fof(f43,plain,(
% 0.08/0.43 ![X0,X1]: (b_stored(pair(X0,X1))|~fresh_to_b(X1)|~message(sent(X0,b,pair(X0,X1))))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f8])).
% 0.08/0.43 fof(f44,plain,(
% 0.08/0.43 ![X0,X1,X2]: (b_holds(key(X0,X1))|~b_stored(pair(X1,X2))|~message(sent(X1,b,pair(encrypt(triple(X1,X0,generate_expiration_time(X2)),bt),encrypt(generate_b_nonce(X2),X0)))))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f9])).
% 0.08/0.43 fof(f47,plain,(
% 0.08/0.43 party_of_protocol(t)),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.43 fof(f50,plain,(
% 0.08/0.43 ![C]: (intruder_message(C)|(![A,B]: ~message(sent(A,B,C))))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f14])).
% 0.08/0.43 fof(f51,plain,(
% 0.08/0.43 ![X0,X1,X2]: (intruder_message(X0)|~message(sent(X1,X2,X0)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f50])).
% 0.08/0.43 fof(f52,plain,(
% 0.08/0.43 ![A]: (intruder_message(A)|(![B]: ~intruder_message(pair(A,B))))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f15])).
% 0.08/0.43 fof(f53,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_message(X0)|~intruder_message(pair(X0,X1)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f52])).
% 0.08/0.43 fof(f54,plain,(
% 0.08/0.43 ![B]: (intruder_message(B)|(![A]: ~intruder_message(pair(A,B))))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f16])).
% 0.08/0.43 fof(f55,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_message(X0)|~intruder_message(pair(X1,X0)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f54])).
% 0.08/0.43 fof(f58,plain,(
% 0.08/0.43 ![B]: (intruder_message(B)|(![A,C]: ~intruder_message(triple(A,B,C))))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f18])).
% 0.08/0.43 fof(f59,plain,(
% 0.08/0.43 ![X0,X1,X2]: (intruder_message(X0)|~intruder_message(triple(X1,X0,X2)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f58])).
% 0.08/0.43 fof(f60,plain,(
% 0.08/0.43 ![C]: (intruder_message(C)|(![A,B]: ~intruder_message(triple(A,B,C))))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f19])).
% 0.08/0.43 fof(f61,plain,(
% 0.08/0.43 ![X0,X1,X2]: (intruder_message(X0)|~intruder_message(triple(X1,X2,X0)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f60])).
% 0.08/0.43 fof(f70,plain,(
% 0.08/0.43 ![A]: ((![B]: (intruder_message(pair(A,B))|~intruder_message(B)))|~intruder_message(A))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f24])).
% 0.08/0.43 fof(f71,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_message(pair(X0,X1))|~intruder_message(X1)|~intruder_message(X0))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f70])).
% 0.08/0.43 fof(f78,plain,(
% 0.08/0.43 ![B]: ((![C]: ((![A]: (message(sent(B,C,A))|~intruder_message(A)))|~party_of_protocol(C)))|~party_of_protocol(B))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f28])).
% 0.08/0.43 fof(f79,plain,(
% 0.08/0.43 ![X0,X1,X2]: (message(sent(X0,X1,X2))|~intruder_message(X2)|~party_of_protocol(X1)|~party_of_protocol(X0))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f78])).
% 0.08/0.43 fof(f80,plain,(
% 0.08/0.43 ![B]: ((![A]: (intruder_holds(key(A,B))|~intruder_message(A)))|~party_of_protocol(B))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f29])).
% 0.08/0.43 fof(f81,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_holds(key(X0,X1))|~intruder_message(X0)|~party_of_protocol(X1))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f80])).
% 0.08/0.43 fof(f82,plain,(
% 0.08/0.43 ![C]: ((![A]: ((![B]: (intruder_message(encrypt(A,B))|~intruder_holds(key(B,C))))|~intruder_message(A)))|~party_of_protocol(C))),
% 0.08/0.43 inference(miniscoping,[status(thm)],[f30])).
% 0.08/0.43 fof(f83,plain,(
% 0.08/0.43 ![X0,X1,X2]: (intruder_message(encrypt(X0,X1))|~intruder_holds(key(X1,X2))|~intruder_message(X0)|~party_of_protocol(X2))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f82])).
% 0.08/0.43 fof(f87,plain,(
% 0.08/0.43 ![X0]: (~b_holds(key(X0,a))|~intruder_holds(key(X0,b)))),
% 0.08/0.43 inference(cnf_transformation,[status(thm)],[f34])).
% 0.08/0.43 fof(f88,plain,(
% 0.08/0.43 b_stored(pair(a,an_a_nonce))|~fresh_to_b(an_a_nonce)),
% 0.08/0.43 inference(resolution,[status(thm)],[f43,f36])).
% 0.08/0.43 fof(f89,definition,(
% 0.08/0.43 sQ0_spl <=> (b_stored(pair(a,an_a_nonce)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f90,plain,(
% 0.08/0.43 b_stored(pair(a,an_a_nonce))|~sQ0_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f89])).
% 0.08/0.43 fof(f92,definition,(
% 0.08/0.43 sQ1_spl <=> (fresh_to_b(an_a_nonce))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f94,plain,(
% 0.08/0.43 ~fresh_to_b(an_a_nonce)|sQ1_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f92])).
% 0.08/0.43 fof(f95,plain,(
% 0.08/0.43 sQ0_spl|~sQ1_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f88,f89,f92])).
% 0.08/0.43 fof(f104,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_message(triple(b,generate_b_nonce(X0),encrypt(triple(X1,X0,generate_expiration_time(X0)),bt)))|~fresh_to_b(X0)|~message(sent(X1,b,pair(X1,X0))))),
% 0.08/0.43 inference(resolution,[status(thm)],[f51,f42])).
% 0.08/0.43 fof(f105,plain,(
% 0.08/0.43 intruder_message(pair(a,an_a_nonce))),
% 0.08/0.43 inference(resolution,[status(thm)],[f51,f36])).
% 0.08/0.43 fof(f106,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~message(sent(a,b,pair(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),X0))))|~sQ0_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f90,f44])).
% 0.08/0.43 fof(f107,plain,(
% 0.08/0.43 intruder_message(an_a_nonce)),
% 0.08/0.43 inference(resolution,[status(thm)],[f105,f55])).
% 0.08/0.43 fof(f108,plain,(
% 0.08/0.43 intruder_message(a)),
% 0.08/0.43 inference(resolution,[status(thm)],[f105,f53])).
% 0.08/0.43 fof(f134,plain,(
% 0.08/0.43 ![X0,X1]: (message(sent(X0,b,X1))|~intruder_message(X1)|~party_of_protocol(X0))),
% 0.08/0.43 inference(resolution,[status(thm)],[f79,f40])).
% 0.08/0.43 fof(f136,plain,(
% 0.08/0.43 ![X0,X1,X2]: (intruder_message(encrypt(X0,X1))|~intruder_message(X0)|~party_of_protocol(X2)|~intruder_message(X1)|~party_of_protocol(X2))),
% 0.08/0.43 inference(resolution,[status(thm)],[f83,f81])).
% 0.08/0.43 fof(f137,definition,(
% 0.08/0.43 ![X0,X1]: (sQ6_spl <=> (intruder_message(encrypt(X0,X1))|~intruder_message(X0)|~intruder_message(X1)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f138,plain,(
% 0.08/0.43 ![X0,X1]: (intruder_message(encrypt(X0,X1))|~intruder_message(X0)|~intruder_message(X1)|~sQ6_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f137])).
% 0.08/0.43 fof(f140,definition,(
% 0.08/0.43 ![X2]: (sQ7_spl <=> (~party_of_protocol(X2)|~party_of_protocol(X2)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f141,plain,(
% 0.08/0.43 ![X0]: (~party_of_protocol(X0)|~party_of_protocol(X0)|~sQ7_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f140])).
% 0.08/0.43 fof(f143,plain,(
% 0.08/0.43 sQ6_spl|sQ7_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f136,f137,f140])).
% 0.08/0.43 fof(f152,plain,(
% 0.08/0.43 $false|sQ1_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f94,f41])).
% 0.08/0.43 fof(f153,plain,(
% 0.08/0.43 sQ1_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f152])).
% 0.08/0.43 fof(f157,plain,(
% 0.08/0.43 intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))|~fresh_to_b(an_a_nonce)),
% 0.08/0.43 inference(resolution,[status(thm)],[f104,f36])).
% 0.08/0.43 fof(f158,definition,(
% 0.08/0.43 sQ10_spl <=> (intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f159,plain,(
% 0.08/0.43 intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))|~sQ10_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f158])).
% 0.08/0.43 fof(f161,plain,(
% 0.08/0.43 sQ10_spl|~sQ1_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f157,f158,f92])).
% 0.08/0.43 fof(f179,plain,(
% 0.08/0.43 $false|~sQ7_spl),
% 0.08/0.43 inference(backward_subsumption_resolution,[status(thm)],[f47,f182])).
% 0.08/0.43 fof(f182,plain,(
% 0.08/0.43 ![X0]: (~party_of_protocol(X0)|~sQ7_spl)),
% 0.08/0.43 inference(duplicate_literals_removal,[status(thm)],[f141])).
% 0.08/0.43 fof(f186,plain,(
% 0.08/0.43 ~sQ7_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f179])).
% 0.08/0.43 fof(f190,plain,(
% 0.08/0.43 ![X0]: (intruder_holds(key(X0,b))|~intruder_message(X0))),
% 0.08/0.43 inference(resolution,[status(thm)],[f40,f81])).
% 0.08/0.43 fof(f243,definition,(
% 0.08/0.43 sQ17_spl <=> (party_of_protocol(a))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f245,plain,(
% 0.08/0.43 ~party_of_protocol(a)|sQ17_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f243])).
% 0.08/0.43 fof(f292,plain,(
% 0.08/0.43 intruder_message(generate_b_nonce(an_a_nonce))|~sQ10_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f159,f59])).
% 0.08/0.43 fof(f293,plain,(
% 0.08/0.43 intruder_message(encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))|~sQ10_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f159,f61])).
% 0.08/0.43 fof(f296,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~intruder_message(pair(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),X0)))|~party_of_protocol(a)|~sQ0_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f106,f134])).
% 0.08/0.43 fof(f298,definition,(
% 0.08/0.43 ![X0]: (sQ23_spl <=> (b_holds(key(X0,a))|~intruder_message(pair(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),X0)))))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f299,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~intruder_message(pair(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),X0)))|~sQ23_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f298])).
% 0.08/0.43 fof(f301,plain,(
% 0.08/0.43 sQ23_spl|~sQ17_spl|~sQ0_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f296,f298,f243,f89])).
% 0.08/0.43 fof(f303,plain,(
% 0.08/0.43 $false|sQ17_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f245,f35])).
% 0.08/0.43 fof(f304,plain,(
% 0.08/0.43 sQ17_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f303])).
% 0.08/0.43 fof(f321,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~intruder_message(encrypt(generate_b_nonce(an_a_nonce),X0))|~intruder_message(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt))|~sQ23_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f299,f71])).
% 0.08/0.43 fof(f347,definition,(
% 0.08/0.43 sQ29_spl <=> (intruder_message(an_a_nonce))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f349,plain,(
% 0.08/0.43 ~intruder_message(an_a_nonce)|sQ29_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f347])).
% 0.08/0.43 fof(f378,plain,(
% 0.08/0.43 $false|sQ29_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f349,f107])).
% 0.08/0.43 fof(f379,plain,(
% 0.08/0.43 sQ29_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f378])).
% 0.08/0.43 fof(f448,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~intruder_message(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt))|~intruder_message(generate_b_nonce(an_a_nonce))|~intruder_message(X0)|~sQ23_spl|~sQ6_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f321,f138])).
% 0.08/0.43 fof(f449,definition,(
% 0.08/0.43 ![X0]: (sQ45_spl <=> (b_holds(key(X0,a))|~intruder_message(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt))|~intruder_message(X0)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f450,plain,(
% 0.08/0.43 ![X0]: (b_holds(key(X0,a))|~intruder_message(encrypt(triple(a,X0,generate_expiration_time(an_a_nonce)),bt))|~intruder_message(X0)|~sQ45_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f449])).
% 0.08/0.43 fof(f452,definition,(
% 0.08/0.43 sQ46_spl <=> (intruder_message(generate_b_nonce(an_a_nonce)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f454,plain,(
% 0.08/0.43 ~intruder_message(generate_b_nonce(an_a_nonce))|sQ46_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f452])).
% 0.08/0.43 fof(f455,plain,(
% 0.08/0.43 sQ45_spl|~sQ46_spl|~sQ23_spl|~sQ6_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f448,f449,f452,f298,f137])).
% 0.08/0.43 fof(f495,definition,(
% 0.08/0.43 sQ52_spl <=> (intruder_message(a))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f497,plain,(
% 0.08/0.43 ~intruder_message(a)|sQ52_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f495])).
% 0.08/0.43 fof(f546,plain,(
% 0.08/0.43 $false|sQ52_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f497,f108])).
% 0.08/0.43 fof(f547,plain,(
% 0.08/0.43 sQ52_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f546])).
% 0.08/0.43 fof(f566,plain,(
% 0.08/0.43 b_holds(key(an_a_nonce,a))|~intruder_message(an_a_nonce)|~sQ45_spl|~sQ10_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f450,f293])).
% 0.08/0.43 fof(f572,definition,(
% 0.08/0.43 sQ64_spl <=> (b_holds(key(an_a_nonce,a)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f573,plain,(
% 0.08/0.43 b_holds(key(an_a_nonce,a))|~sQ64_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f572])).
% 0.08/0.43 fof(f575,plain,(
% 0.08/0.43 sQ64_spl|~sQ29_spl|~sQ45_spl|~sQ10_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f566,f572,f347,f449,f158])).
% 0.08/0.43 fof(f584,plain,(
% 0.08/0.43 ~intruder_holds(key(an_a_nonce,b))|~sQ64_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f573,f87])).
% 0.08/0.43 fof(f592,plain,(
% 0.08/0.43 ~intruder_message(an_a_nonce)|~sQ64_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f584,f190])).
% 0.08/0.43 fof(f593,plain,(
% 0.08/0.43 ~sQ29_spl|~sQ64_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f592,f347,f572])).
% 0.08/0.43 fof(f594,plain,(
% 0.08/0.43 $false|~sQ10_spl|sQ46_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f454,f292])).
% 0.08/0.43 fof(f595,plain,(
% 0.08/0.43 ~sQ10_spl|sQ46_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f594])).
% 0.08/0.43 fof(f596,plain,(
% 0.08/0.43 $false),
% 0.08/0.43 inference(sat_refutation,[status(thm)],[f95,f143,f153,f161,f186,f301,f304,f379,f455,f547,f575,f593,f595])).
% 0.08/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.48 % Elapsed time: 0.100885 seconds
% 0.13/0.48 % CPU time: 0.298264 seconds
% 0.13/0.48 % Total memory used: 28.475 MB
% 0.13/0.48 % Net memory used: 28.308 MB
%------------------------------------------------------------------------------