%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV016-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:07:55 PM UTC 2026
% Result : Satisfiable 121.96s 21.04s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u45,negated_conjecture,
( ~ b_holds(key(X0,X2))
| ~ intruder_message(X0) ) ).
cnf(u91,axiom,
( intruder_message(encrypt(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u120,negated_conjecture,
~ fresh_to_b(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))) ).
cnf(u124,negated_conjecture,
~ party_of_protocol(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u167,negated_conjecture,
~ party_of_protocol(generate_b_nonce(an_a_nonce)) ).
cnf(u175,negated_conjecture,
~ party_of_protocol(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(u183,negated_conjecture,
~ party_of_protocol(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u191,negated_conjecture,
~ party_of_protocol(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))) ).
cnf(u199,negated_conjecture,
~ party_of_protocol(encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u211,negated_conjecture,
~ party_of_protocol(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at)) ).
cnf(u219,negated_conjecture,
~ party_of_protocol(pair(a,an_a_nonce)) ).
cnf(u227,negated_conjecture,
~ party_of_protocol(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce)))) ).
cnf(u235,negated_conjecture,
~ party_of_protocol(an_a_nonce) ).
cnf(u258,negated_conjecture,
~ fresh_to_b(generate_b_nonce(an_a_nonce)) ).
cnf(u267,negated_conjecture,
~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(u276,negated_conjecture,
~ fresh_to_b(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u285,negated_conjecture,
~ fresh_to_b(encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u294,negated_conjecture,
~ fresh_to_b(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u303,negated_conjecture,
~ fresh_to_b(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at)) ).
cnf(u312,negated_conjecture,
~ fresh_to_b(pair(a,an_a_nonce)) ).
cnf(u321,negated_conjecture,
~ fresh_to_b(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce)))) ).
cnf(u331,negated_conjecture,
~ fresh_to_b(b) ).
cnf(u340,negated_conjecture,
~ fresh_to_b(a) ).
cnf(u357,negated_conjecture,
~ party_of_protocol(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u362,negated_conjecture,
~ fresh_to_b(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u376,negated_conjecture,
~ party_of_protocol(encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u381,negated_conjecture,
~ fresh_to_b(encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u435,negated_conjecture,
~ a_nonce(generate_key(an_a_nonce)) ).
cnf(u544,negated_conjecture,
~ party_of_protocol(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(u549,negated_conjecture,
~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(u587,negated_conjecture,
~ party_of_protocol(encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u592,negated_conjecture,
~ fresh_to_b(encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u606,negated_conjecture,
~ a_nonce(encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u622,negated_conjecture,
b_stored(pair(b,an_a_nonce)) ).
cnf(u627,negated_conjecture,
b_holds(key(generate_key(an_a_nonce),b)) ).
cnf(u646,negated_conjecture,
~ party_of_protocol(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u651,negated_conjecture,
~ fresh_to_b(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u690,negated_conjecture,
~ intruder_message(at) ).
cnf(u772,negated_conjecture,
~ a_nonce(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u804,negated_conjecture,
( ~ t_holds(key(generate_key(an_a_nonce),X0))
| ~ t_holds(key(X1,b))
| ~ party_of_protocol(X0)
| intruder_message(triple(encrypt(quadruple(X0,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X1),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),X2))
| ~ intruder_message(X2)
| ~ intruder_message(X0) ) ).
cnf(a_stored_message_i_4,axiom,
a_stored(pair(b,an_a_nonce)) ).
cnf(u75,negated_conjecture,
intruder_message(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u524,negated_conjecture,
( ~ a_nonce(triple(X0,X1,X2))
| intruder_message(triple(encrypt(quadruple(b,triple(X0,X1,X2),generate_key(triple(X0,X1,X2)),generate_expiration_time(triple(X0,X1,X2))),bt),encrypt(triple(b,generate_key(triple(X0,X1,X2)),generate_expiration_time(triple(X0,X1,X2))),bt),generate_b_nonce(triple(X0,X1,X2))))
| ~ fresh_to_b(triple(X0,X1,X2))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u135,negated_conjecture,
intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(intruder_decomposes_quadruples_24,axiom,
( ~ intruder_message(quadruple(X1,X0,X2,X3))
| intruder_message(X0) ) ).
cnf(u521,negated_conjecture,
( ~ a_nonce(quadruple(X0,X1,X2,X3))
| intruder_message(triple(encrypt(quadruple(b,quadruple(X0,X1,X2,X3),generate_key(quadruple(X0,X1,X2,X3)),generate_expiration_time(quadruple(X0,X1,X2,X3))),bt),encrypt(triple(b,generate_key(quadruple(X0,X1,X2,X3)),generate_expiration_time(quadruple(X0,X1,X2,X3))),bt),generate_b_nonce(quadruple(X0,X1,X2,X3))))
| ~ fresh_to_b(quadruple(X0,X1,X2,X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u710,negated_conjecture,
( ~ a_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ fresh_to_b(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| intruder_message(triple(encrypt(quadruple(b,pair(X0,encrypt(X1,generate_key(an_a_nonce))),generate_key(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),bt),encrypt(triple(b,generate_key(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),bt),generate_b_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce))))))
| ~ intruder_message(X0) ) ).
cnf(u430,negated_conjecture,
( ~ t_holds(key(bt,X0))
| ~ t_holds(key(X1,b))
| ~ party_of_protocol(X0)
| intruder_message(triple(encrypt(quadruple(X0,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X1),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X2))
| ~ intruder_message(X2)
| ~ intruder_message(X0) ) ).
cnf(u442,negated_conjecture,
( ~ t_holds(key(X0,a))
| intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X0),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X1))
| ~ intruder_message(X1) ) ).
cnf(co1_40,negated_conjecture,
( ~ intruder_holds(key(X0,X2))
| ~ b_holds(key(X0,X1)) ) ).
cnf(u49,negated_conjecture,
message(sent(b,t,triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))) ).
cnf(u81,negated_conjecture,
( ~ intruder_message(pair(encrypt(triple(X1,X0,generate_expiration_time(X2)),bt),encrypt(generate_b_nonce(X2),X0)))
| ~ b_stored(pair(X1,X2))
| b_holds(key(X0,X1))
| ~ a_key(X0)
| ~ party_of_protocol(X1) ) ).
cnf(u348,negated_conjecture,
intruder_message(encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u63,negated_conjecture,
~ a_key(generate_expiration_time(X0)) ).
cnf(nonce_a_is_fresh_to_b_9,axiom,
fresh_to_b(an_a_nonce) ).
cnf(u452,negated_conjecture,
( message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))))
| ~ intruder_message(X0) ) ).
cnf(u756,negated_conjecture,
( ~ t_holds(key(X2,X3))
| ~ t_holds(key(X0,X1))
| intruder_message(triple(encrypt(quadruple(X3,X4,generate_key(X4),X5),X0),encrypt(triple(X1,generate_key(X4),X5),X2),X6))
| ~ a_nonce(X4)
| ~ intruder_message(X6)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ party_of_protocol(X3)
| ~ intruder_message(X5)
| ~ intruder_message(X4)
| ~ intruder_message(X1) ) ).
cnf(u415,negated_conjecture,
( ~ intruder_message(pair(a,X0))
| ~ a_nonce(X0)
| ~ a_stored(pair(b,X0))
| ~ fresh_to_b(X0)
| intruder_message(pair(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(generate_b_nonce(X0),generate_key(X0)))) ) ).
cnf(u531,negated_conjecture,
intruder_message(encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u746,negated_conjecture,
( ~ party_of_protocol(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),X1,generate_expiration_time(X1)),bt)))
| ~ intruder_message(X1)
| ~ fresh_to_b(X1) ) ).
cnf(b_accepts_secure_session_key_12,negated_conjecture,
( ~ message(sent(X1,b,pair(encrypt(triple(X1,X0,generate_expiration_time(X2)),bt),encrypt(generate_b_nonce(X2),X0))))
| ~ a_key(X0)
| ~ b_stored(pair(X1,X2))
| b_holds(key(X0,X1)) ) ).
cnf(u70,negated_conjecture,
( message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt))))
| ~ party_of_protocol(X0)
| ~ fresh_to_b(X1)
| ~ intruder_message(pair(X0,X1)) ) ).
cnf(intruder_composes_pairs_27,axiom,
( intruder_message(pair(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u478,negated_conjecture,
( ~ t_holds(key(X2,X1))
| ~ a_nonce(X0)
| ~ party_of_protocol(X1)
| ~ fresh_to_b(X0)
| intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),X2),encrypt(triple(X1,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0)))
| ~ intruder_message(X0)
| ~ intruder_message(X1) ) ).
cnf(u490,negated_conjecture,
( ~ a_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| intruder_message(triple(encrypt(quadruple(b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))),generate_key(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),at),encrypt(triple(a,generate_key(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),bt),generate_b_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))))
| ~ fresh_to_b(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0) ) ).
cnf(u788,negated_conjecture,
( ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0)
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ t_holds(key(X1,a))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X0,generate_key(an_a_nonce)),generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),X1),encrypt(triple(a,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))))) ) ).
cnf(u493,negated_conjecture,
( ~ a_nonce(encrypt(X0,X1))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X0,X1),generate_key(encrypt(X0,X1)),generate_expiration_time(encrypt(X0,X1))),at),encrypt(triple(a,generate_key(encrypt(X0,X1)),generate_expiration_time(encrypt(X0,X1))),bt),generate_b_nonce(encrypt(X0,X1))))
| ~ fresh_to_b(encrypt(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u798,negated_conjecture,
( ~ t_holds(key(generate_key(an_a_nonce),X0))
| ~ t_holds(key(X1,X2))
| ~ party_of_protocol(X0)
| intruder_message(triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X1),encrypt(triple(X2,generate_key(X3),X4),generate_key(an_a_nonce)),X5))
| ~ a_nonce(X3)
| ~ intruder_message(X5)
| ~ intruder_message(X0)
| ~ intruder_message(X4)
| ~ intruder_message(X3)
| ~ intruder_message(X2) ) ).
cnf(an_a_nonce_is_a_nonce_34,axiom,
a_nonce(an_a_nonce) ).
cnf(u51,negated_conjecture,
intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u732,negated_conjecture,
( ~ intruder_message(triple(a,X1,X2))
| ~ a_stored(pair(X0,X1))
| ~ party_of_protocol(X0)
| intruder_message(pair(encrypt(triple(a,generate_key(X1),X2),generate_key(an_a_nonce)),encrypt(X3,generate_key(X1))))
| ~ a_nonce(X1)
| ~ intruder_message(X3)
| ~ intruder_message(X0)
| ~ t_holds(key(generate_key(an_a_nonce),X0)) ) ).
cnf(u391,negated_conjecture,
( ~ fresh_to_b(pair(X0,X1))
| intruder_message(triple(b,generate_b_nonce(pair(X0,X1)),encrypt(triple(a,pair(X0,X1),generate_expiration_time(pair(X0,X1))),bt)))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u695,negated_conjecture,
( message(sent(a,b,pair(X0,encrypt(X1,generate_key(an_a_nonce)))))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(server_t_generates_key_16,negated_conjecture,
( ~ message(sent(X1,t,triple(X1,X6,encrypt(triple(X0,X2,X3),X5))))
| ~ a_nonce(X2)
| message(sent(t,X0,triple(encrypt(quadruple(X1,X2,generate_key(X2),X3),X4),encrypt(triple(X0,generate_key(X2),X3),X5),X6)))
| ~ t_holds(key(X4,X0))
| ~ t_holds(key(X5,X1)) ) ).
cnf(u701,negated_conjecture,
( b_stored(pair(a,encrypt(X0,generate_key(an_a_nonce))))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(a_is_party_of_protocol_2,axiom,
party_of_protocol(a) ).
cnf(intruder_message_sent_31,axiom,
( message(sent(X0,X1,X2))
| ~ intruder_message(X2)
| ~ party_of_protocol(X1)
| ~ party_of_protocol(X0) ) ).
cnf(u466,negated_conjecture,
( ~ party_of_protocol(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(encrypt(X0,generate_key(an_a_nonce)),X1,generate_expiration_time(X1)),bt)))
| ~ intruder_message(X1)
| ~ fresh_to_b(X1) ) ).
cnf(u409,negated_conjecture,
( ~ intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(a,X0,generate_expiration_time(X1)),bt)))
| ~ a_nonce(X0)
| ~ a_stored(pair(b,X0))
| ~ b_stored(pair(a,X1))
| b_holds(key(generate_key(X0),a)) ) ).
cnf(u73,negated_conjecture,
( message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1)))
| ~ party_of_protocol(X0)
| ~ a_nonce(X3)
| ~ intruder_message(triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))
| ~ t_holds(key(X6,X2))
| ~ t_holds(key(X5,X0)) ) ).
cnf(u469,negated_conjecture,
( ~ b_stored(pair(a,X0))
| ~ a_stored(pair(b,X0))
| ~ fresh_to_b(X0)
| ~ a_nonce(X0)
| b_holds(key(generate_key(X0),a))
| ~ intruder_message(X0) ) ).
cnf(u55,negated_conjecture,
~ a_key(generate_b_nonce(X0)) ).
cnf(u500,negated_conjecture,
( ~ a_nonce(quadruple(X0,X1,X2,X3))
| intruder_message(triple(encrypt(quadruple(b,quadruple(X0,X1,X2,X3),generate_key(quadruple(X0,X1,X2,X3)),generate_expiration_time(quadruple(X0,X1,X2,X3))),at),encrypt(triple(a,generate_key(quadruple(X0,X1,X2,X3)),generate_expiration_time(quadruple(X0,X1,X2,X3))),bt),generate_b_nonce(quadruple(X0,X1,X2,X3))))
| ~ fresh_to_b(quadruple(X0,X1,X2,X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u99,axiom,
intruder_message(a) ).
cnf(u781,negated_conjecture,
( ~ t_holds(key(X1,X2))
| ~ t_holds(key(X0,b))
| intruder_message(triple(encrypt(quadruple(X2,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X0),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X1),X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ party_of_protocol(X2) ) ).
cnf(generated_times_and_nonces_are_nonces_37,negated_conjecture,
a_nonce(generate_b_nonce(X0)) ).
cnf(u745,negated_conjecture,
( ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(b,generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),encrypt(triple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt)))
| ~ intruder_message(X0) ) ).
cnf(b_hold_key_bt_for_t_7,axiom,
b_holds(key(bt,t)) ).
cnf(u77,negated_conjecture,
intruder_message(generate_b_nonce(an_a_nonce)) ).
cnf(b_creates_freash_nonces_in_time_10,negated_conjecture,
( ~ message(sent(X1,b,pair(X1,X0)))
| ~ fresh_to_b(X0)
| message(sent(b,t,triple(b,generate_b_nonce(X0),encrypt(triple(X1,X0,generate_expiration_time(X0)),bt)))) ) ).
cnf(generated_keys_are_keys_39,negated_conjecture,
a_key(generate_key(X0)) ).
cnf(u416,negated_conjecture,
( ~ intruder_message(pair(a,X0))
| ~ a_nonce(X0)
| ~ a_stored(pair(b,X0))
| ~ fresh_to_b(X0)
| ~ b_stored(pair(a,X0))
| b_holds(key(generate_key(X0),a)) ) ).
cnf(intruder_key_encrypts_33,axiom,
( ~ intruder_holds(key(X1,X2))
| intruder_message(encrypt(X0,X1))
| ~ intruder_message(X0)
| ~ party_of_protocol(X2) ) ).
cnf(u103,negated_conjecture,
( message(sent(t,X0,triple(encrypt(quadruple(b,X1,generate_key(X1),generate_expiration_time(X1)),X2),encrypt(triple(X0,generate_key(X1),generate_expiration_time(X1)),bt),generate_b_nonce(X1))))
| ~ fresh_to_b(X1)
| ~ intruder_message(pair(X0,X1))
| ~ a_nonce(X1)
| ~ party_of_protocol(X0)
| ~ t_holds(key(X2,X0)) ) ).
cnf(u511,negated_conjecture,
( ~ a_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| intruder_message(triple(encrypt(quadruple(b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))),generate_key(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),bt),encrypt(triple(b,generate_key(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),bt),generate_b_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))))
| ~ fresh_to_b(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0) ) ).
cnf(u782,negated_conjecture,
( ~ t_holds(key(X1,X2))
| ~ t_holds(key(X0,b))
| intruder_message(triple(encrypt(quadruple(X2,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X0),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X1),X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ party_of_protocol(X2) ) ).
cnf(u62,negated_conjecture,
intruder_message(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce)))) ).
cnf(u106,negated_conjecture,
( message(sent(a,X0,pair(encrypt(triple(a,generate_key(X1),X3),X4),encrypt(X2,generate_key(X1)))))
| ~ a_nonce(X1)
| ~ intruder_message(triple(X0,X2,encrypt(triple(a,X1,X3),X4)))
| ~ t_holds(key(X4,X0))
| ~ a_stored(pair(X0,X1))
| ~ party_of_protocol(X0) ) ).
cnf(u731,negated_conjecture,
( ~ intruder_message(triple(a,X2,X3))
| ~ a_stored(pair(X1,X2))
| ~ party_of_protocol(X1)
| intruder_message(pair(encrypt(triple(a,generate_key(X2),X3),X0),encrypt(X4,generate_key(X2))))
| ~ a_nonce(X2)
| ~ intruder_message(X4)
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ t_holds(key(X0,X1)) ) ).
cnf(u743,negated_conjecture,
( ~ a_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(encrypt(quadruple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),at),encrypt(triple(a,generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))))
| ~ intruder_message(X0) ) ).
cnf(u742,negated_conjecture,
( ~ a_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(encrypt(quadruple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),encrypt(triple(b,generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))))
| ~ intruder_message(X0) ) ).
cnf(u238,negated_conjecture,
( ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X0),encrypt(triple(a,X0,generate_expiration_time(X0)),bt)))
| ~ fresh_to_b(X0) ) ).
cnf(intruder_decomposes_triples_21,axiom,
( ~ intruder_message(triple(X1,X0,X2))
| intruder_message(X0) ) ).
cnf(u422,negated_conjecture,
( ~ t_holds(key(X0,b))
| intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X0),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ) ).
cnf(t_holds_key_bt_for_b_14,axiom,
t_holds(key(bt,b)) ).
cnf(u459,negated_conjecture,
( intruder_message(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(u712,negated_conjecture,
( ~ fresh_to_b(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| intruder_message(triple(b,generate_b_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),encrypt(triple(a,pair(X0,encrypt(X1,generate_key(an_a_nonce))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u151,negated_conjecture,
( ~ party_of_protocol(encrypt(X0,X1))
| intruder_message(triple(b,generate_b_nonce(X2),encrypt(triple(encrypt(X0,X1),X2,generate_expiration_time(X2)),bt)))
| ~ intruder_message(X2)
| ~ fresh_to_b(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u38,axiom,
~ a_key(an_a_nonce) ).
cnf(u700,negated_conjecture,
( message(sent(b,t,triple(b,generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),encrypt(triple(a,encrypt(X0,generate_key(an_a_nonce)),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt))))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(u82,negated_conjecture,
b_holds(key(generate_key(an_a_nonce),a)) ).
cnf(u735,negated_conjecture,
( ~ t_holds(key(X0,b))
| intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X0),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X1))
| ~ intruder_message(X1) ) ).
cnf(intruder_decomposes_quadruples_25,axiom,
( ~ intruder_message(quadruple(X1,X2,X0,X3))
| intruder_message(X0) ) ).
cnf(u53,negated_conjecture,
( message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X0),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))))
| ~ t_holds(key(X0,a)) ) ).
cnf(u713,negated_conjecture,
( ~ fresh_to_b(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| intruder_message(triple(b,generate_b_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),encrypt(triple(b,pair(X0,encrypt(X1,generate_key(an_a_nonce))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u505,negated_conjecture,
( ~ a_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(encrypt(quadruple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),at),encrypt(triple(a,generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))))
| ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0) ) ).
cnf(u449,negated_conjecture,
( ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(b,generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),encrypt(triple(a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u512,negated_conjecture,
( ~ a_nonce(pair(X0,X1))
| intruder_message(triple(encrypt(quadruple(b,pair(X0,X1),generate_key(pair(X0,X1)),generate_expiration_time(pair(X0,X1))),bt),encrypt(triple(b,generate_key(pair(X0,X1)),generate_expiration_time(pair(X0,X1))),bt),generate_b_nonce(pair(X0,X1))))
| ~ fresh_to_b(pair(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u461,negated_conjecture,
( ~ fresh_to_b(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| intruder_message(triple(b,generate_b_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),encrypt(triple(b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u718,negated_conjecture,
( ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce))))
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0)
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| b_holds(key(generate_key(encrypt(X0,generate_key(an_a_nonce))),a)) ) ).
cnf(u803,negated_conjecture,
( ~ t_holds(key(generate_key(an_a_nonce),X0))
| ~ t_holds(key(X1,b))
| ~ party_of_protocol(X0)
| intruder_message(triple(encrypt(quadruple(X0,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),X1),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),X2))
| ~ intruder_message(X2)
| ~ intruder_message(X0) ) ).
cnf(u431,negated_conjecture,
( ~ t_holds(key(bt,X0))
| ~ t_holds(key(X1,a))
| ~ party_of_protocol(X0)
| intruder_message(triple(encrypt(quadruple(X0,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X1),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X2))
| ~ intruder_message(X2)
| ~ intruder_message(X0) ) ).
cnf(u526,negated_conjecture,
( ~ a_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(encrypt(quadruple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),encrypt(triple(b,generate_key(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt),generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))))
| ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0) ) ).
cnf(u463,negated_conjecture,
( ~ intruder_message(triple(X0,X1,X2))
| ~ party_of_protocol(X3)
| ~ t_holds(key(X4,X0))
| ~ t_holds(key(generate_key(an_a_nonce),X3))
| intruder_message(triple(encrypt(quadruple(X3,X1,generate_key(X1),X2),X4),encrypt(triple(X0,generate_key(X1),X2),generate_key(an_a_nonce)),X5))
| ~ a_nonce(X1)
| ~ intruder_message(X5)
| ~ intruder_message(X3) ) ).
cnf(u464,negated_conjecture,
( ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| intruder_message(triple(b,generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),encrypt(triple(a,encrypt(X0,generate_key(an_a_nonce)),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt)))
| ~ intruder_message(X0) ) ).
cnf(intruder_composes_triples_28,axiom,
( intruder_message(triple(X0,X1,X2))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u86,negated_conjecture,
intruder_message(b) ).
cnf(u711,negated_conjecture,
( ~ a_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ fresh_to_b(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| intruder_message(triple(encrypt(quadruple(b,pair(X0,encrypt(X1,generate_key(an_a_nonce))),generate_key(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),at),encrypt(triple(a,generate_key(pair(X0,encrypt(X1,generate_key(an_a_nonce)))),generate_expiration_time(pair(X0,encrypt(X1,generate_key(an_a_nonce))))),bt),generate_b_nonce(pair(X0,encrypt(X1,generate_key(an_a_nonce))))))
| ~ intruder_message(X0) ) ).
cnf(u158,negated_conjecture,
( ~ party_of_protocol(triple(X0,X1,X2))
| intruder_message(triple(b,generate_b_nonce(X3),encrypt(triple(triple(X0,X1,X2),X3,generate_expiration_time(X3)),bt)))
| ~ intruder_message(X3)
| ~ fresh_to_b(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u494,negated_conjecture,
( ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X0,generate_key(an_a_nonce)),generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),at),encrypt(triple(a,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),generate_b_nonce(encrypt(X0,generate_key(an_a_nonce)))))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(u717,negated_conjecture,
( ~ intruder_message(encrypt(triple(X0,generate_key(an_a_nonce),generate_expiration_time(X1)),bt))
| ~ intruder_message(generate_b_nonce(X1))
| ~ b_stored(pair(X0,X1))
| b_holds(key(generate_key(an_a_nonce),X0))
| ~ party_of_protocol(X0) ) ).
cnf(a_forwards_secure_5,negated_conjecture,
( ~ message(sent(t,a,triple(encrypt(quadruple(X0,X4,X3,X5),at),X1,X2)))
| ~ a_stored(pair(X0,X4))
| message(sent(a,X0,pair(X1,encrypt(X2,X3)))) ) ).
cnf(u127,negated_conjecture,
( ~ intruder_message(pair(X1,X0))
| ~ fresh_to_b(X0)
| ~ a_nonce(X0)
| ~ party_of_protocol(X1)
| ~ t_holds(key(X2,X1))
| intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),X2),encrypt(triple(X1,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0))) ) ).
cnf(t_holds_key_at_for_a_13,negated_conjecture,
t_holds(key(at,a)) ).
cnf(u71,axiom,
( ~ intruder_message(pair(X0,X1))
| ~ party_of_protocol(X0)
| ~ fresh_to_b(X1)
| b_stored(pair(X0,X1)) ) ).
cnf(u514,negated_conjecture,
( ~ a_nonce(encrypt(X0,X1))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X0,X1),generate_key(encrypt(X0,X1)),generate_expiration_time(encrypt(X0,X1))),bt),encrypt(triple(b,generate_key(encrypt(X0,X1)),generate_expiration_time(encrypt(X0,X1))),bt),generate_b_nonce(encrypt(X0,X1))))
| ~ fresh_to_b(encrypt(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u451,negated_conjecture,
( ~ party_of_protocol(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),X1,generate_expiration_time(X1)),bt)))
| ~ intruder_message(X1)
| ~ fresh_to_b(X1) ) ).
cnf(u243,negated_conjecture,
( ~ fresh_to_b(pair(X0,X1))
| intruder_message(triple(b,generate_b_nonce(pair(X0,X1)),encrypt(triple(b,pair(X0,X1),generate_expiration_time(pair(X0,X1))),bt)))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u702,negated_conjecture,
( ~ a_nonce(encrypt(X1,generate_key(an_a_nonce)))
| ~ intruder_message(X1)
| ~ fresh_to_b(encrypt(X1,generate_key(an_a_nonce)))
| ~ intruder_message(X0)
| ~ party_of_protocol(X0)
| ~ t_holds(key(X2,X0))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X1,generate_key(an_a_nonce)),generate_key(encrypt(X1,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X1,generate_key(an_a_nonce)))),X2),encrypt(triple(X0,generate_key(encrypt(X1,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X1,generate_key(an_a_nonce)))),bt),generate_b_nonce(encrypt(X1,generate_key(an_a_nonce))))) ) ).
cnf(a_sent_message_i_to_b_3,axiom,
message(sent(a,b,pair(a,an_a_nonce))) ).
cnf(intruder_holds_key_32,axiom,
( intruder_holds(key(X0,X1))
| ~ intruder_message(X0)
| ~ party_of_protocol(X1) ) ).
cnf(u100,axiom,
intruder_message(an_a_nonce) ).
cnf(u74,negated_conjecture,
( ~ intruder_message(triple(encrypt(quadruple(X0,X1,X2,X3),at),X4,X5))
| ~ a_stored(pair(X0,X1))
| message(sent(a,X0,pair(X4,encrypt(X5,X2)))) ) ).
cnf(u529,negated_conjecture,
intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ).
cnf(u134,negated_conjecture,
( ~ intruder_message(encrypt(quadruple(X0,X1,X4,X5),at))
| message(sent(a,X0,pair(X2,encrypt(X3,X4))))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ a_stored(pair(X0,X1)) ) ).
cnf(intruder_decomposes_pairs_19,axiom,
( ~ intruder_message(pair(X1,X0))
| intruder_message(X0) ) ).
cnf(u425,negated_conjecture,
( ~ intruder_message(encrypt(triple(a,X0,generate_expiration_time(X1)),bt))
| ~ a_stored(pair(b,X0))
| ~ b_stored(pair(a,X1))
| b_holds(key(generate_key(X0),a))
| ~ a_nonce(X0)
| ~ intruder_message(generate_b_nonce(X1)) ) ).
cnf(u485,negated_conjecture,
( ~ intruder_message(X0)
| ~ fresh_to_b(X0)
| intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),at),encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0)))
| ~ a_nonce(X0) ) ).
cnf(u149,negated_conjecture,
( ~ party_of_protocol(pair(X0,X1))
| intruder_message(triple(b,generate_b_nonce(X2),encrypt(triple(pair(X0,X1),X2,generate_expiration_time(X2)),bt)))
| ~ intruder_message(X2)
| ~ fresh_to_b(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u48,axiom,
intruder_message(pair(a,an_a_nonce)) ).
cnf(u129,negated_conjecture,
( message(sent(a,b,pair(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(generate_b_nonce(X0),generate_key(X0)))))
| ~ intruder_message(pair(a,X0))
| ~ a_nonce(X0)
| ~ a_stored(pair(b,X0))
| ~ fresh_to_b(X0) ) ).
cnf(u736,negated_conjecture,
( intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0) ) ).
cnf(u699,negated_conjecture,
( intruder_message(pair(X1,encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(b_is_party_of_protocol_8,axiom,
party_of_protocol(b) ).
cnf(u250,negated_conjecture,
( ~ fresh_to_b(quadruple(X0,X1,X2,X3))
| intruder_message(triple(b,generate_b_nonce(quadruple(X0,X1,X2,X3)),encrypt(triple(b,quadruple(X0,X1,X2,X3),generate_expiration_time(quadruple(X0,X1,X2,X3))),bt)))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(intruder_decomposes_quadruples_23,axiom,
( ~ intruder_message(quadruple(X0,X1,X2,X3))
| intruder_message(X0) ) ).
cnf(generated_times_and_nonces_are_nonces_36,negated_conjecture,
a_nonce(generate_expiration_time(X0)) ).
cnf(u429,negated_conjecture,
( ~ intruder_message(triple(X2,X4,X5))
| ~ t_holds(key(X1,X2))
| ~ t_holds(key(X3,X0))
| intruder_message(triple(encrypt(quadruple(X0,X4,generate_key(X4),X5),X1),encrypt(triple(X2,generate_key(X4),X5),X3),X6))
| ~ a_nonce(X4)
| ~ intruder_message(X6)
| ~ intruder_message(X0)
| ~ intruder_message(X3)
| ~ party_of_protocol(X0) ) ).
cnf(u137,negated_conjecture,
intruder_message(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at)) ).
cnf(intruder_decomposes_quadruples_26,axiom,
( ~ intruder_message(quadruple(X1,X2,X3,X0))
| intruder_message(X0) ) ).
cnf(u156,negated_conjecture,
( ~ party_of_protocol(quadruple(X0,X1,X2,X3))
| intruder_message(triple(b,generate_b_nonce(X4),encrypt(triple(quadruple(X0,X1,X2,X3),X4,generate_expiration_time(X4)),bt)))
| ~ intruder_message(X4)
| ~ fresh_to_b(X4)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u59,negated_conjecture,
( ~ t_holds(key(X0,a))
| intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X0),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ) ).
cnf(u327,negated_conjecture,
intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(b,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ).
cnf(u793,negated_conjecture,
( ~ t_holds(key(generate_key(an_a_nonce),X0))
| ~ party_of_protocol(X0)
| intruder_message(pair(encrypt(triple(a,generate_key(X1),X2),generate_key(an_a_nonce)),encrypt(X3,generate_key(X1))))
| ~ a_nonce(X1)
| ~ intruder_message(X3)
| ~ intruder_message(X0)
| ~ a_stored(pair(X0,X1))
| ~ intruder_message(X2)
| ~ intruder_message(X1) ) ).
cnf(u744,negated_conjecture,
( ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(b,generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),encrypt(triple(a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(triple(b,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u399,negated_conjecture,
( ~ fresh_to_b(quadruple(X0,X1,X2,X3))
| intruder_message(triple(b,generate_b_nonce(quadruple(X0,X1,X2,X3)),encrypt(triple(a,quadruple(X0,X1,X2,X3),generate_expiration_time(quadruple(X0,X1,X2,X3))),bt)))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u515,negated_conjecture,
( ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| intruder_message(triple(encrypt(quadruple(b,encrypt(X0,generate_key(an_a_nonce)),generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),encrypt(triple(b,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),generate_b_nonce(encrypt(X0,generate_key(an_a_nonce)))))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(u703,negated_conjecture,
( ~ fresh_to_b(encrypt(X1,generate_key(an_a_nonce)))
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ party_of_protocol(X0)
| intruder_message(triple(b,generate_b_nonce(encrypt(X1,generate_key(an_a_nonce))),encrypt(triple(X0,encrypt(X1,generate_key(an_a_nonce)),generate_expiration_time(encrypt(X1,generate_key(an_a_nonce)))),bt))) ) ).
cnf(u460,negated_conjecture,
( ~ fresh_to_b(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| intruder_message(triple(b,generate_b_nonce(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce)))),encrypt(triple(a,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u402,negated_conjecture,
( ~ fresh_to_b(triple(X0,X1,X2))
| intruder_message(triple(b,generate_b_nonce(triple(X0,X1,X2)),encrypt(triple(a,triple(X0,X1,X2),generate_expiration_time(triple(X0,X1,X2))),bt)))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(b_creates_freash_nonces_in_time_11,axiom,
( ~ message(sent(X0,b,pair(X0,X1)))
| ~ fresh_to_b(X1)
| b_stored(pair(X0,X1)) ) ).
cnf(u462,negated_conjecture,
( ~ party_of_protocol(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))),X1,generate_expiration_time(X1)),bt)))
| ~ intruder_message(X1)
| ~ fresh_to_b(X1) ) ).
cnf(u474,negated_conjecture,
( ~ a_stored(pair(b,X0))
| ~ fresh_to_b(X0)
| ~ a_nonce(X0)
| b_holds(key(generate_key(X0),a))
| ~ intruder_message(X0) ) ).
cnf(u141,negated_conjecture,
( ~ intruder_message(encrypt(triple(X0,X2,generate_expiration_time(X1)),bt))
| b_holds(key(X2,X0))
| ~ a_key(X2)
| ~ party_of_protocol(X0)
| ~ intruder_message(encrypt(generate_b_nonce(X1),X2))
| ~ b_stored(pair(X0,X1)) ) ).
cnf(nothing_is_a_nonce_and_a_key_38,axiom,
( ~ a_nonce(X0)
| ~ a_key(X0) ) ).
cnf(u443,negated_conjecture,
( intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| ~ intruder_message(X0) ) ).
cnf(u716,negated_conjecture,
( ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce))))
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0)
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| intruder_message(pair(encrypt(triple(a,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),encrypt(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),generate_key(encrypt(X0,generate_key(an_a_nonce)))))) ) ).
cnf(u503,negated_conjecture,
( ~ a_nonce(triple(X0,X1,X2))
| intruder_message(triple(encrypt(quadruple(b,triple(X0,X1,X2),generate_key(triple(X0,X1,X2)),generate_expiration_time(triple(X0,X1,X2))),at),encrypt(triple(a,generate_key(triple(X0,X1,X2)),generate_expiration_time(triple(X0,X1,X2))),bt),generate_b_nonce(triple(X0,X1,X2))))
| ~ fresh_to_b(triple(X0,X1,X2))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u54,negated_conjecture,
~ intruder_message(bt) ).
cnf(u679,negated_conjecture,
( ~ a_stored(pair(b,X0))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| intruder_message(pair(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(generate_b_nonce(X0),generate_key(X0))))
| ~ intruder_message(X0) ) ).
cnf(u789,negated_conjecture,
( message(sent(a,b,pair(encrypt(triple(a,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),encrypt(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),generate_key(encrypt(X0,generate_key(an_a_nonce)))))))
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0) ) ).
cnf(u723,negated_conjecture,
( message(sent(t,a,triple(encrypt(quadruple(b,encrypt(X0,generate_key(an_a_nonce)),generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),X1),encrypt(triple(a,generate_key(encrypt(X0,generate_key(an_a_nonce))),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt),generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))))))
| ~ intruder_message(X0)
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ t_holds(key(X1,a)) ) ).
cnf(u751,negated_conjecture,
( ~ t_holds(key(X3,X0))
| ~ party_of_protocol(X0)
| intruder_message(pair(encrypt(triple(a,generate_key(X1),X2),X3),encrypt(X4,generate_key(X1))))
| ~ a_nonce(X1)
| ~ intruder_message(X4)
| ~ intruder_message(X0)
| ~ intruder_message(X3)
| ~ a_stored(pair(X0,X1))
| ~ intruder_message(X2)
| ~ intruder_message(X1) ) ).
cnf(u406,negated_conjecture,
( ~ intruder_message(triple(X1,X2,encrypt(triple(a,X0,X3),X4)))
| ~ a_nonce(X0)
| ~ t_holds(key(X4,X1))
| ~ a_stored(pair(X1,X0))
| ~ party_of_protocol(X1)
| intruder_message(pair(encrypt(triple(a,generate_key(X0),X3),X4),encrypt(X2,generate_key(X0)))) ) ).
cnf(t_is_party_of_protocol_15,axiom,
party_of_protocol(t) ).
cnf(u450,negated_conjecture,
( ~ fresh_to_b(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))
| intruder_message(triple(b,generate_b_nonce(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0)),encrypt(triple(b,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0),generate_expiration_time(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),X0))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u393,negated_conjecture,
( ~ fresh_to_b(encrypt(X0,X1))
| intruder_message(triple(b,generate_b_nonce(encrypt(X0,X1)),encrypt(triple(a,encrypt(X0,X1),generate_expiration_time(encrypt(X0,X1))),bt)))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u245,negated_conjecture,
( ~ fresh_to_b(encrypt(X0,X1))
| intruder_message(triple(b,generate_b_nonce(encrypt(X0,X1)),encrypt(triple(b,encrypt(X0,X1),generate_expiration_time(encrypt(X0,X1))),bt)))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(intruder_decomposes_pairs_18,axiom,
( ~ intruder_message(pair(X0,X1))
| intruder_message(X0) ) ).
cnf(u76,negated_conjecture,
intruder_message(encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u484,negated_conjecture,
( ~ intruder_message(X0)
| ~ fresh_to_b(X0)
| intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(triple(b,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0)))
| ~ a_nonce(X0) ) ).
cnf(u419,negated_conjecture,
( ~ intruder_message(encrypt(triple(X3,X0,X5),X4))
| ~ party_of_protocol(X1)
| ~ t_holds(key(X2,X3))
| ~ t_holds(key(X4,X1))
| intruder_message(triple(encrypt(quadruple(X1,X0,generate_key(X0),X5),X2),encrypt(triple(X3,generate_key(X0),X5),X4),X6))
| ~ a_nonce(X0)
| ~ intruder_message(X6)
| ~ intruder_message(X1) ) ).
cnf(u83,negated_conjecture,
~ intruder_message(generate_key(an_a_nonce)) ).
cnf(u704,negated_conjecture,
( b_stored(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ party_of_protocol(X0)
| ~ fresh_to_b(encrypt(X1,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ) ).
cnf(u143,negated_conjecture,
( ~ intruder_message(X1)
| ~ party_of_protocol(X1)
| intruder_message(triple(b,generate_b_nonce(X0),encrypt(triple(X1,X0,generate_expiration_time(X0)),bt)))
| ~ intruder_message(X0)
| ~ fresh_to_b(X0) ) ).
cnf(u102,negated_conjecture,
( ~ intruder_message(pair(X0,X1))
| ~ fresh_to_b(X1)
| ~ party_of_protocol(X0)
| intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt))) ) ).
cnf(u727,negated_conjecture,
( ~ intruder_message(encrypt(triple(a,X0,X3),X1))
| ~ t_holds(key(X1,X2))
| ~ a_stored(pair(X2,X0))
| ~ party_of_protocol(X2)
| intruder_message(pair(encrypt(triple(a,generate_key(X0),X3),X1),encrypt(X4,generate_key(X0))))
| ~ a_nonce(X0)
| ~ intruder_message(X4)
| ~ intruder_message(X2) ) ).
cnf(u57,axiom,
b_stored(pair(a,an_a_nonce)) ).
cnf(u454,negated_conjecture,
( intruder_message(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0) ) ).
cnf(u491,negated_conjecture,
( ~ a_nonce(pair(X0,X1))
| intruder_message(triple(encrypt(quadruple(b,pair(X0,X1),generate_key(pair(X0,X1)),generate_expiration_time(pair(X0,X1))),at),encrypt(triple(a,generate_key(pair(X0,X1)),generate_expiration_time(pair(X0,X1))),bt),generate_b_nonce(pair(X0,X1))))
| ~ fresh_to_b(pair(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(intruder_decomposes_triples_22,axiom,
( ~ intruder_message(triple(X1,X2,X0))
| intruder_message(X0) ) ).
cnf(u465,negated_conjecture,
( ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| intruder_message(triple(b,generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),encrypt(triple(b,encrypt(X0,generate_key(an_a_nonce)),generate_expiration_time(encrypt(X0,generate_key(an_a_nonce)))),bt)))
| ~ intruder_message(X0) ) ).
cnf(u64,negated_conjecture,
intruder_message(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))) ).
cnf(u252,negated_conjecture,
( ~ fresh_to_b(triple(X0,X1,X2))
| intruder_message(triple(b,generate_b_nonce(triple(X0,X1,X2)),encrypt(triple(b,triple(X0,X1,X2),generate_expiration_time(triple(X0,X1,X2))),bt)))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(intruder_can_record_17,axiom,
( ~ message(sent(X1,X2,X0))
| intruder_message(X0) ) ).
cnf(intruder_composes_quadruples_29,axiom,
( intruder_message(quadruple(X0,X1,X2,X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(u530,negated_conjecture,
intruder_message(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ).
cnf(u111,axiom,
( b_stored(pair(X0,X1))
| ~ fresh_to_b(X1)
| ~ party_of_protocol(X0)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ) ).
cnf(intruder_decomposes_triples_20,axiom,
( ~ intruder_message(triple(X0,X1,X2))
| intruder_message(X0) ) ).
cnf(u61,negated_conjecture,
message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))))) ).
cnf(u105,negated_conjecture,
( ~ intruder_message(triple(X0,X2,encrypt(triple(X3,X1,X4),X5)))
| ~ a_nonce(X1)
| ~ party_of_protocol(X0)
| ~ t_holds(key(X6,X3))
| ~ t_holds(key(X5,X0))
| intruder_message(triple(encrypt(quadruple(X0,X1,generate_key(X1),X4),X6),encrypt(triple(X3,generate_key(X1),X4),X5),X2)) ) ).
cnf(u237,negated_conjecture,
( ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X0),encrypt(triple(b,X0,generate_expiration_time(X0)),bt)))
| ~ fresh_to_b(X0) ) ).
cnf(u714,negated_conjecture,
( ~ party_of_protocol(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| intruder_message(triple(b,generate_b_nonce(X2),encrypt(triple(pair(X0,encrypt(X1,generate_key(an_a_nonce))),X2,generate_expiration_time(X2)),bt)))
| ~ intruder_message(X2)
| ~ fresh_to_b(X2) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV016-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n004.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 09:42:27 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.05/2.22 % (244410)Input is clausal, will run a generic CNF schedule.
% 11.05/2.22 % (244533)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=28732055:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.05/2.22 % (244529)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=29636154:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.05/2.22 % (244528)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=470548550:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.05/2.22 % (244526)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=3772284744:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.05/2.22 % (244530)lrs+10_1_sil=8000:sp=occurrence:random_seed=1803091155:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.05/2.22 % (244532)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1782294999:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.05/2.22 % (244535)dis-21_1_sil=8000:lcm=predicate:random_seed=982658569:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.05/2.22 % (244533)Instruction limit reached!
% 11.05/2.22 % (244533)------------------------------
% 11.05/2.22 % (244533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.22 % (244533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.22 % (244533)CaDiCaL version: 2.1.3
% 11.05/2.22 % (244533)Termination reason: Instruction limit
% 11.05/2.22 % (244533)Termination phase: Saturation
% 11.05/2.22 % (244533)Time elapsed: 0.062 s
% 11.05/2.22 % (244533)Peak memory usage: 92 MB
% 11.05/2.22 % (244533)Instructions burned: 180 (million)
% 11.05/2.22 % (244530)Instruction limit reached!
% 11.05/2.22 % (244530)------------------------------
% 11.05/2.22 % (244530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.22 % (244530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.22 % (244530)CaDiCaL version: 2.1.3
% 11.05/2.22 % (244530)Termination reason: Instruction limit
% 11.05/2.22 % (244530)Termination phase: Saturation
% 11.05/2.22 % (244530)Time elapsed: 0.068 s
% 11.05/2.22 % (244530)Peak memory usage: 89 MB
% 11.05/2.22 % (244530)Instructions burned: 108 (million)
% 11.05/2.22 % (244535)Instruction limit reached!
% 11.05/2.22 % (244535)------------------------------
% 11.05/2.22 % (244535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.22 % (244535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.22 % (244535)CaDiCaL version: 2.1.3
% 11.05/2.22 % (244535)Termination reason: Instruction limit
% 11.05/2.22 % (244535)Termination phase: Saturation
% 11.05/2.22 % (244535)Time elapsed: 0.068 s
% 11.05/2.22 % (244535)Peak memory usage: 89 MB
% 11.05/2.22 % (244535)Instructions burned: 118 (million)
% 11.05/2.22 % (244532)Instruction limit reached!
% 11.05/2.22 % (244532)------------------------------
% 11.05/2.22 % (244532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.22 % (244532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.22 % (244532)CaDiCaL version: 2.1.3
% 11.05/2.22 % (244532)Termination reason: Instruction limit
% 11.05/2.22 % (244532)Termination phase: Saturation
% 11.05/2.22 % (244532)Time elapsed: 0.095 s
% 11.05/2.22 % (244532)Peak memory usage: 88 MB
% 11.05/2.22 % (244532)Instructions burned: 115 (million)
% 11.05/2.22 % (244572)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1663048398:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.05/2.22 % (244572)Refutation not found, incomplete strategy
% 11.05/2.22 % (244572)------------------------------
% 11.05/2.22 % (244572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.22 % (244572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.22 % (244572)CaDiCaL version: 2.1.3
% 11.05/2.22 % (244572)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.22 % (244572)Time elapsed: 0.001 s
% 11.05/2.22 % (244572)Peak memory usage: 88 MB
% 11.05/2.22 % (244572)Instructions burned: 1 (million)
% 11.05/2.22 % (244573)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1996364046:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 19.39/3.48 % (244574)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2566898722:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.39/3.48 % (244574)Refutation not found, incomplete strategy
% 19.39/3.48 % (244574)------------------------------
% 19.39/3.48 % (244574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.48 % (244574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.48 % (244574)CaDiCaL version: 2.1.3
% 19.39/3.48 % (244574)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.48 % (244574)Time elapsed: 0.002 s
% 19.39/3.48 % (244574)Peak memory usage: 88 MB
% 19.39/3.48 % (244574)Instructions burned: 1 (million)
% 19.39/3.48 % (244577)lrs+10_64_to=lpo:sil=8000:random_seed=3338888833:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 19.39/3.48 % (244572)------------------------------
% 19.39/3.48 % (244572)------------------------------
% 19.39/3.48 % (244573)Instruction limit reached!
% 19.39/3.48 % (244573)------------------------------
% 19.39/3.48 % (244573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.48 % (244573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.48 % (244573)CaDiCaL version: 2.1.3
% 19.39/3.48 % (244573)Termination reason: Instruction limit
% 19.39/3.48 % (244573)Termination phase: Saturation
% 19.39/3.48 % (244573)Time elapsed: 0.109 s
% 19.39/3.48 % (244573)Peak memory usage: 92 MB
% 19.39/3.48 % (244573)Instructions burned: 191 (million)
% 19.39/3.48 % (244577)Instruction limit reached!
% 19.39/3.48 % (244577)------------------------------
% 19.39/3.48 % (244577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.48 % (244577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.48 % (244577)CaDiCaL version: 2.1.3
% 19.39/3.48 % (244577)Termination reason: Instruction limit
% 19.39/3.48 % (244577)Termination phase: Saturation
% 19.39/3.48 % (244577)Time elapsed: 0.071 s
% 19.39/3.48 % (244577)Peak memory usage: 90 MB
% 19.39/3.48 % (244577)Instructions burned: 127 (million)
% 19.39/3.48 % (244654)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=355717574:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.39/3.48 % (244654)Refutation not found, incomplete strategy
% 19.39/3.48 % (244654)------------------------------
% 19.39/3.48 % (244654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.48 % (244654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.48 % (244654)CaDiCaL version: 2.1.3
% 19.39/3.48 % (244654)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.48 % (244654)Time elapsed: 0.004 s
% 19.39/3.48 % (244654)Peak memory usage: 88 MB
% 19.39/3.48 % (244654)Instructions burned: 8 (million)
% 19.39/3.48 % (244574)------------------------------
% 19.39/3.48 % (244574)------------------------------
% 19.39/3.48 % (244665)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=616035813:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.39/3.48 % (244671)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2782534168:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 19.39/3.48 % (244654)------------------------------
% 19.39/3.48 % (244654)------------------------------
% 19.39/3.48 % (244665)Instruction limit reached!
% 19.39/3.48 % (244665)------------------------------
% 19.39/3.48 % (244665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.48 % (244665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.48 % (244665)CaDiCaL version: 2.1.3
% 19.39/3.48 % (244665)Termination reason: Instruction limit
% 19.39/3.48 % (244665)Termination phase: Saturation
% 19.39/3.48 % (244665)Time elapsed: 0.098 s
% 19.39/3.48 % (244665)Peak memory usage: 90 MB
% 19.39/3.48 % (244665)Instructions burned: 159 (million)
% 19.39/3.48 % (244690)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1738265614:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.39/3.48 % (244700)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=163891122:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 19.39/3.48 % (244700)Refutation not found, incomplete strategy
% 29.26/4.83 % (244700)------------------------------
% 29.26/4.83 % (244700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.83 % (244700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.83 % (244700)CaDiCaL version: 2.1.3
% 29.26/4.83 % (244700)Termination reason: Refutation not found, incomplete strategy
% 29.26/4.83 % (244700)Time elapsed: 0.001 s
% 29.26/4.83 % (244700)Peak memory usage: 87 MB
% 29.26/4.83 % (244690)Instruction limit reached!
% 29.26/4.83 % (244690)------------------------------
% 29.26/4.83 % (244690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.83 % (244690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.83 % (244690)CaDiCaL version: 2.1.3
% 29.26/4.83 % (244690)Termination reason: Instruction limit
% 29.26/4.83 % (244690)Termination phase: Saturation
% 29.26/4.83 % (244690)Time elapsed: 0.056 s
% 29.26/4.83 % (244690)Peak memory usage: 89 MB
% 29.26/4.83 % (244690)Instructions burned: 107 (million)
% 29.26/4.83 % (244713)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3987633422:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 29.26/4.84 % (244700)------------------------------
% 29.26/4.84 % (244700)------------------------------
% 29.26/4.84 % (244743)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=445255964:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 29.26/4.84 % (244713)Instruction limit reached!
% 29.26/4.84 % (244713)------------------------------
% 29.26/4.84 % (244713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.84 % (244713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.84 % (244713)CaDiCaL version: 2.1.3
% 29.26/4.84 % (244713)Termination reason: Instruction limit
% 29.26/4.84 % (244713)Termination phase: Saturation
% 29.26/4.84 % (244713)Time elapsed: 0.148 s
% 29.26/4.84 % (244713)Peak memory usage: 92 MB
% 29.26/4.84 % (244713)Instructions burned: 243 (million)
% 29.26/4.84 % (244745)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1362885068:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 29.26/4.84 % (244745)Refutation not found, incomplete strategy
% 29.26/4.84 % (244745)------------------------------
% 29.26/4.84 % (244745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.84 % (244745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.84 % (244745)CaDiCaL version: 2.1.3
% 29.26/4.84 % (244745)Termination reason: Refutation not found, incomplete strategy
% 29.26/4.84 % (244745)Time elapsed: 0.002 s
% 29.26/4.84 % (244745)Peak memory usage: 88 MB
% 29.26/4.84 % (244745)Instructions burned: 4 (million)
% 29.26/4.84 % (244747)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2639346481:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 29.26/4.84 % (244745)------------------------------
% 29.26/4.84 % (244745)------------------------------
% 29.26/4.84 % (244750)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3024246116:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 29.26/4.84 % (244750)Instruction limit reached!
% 29.26/4.84 % (244750)------------------------------
% 29.26/4.84 % (244750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.84 % (244750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.84 % (244750)CaDiCaL version: 2.1.3
% 29.26/4.84 % (244750)Termination reason: Instruction limit
% 29.26/4.84 % (244750)Termination phase: Saturation
% 29.26/4.84 % (244750)Time elapsed: 0.060 s
% 29.26/4.84 % (244750)Peak memory usage: 93 MB
% 29.26/4.84 % (244750)Instructions burned: 191 (million)
% 29.26/4.84 % (244747)Instruction limit reached!
% 29.26/4.84 % (244747)------------------------------
% 29.26/4.84 % (244747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.26/4.84 % (244747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.26/4.84 % (244747)CaDiCaL version: 2.1.3
% 29.26/4.84 % (244747)Termination reason: Instruction limit
% 29.26/4.84 % (244747)Termination phase: Saturation
% 29.26/4.84 % (244747)Time elapsed: 0.237 s
% 29.26/4.84 % (244747)Peak memory usage: 103 MB
% 29.26/4.84 % (244747)Instructions burned: 500 (million)
% 29.26/4.84 % (244752)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4020762388:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 52.50/8.09 % (244753)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3093533402:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 52.50/8.09 % (244752)Instruction limit reached!
% 52.50/8.09 % (244752)------------------------------
% 52.50/8.09 % (244752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244752)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244752)Termination reason: Instruction limit
% 52.50/8.09 % (244752)Termination phase: Saturation
% 52.50/8.09 % (244752)Time elapsed: 0.084 s
% 52.50/8.09 % (244752)Peak memory usage: 93 MB
% 52.50/8.09 % (244752)Instructions burned: 267 (million)
% 52.50/8.09 % (244753)Instruction limit reached!
% 52.50/8.09 % (244753)------------------------------
% 52.50/8.09 % (244753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244753)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244753)Termination reason: Instruction limit
% 52.50/8.09 % (244753)Termination phase: Saturation
% 52.50/8.09 % (244753)Time elapsed: 0.097 s
% 52.50/8.09 % (244753)Peak memory usage: 90 MB
% 52.50/8.09 % (244753)Instructions burned: 157 (million)
% 52.50/8.09 % (244756)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1234139308:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 52.50/8.09 % (244757)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=76761630:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 52.50/8.09 % (244757)Refutation not found, incomplete strategy
% 52.50/8.09 % (244757)------------------------------
% 52.50/8.09 % (244757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244757)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244757)Termination reason: Refutation not found, incomplete strategy
% 52.50/8.09 % (244757)Time elapsed: 0.024 s
% 52.50/8.09 % (244757)Peak memory usage: 87 MB
% 52.50/8.09 % (244757)Instructions burned: 44 (million)
% 52.50/8.09 % (244757)------------------------------
% 52.50/8.09 % (244757)------------------------------
% 52.50/8.09 % (244760)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4237595191:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 52.50/8.09 % (244760)Instruction limit reached!
% 52.50/8.09 % (244760)------------------------------
% 52.50/8.09 % (244760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244760)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244760)Termination reason: Instruction limit
% 52.50/8.09 % (244760)Termination phase: Saturation
% 52.50/8.09 % (244760)Time elapsed: 0.094 s
% 52.50/8.09 % (244760)Peak memory usage: 90 MB
% 52.50/8.09 % (244760)Instructions burned: 181 (million)
% 52.50/8.09 % (244762)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4052372349:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 52.50/8.09 % (244756)Instruction limit reached!
% 52.50/8.09 % (244756)------------------------------
% 52.50/8.09 % (244756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244756)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244756)Termination reason: Instruction limit
% 52.50/8.09 % (244756)Termination phase: Saturation
% 52.50/8.09 % (244756)Time elapsed: 0.989 s
% 52.50/8.09 % (244756)Peak memory usage: 156 MB
% 52.50/8.09 % (244756)Instructions burned: 3259 (million)
% 52.50/8.09 % (244671)Instruction limit reached!
% 52.50/8.09 % (244671)------------------------------
% 52.50/8.09 % (244671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.09 % (244671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.09 % (244671)CaDiCaL version: 2.1.3
% 52.50/8.09 % (244671)Termination reason: Instruction limit
% 52.50/8.09 % (244671)Termination phase: Saturation
% 52.50/8.09 % (244671)Time elapsed: 2.136 s
% 52.50/8.09 % (244671)Peak memory usage: 144 MB
% 67.75/10.20 % (244671)Instructions burned: 3396 (million)
% 67.75/10.20 % (244764)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1830780431:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 67.75/10.20 % (244765)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2737810894:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 67.75/10.20 % (244764)Instruction limit reached!
% 67.75/10.20 % (244764)------------------------------
% 67.75/10.20 % (244764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.75/10.20 % (244764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.75/10.20 % (244764)CaDiCaL version: 2.1.3
% 67.75/10.20 % (244764)Termination reason: Instruction limit
% 67.75/10.20 % (244764)Termination phase: Saturation
% 67.75/10.20 % (244764)Time elapsed: 0.134 s
% 67.75/10.20 % (244764)Peak memory usage: 93 MB
% 67.75/10.20 % (244764)Instructions burned: 414 (million)
% 67.75/10.20 % (244768)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1533355670:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 67.75/10.20 % (244768)Instruction limit reached!
% 67.75/10.20 % (244768)------------------------------
% 67.75/10.20 % (244768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.75/10.20 % (244768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.75/10.20 % (244768)CaDiCaL version: 2.1.3
% 67.75/10.20 % (244768)Termination reason: Instruction limit
% 67.75/10.20 % (244768)Termination phase: Saturation
% 67.75/10.20 % (244768)Time elapsed: 0.071 s
% 67.75/10.20 % (244768)Peak memory usage: 92 MB
% 67.75/10.20 % (244768)Instructions burned: 304 (million)
% 67.75/10.20 % (244770)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1963910355:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 67.75/10.20 % (244770)Instruction limit reached!
% 67.75/10.20 % (244770)------------------------------
% 67.75/10.20 % (244770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.75/10.20 % (244770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.75/10.20 % (244770)CaDiCaL version: 2.1.3
% 67.75/10.20 % (244770)Termination reason: Instruction limit
% 67.75/10.20 % (244770)Termination phase: Saturation
% 67.75/10.20 % (244770)Time elapsed: 0.236 s
% 67.75/10.20 % (244770)Peak memory usage: 105 MB
% 67.75/10.20 % (244770)Instructions burned: 720 (million)
% 67.75/10.20 % (244772)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1706529338:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 67.75/10.20 % (244772)Instruction limit reached!
% 67.75/10.20 % (244772)------------------------------
% 67.75/10.20 % (244772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.75/10.20 % (244772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.75/10.20 % (244772)CaDiCaL version: 2.1.3
% 67.75/10.20 % (244772)Termination reason: Instruction limit
% 67.75/10.20 % (244772)Termination phase: Saturation
% 67.75/10.20 % (244772)Time elapsed: 0.179 s
% 67.75/10.20 % (244772)Peak memory usage: 90 MB
% 67.75/10.20 % (244772)Instructions burned: 599 (million)
% 67.75/10.20 % (244743)Instruction limit reached!
% 67.75/10.20 % (244743)------------------------------
% 67.75/10.20 % (244743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.75/10.20 % (244743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.75/10.20 % (244743)CaDiCaL version: 2.1.3
% 67.75/10.20 % (244743)Termination reason: Instruction limit
% 67.75/10.20 % (244743)Termination phase: Saturation
% 67.75/10.20 % (244743)Time elapsed: 2.970 s
% 67.75/10.20 % (244743)Peak memory usage: 146 MB
% 67.75/10.20 % (244743)Instructions burned: 5208 (million)
% 67.75/10.20 % (244774)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2132924447:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 67.75/10.20 % (244775)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=4188300679:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 99.72/14.89 % (244774)Instruction limit reached!
% 99.72/14.89 % (244774)------------------------------
% 99.72/14.89 % (244774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.89 % (244774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.89 % (244774)CaDiCaL version: 2.1.3
% 99.72/14.89 % (244774)Termination reason: Instruction limit
% 99.72/14.89 % (244774)Termination phase: Saturation
% 99.72/14.89 % (244774)Time elapsed: 1.025 s
% 99.72/14.89 % (244774)Peak memory usage: 141 MB
% 99.72/14.89 % (244774)Instructions burned: 2990 (million)
% 99.72/14.89 % (244778)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3999095435:i=2088:bd=preordered:av=off_2949 on theBenchmark for (2949ds/2088Mi)
% 99.72/14.89 % (244775)Instruction limit reached!
% 99.72/14.89 % (244775)------------------------------
% 99.72/14.89 % (244775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.89 % (244775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.90 % (244775)CaDiCaL version: 2.1.3
% 99.72/14.90 % (244775)Termination reason: Instruction limit
% 99.72/14.90 % (244775)Termination phase: Saturation
% 99.72/14.90 % (244775)Time elapsed: 1.245 s
% 99.72/14.90 % (244775)Peak memory usage: 136 MB
% 99.72/14.90 % (244775)Instructions burned: 1997 (million)
% 99.72/14.90 % (244780)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1766573672:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi)
% 99.72/14.90 % (244778)Instruction limit reached!
% 99.72/14.90 % (244778)------------------------------
% 99.72/14.90 % (244778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.90 % (244778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.90 % (244778)CaDiCaL version: 2.1.3
% 99.72/14.90 % (244778)Termination reason: Instruction limit
% 99.72/14.90 % (244778)Termination phase: Saturation
% 99.72/14.90 % (244778)Time elapsed: 0.714 s
% 99.72/14.90 % (244778)Peak memory usage: 135 MB
% 99.72/14.90 % (244778)Instructions burned: 2089 (million)
% 99.72/14.90 % (244782)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3797996750:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi)
% 99.72/14.90 % (244780)Instruction limit reached!
% 99.72/14.90 % (244780)------------------------------
% 99.72/14.90 % (244780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.90 % (244780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.90 % (244780)CaDiCaL version: 2.1.3
% 99.72/14.90 % (244780)Termination reason: Instruction limit
% 99.72/14.90 % (244780)Termination phase: Saturation
% 99.72/14.90 % (244780)Time elapsed: 0.536 s
% 99.72/14.90 % (244780)Peak memory usage: 121 MB
% 99.72/14.90 % (244780)Instructions burned: 1098 (million)
% 99.72/14.90 % (244782)Instruction limit reached!
% 99.72/14.90 % (244782)------------------------------
% 99.72/14.90 % (244782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.90 % (244782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.90 % (244782)CaDiCaL version: 2.1.3
% 99.72/14.90 % (244782)Termination reason: Instruction limit
% 99.72/14.90 % (244782)Termination phase: Saturation
% 99.72/14.90 % (244782)Time elapsed: 0.134 s
% 99.72/14.90 % (244782)Peak memory usage: 99 MB
% 99.72/14.90 % (244782)Instructions burned: 435 (million)
% 99.72/14.90 % (244784)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3678588528:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2938 on theBenchmark for (2938ds/2942Mi)
% 99.72/14.90 % (244785)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1175474195:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2938 on theBenchmark for (2938ds/6922Mi)
% 99.72/14.90 % (244765)Instruction limit reached!
% 99.72/14.90 % (244765)------------------------------
% 99.72/14.90 % (244765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.72/14.90 % (244765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.72/14.90 % (244765)CaDiCaL version: 2.1.3
% 99.72/14.90 % (244765)Termination reason: Instruction limit
% 99.72/14.90 % (244765)Termination phase: Saturation
% 99.72/14.90 % (244765)Time elapsed: 4.436 s
% 99.72/14.90 % (244765)Peak memory usage: 226 MB
% 117.03/17.18 % (244765)Instructions burned: 8480 (million)
% 117.03/17.18 % (244788)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=983313607:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2925 on theBenchmark for (2925ds/596Mi)
% 117.03/17.18 % (244788)Refutation not found, incomplete strategy
% 117.03/17.18 % (244788)------------------------------
% 117.03/17.18 % (244788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.03/17.18 % (244788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.03/17.18 % (244788)CaDiCaL version: 2.1.3
% 117.03/17.18 % (244788)Termination reason: Refutation not found, incomplete strategy
% 117.03/17.18 % (244788)Time elapsed: 0.003 s
% 117.03/17.18 % (244788)Peak memory usage: 88 MB
% 117.03/17.18 % (244788)Instructions burned: 4 (million)
% 117.03/17.18 % (244788)------------------------------
% 117.03/17.18 % (244788)------------------------------
% 117.03/17.18 % (244799)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2932151733:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2921 on theBenchmark for (2921ds/4123Mi)
% 117.03/17.18 % (244784)Instruction limit reached!
% 117.03/17.18 % (244784)------------------------------
% 117.03/17.18 % (244784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.03/17.18 % (244784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.03/17.18 % (244784)CaDiCaL version: 2.1.3
% 117.03/17.18 % (244784)Termination reason: Instruction limit
% 117.03/17.18 % (244784)Termination phase: Saturation
% 117.03/17.18 % (244784)Time elapsed: 1.803 s
% 117.03/17.18 % (244784)Peak memory usage: 140 MB
% 117.03/17.18 % (244784)Instructions burned: 2943 (million)
% 117.03/17.18 % (244892)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3095378856:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2919 on theBenchmark for (2919ds/16411Mi)
% 117.03/17.18 % (244785)Instruction limit reached!
% 117.03/17.18 % (244785)------------------------------
% 117.03/17.18 % (244785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.03/17.18 % (244785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.03/17.18 % (244785)CaDiCaL version: 2.1.3
% 117.03/17.18 % (244785)Termination reason: Instruction limit
% 117.03/17.18 % (244785)Termination phase: Saturation
% 117.03/17.18 % (244785)Time elapsed: 1.969 s
% 117.03/17.18 % (244785)Peak memory usage: 198 MB
% 117.03/17.18 % (244785)Instructions burned: 6923 (million)
% 117.03/17.18 % (244926)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3546824753:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2917 on theBenchmark for (2917ds/1670Mi)
% 117.03/17.18 % (244926)Instruction limit reached!
% 117.03/17.18 % (244926)------------------------------
% 117.03/17.18 % (244926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.03/17.18 % (244926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.03/17.18 % (244926)CaDiCaL version: 2.1.3
% 117.03/17.18 % (244926)Termination reason: Instruction limit
% 117.03/17.18 % (244926)Termination phase: Saturation
% 117.03/17.18 % (244926)Time elapsed: 0.815 s
% 117.03/17.18 % (244926)Peak memory usage: 136 MB
% 117.03/17.18 % (244926)Instructions burned: 1671 (million)
% 117.03/17.18 % (244762)Instruction limit reached!
% 117.03/17.18 % (244762)------------------------------
% 117.03/17.18 % (244762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.03/17.18 % (244762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.03/17.18 % (244762)CaDiCaL version: 2.1.3
% 117.03/17.18 % (244762)Termination reason: Instruction limit
% 117.03/17.18 % (244762)Termination phase: Saturation
% 117.03/17.18 % (244762)Time elapsed: 6.790 s
% 117.03/17.18 % (244762)Peak memory usage: 191 MB
% 117.03/17.18 % (244762)Instructions burned: 10307 (million)
% 117.03/17.18 % (245110)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2356970662:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2907 on theBenchmark for (2907ds/1722Mi)
% 117.03/17.18 % (245163)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=29198128:cts=off:cond=on:i=9530:bs=on:fsd=on_2906 on theBenchmark for (2906ds/9530Mi)
% 131.16/19.20 % (244799)Instruction limit reached!
% 131.16/19.20 % (244799)------------------------------
% 131.16/19.20 % (244799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (244799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (244799)CaDiCaL version: 2.1.3
% 131.16/19.20 % (244799)Termination reason: Instruction limit
% 131.16/19.20 % (244799)Termination phase: Saturation
% 131.16/19.20 % (244799)Time elapsed: 2.233 s
% 131.16/19.20 % (244799)Peak memory usage: 176 MB
% 131.16/19.20 % (244799)Instructions burned: 4123 (million)
% 131.16/19.20 % (245223)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=692748229:st=2:i=4495:sd=10:ss=included_2897 on theBenchmark for (2897ds/4495Mi)
% 131.16/19.20 % (245110)Instruction limit reached!
% 131.16/19.20 % (245110)------------------------------
% 131.16/19.20 % (245110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (245110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (245110)CaDiCaL version: 2.1.3
% 131.16/19.20 % (245110)Termination reason: Instruction limit
% 131.16/19.20 % (245110)Termination phase: Saturation
% 131.16/19.20 % (245110)Time elapsed: 1.113 s
% 131.16/19.20 % (245110)Peak memory usage: 136 MB
% 131.16/19.20 % (245110)Instructions burned: 1722 (million)
% 131.16/19.20 % (245225)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=297423208:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 131.16/19.20 % (245223)Instruction limit reached!
% 131.16/19.20 % (245223)------------------------------
% 131.16/19.20 % (245223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (245223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (245223)CaDiCaL version: 2.1.3
% 131.16/19.20 % (245223)Termination reason: Instruction limit
% 131.16/19.20 % (245223)Termination phase: Saturation
% 131.16/19.20 % (245223)Time elapsed: 2.657 s
% 131.16/19.20 % (245223)Peak memory usage: 147 MB
% 131.16/19.20 % (245223)Instructions burned: 4496 (million)
% 131.16/19.20 % (245227)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=4062574453:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2869 on theBenchmark for (2869ds/2083Mi)
% 131.16/19.20 % (245225)Instruction limit reached!
% 131.16/19.20 % (245225)------------------------------
% 131.16/19.20 % (245225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (245225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (245225)CaDiCaL version: 2.1.3
% 131.16/19.20 % (245225)Termination reason: Instruction limit
% 131.16/19.20 % (245225)Termination phase: Saturation
% 131.16/19.20 % (245225)Time elapsed: 2.806 s
% 131.16/19.20 % (245225)Peak memory usage: 157 MB
% 131.16/19.20 % (245225)Instructions burned: 4920 (million)
% 131.16/19.20 % (245229)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1421898267:i=4629:av=off:gsp=on_2865 on theBenchmark for (2865ds/4629Mi)
% 131.16/19.20 % (244892)Instruction limit reached!
% 131.16/19.20 % (244892)------------------------------
% 131.16/19.20 % (244892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (244892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (244892)CaDiCaL version: 2.1.3
% 131.16/19.20 % (244892)Termination reason: Instruction limit
% 131.16/19.20 % (244892)Termination phase: Saturation
% 131.16/19.20 % (244892)Time elapsed: 5.720 s
% 131.16/19.20 % (244892)Peak memory usage: 307 MB
% 131.16/19.20 % (244892)Instructions burned: 16413 (million)
% 131.16/19.20 % (245231)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1351558225:i=1258:av=off_2860 on theBenchmark for (2860ds/1258Mi)
% 131.16/19.20 % (245229)Refutation not found, incomplete strategy
% 131.16/19.20 % (245229)------------------------------
% 131.16/19.20 % (245229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.16/19.20 % (245229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.16/19.20 % (245229)CaDiCaL version: 2.1.3
% 131.16/19.20 % (245229)Termination reason: Refutation not found, incomplete strategy
% 131.16/19.20 % (245229)Time elapsed: 0.594 s
% 131.16/19.20 % (245229)Peak memory usage: 128 MB
% 121.96/21.04 % (245229)Instructions burned: 899 (million)
% 121.96/21.04 % (245231)Instruction limit reached!
% 121.96/21.04 % (245231)------------------------------
% 121.96/21.04 % (245231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245231)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245231)Termination reason: Instruction limit
% 121.96/21.04 % (245231)Termination phase: Saturation
% 121.96/21.04 % (245231)Time elapsed: 0.361 s
% 121.96/21.04 % (245231)Peak memory usage: 136 MB
% 121.96/21.04 % (245231)Instructions burned: 1261 (million)
% 121.96/21.04 % (245227)Instruction limit reached!
% 121.96/21.04 % (245227)------------------------------
% 121.96/21.04 % (245227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245227)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245227)Termination reason: Instruction limit
% 121.96/21.04 % (245227)Termination phase: Saturation
% 121.96/21.04 % (245227)Time elapsed: 1.226 s
% 121.96/21.04 % (245227)Peak memory usage: 139 MB
% 121.96/21.04 % (245227)Instructions burned: 2085 (million)
% 121.96/21.04 % (245229)------------------------------
% 121.96/21.04 % (245229)------------------------------
% 121.96/21.04 % (245233)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2741126298:i=7343:av=off:ss=included_2855 on theBenchmark for (2855ds/7343Mi)
% 121.96/21.04 % (245234)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1392610358:i=1325:sd=2:ss=axioms:sgt=16_2855 on theBenchmark for (2855ds/1325Mi)
% 121.96/21.04 % (245234)Refutation not found, incomplete strategy
% 121.96/21.04 % (245234)------------------------------
% 121.96/21.04 % (245234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245234)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245234)Termination reason: Refutation not found, incomplete strategy
% 121.96/21.04 % (245234)Time elapsed: 0.001 s
% 121.96/21.04 % (245234)Peak memory usage: 88 MB
% 121.96/21.04 % (245234)Instructions burned: 1 (million)
% 121.96/21.04 % (245235)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=907821222:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2855 on theBenchmark for (2855ds/2646Mi)
% 121.96/21.04 % (245234)------------------------------
% 121.96/21.04 % (245234)------------------------------
% 121.96/21.04 % (245239)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2089843498:i=1489:sd=2:ep=R:ss=axioms_2851 on theBenchmark for (2851ds/1489Mi)
% 121.96/21.04 % (245239)Refutation not found, incomplete strategy
% 121.96/21.04 % (245239)------------------------------
% 121.96/21.04 % (245239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245239)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245239)Termination reason: Refutation not found, incomplete strategy
% 121.96/21.04 % (245239)Time elapsed: 0.585 s
% 121.96/21.04 % (245239)Peak memory usage: 128 MB
% 121.96/21.04 % (245239)Instructions burned: 894 (million)
% 121.96/21.04 % (245163)Instruction limit reached!
% 121.96/21.04 % (245163)------------------------------
% 121.96/21.04 % (245163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245163)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245163)Termination reason: Instruction limit
% 121.96/21.04 % (245163)Termination phase: Saturation
% 121.96/21.04 % (245163)Time elapsed: 6.203 s
% 121.96/21.04 % (245163)Peak memory usage: 175 MB
% 121.96/21.04 % (245163)Instructions burned: 9531 (million)
% 121.96/21.04 % (245239)------------------------------
% 121.96/21.04 % (245239)------------------------------
% 121.96/21.04 % (245241)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2042382620:i=1503_2842 on theBenchmark for (2842ds/1503Mi)
% 121.96/21.04 % (245242)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3619630518:i=13942:kws=frequency_2841 on theBenchmark for (2841ds/13942Mi)
% 121.96/21.04 % (245235)Instruction limit reached!
% 121.96/21.04 % (245235)------------------------------
% 121.96/21.04 % (245235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245235)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245235)Termination reason: Instruction limit
% 121.96/21.04 % (245235)Termination phase: Saturation
% 121.96/21.04 % (245235)Time elapsed: 1.869 s
% 121.96/21.04 % (245235)Peak memory usage: 144 MB
% 121.96/21.04 % (245235)Instructions burned: 2647 (million)
% 121.96/21.04 % (245245)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=146483859:i=3604:fsr=off:er=filter_2834 on theBenchmark for (2834ds/3604Mi)
% 121.96/21.04 % (245233)Instruction limit reached!
% 121.96/21.04 % (245233)------------------------------
% 121.96/21.04 % (245233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245233)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245233)Termination reason: Instruction limit
% 121.96/21.04 % (245233)Termination phase: Saturation
% 121.96/21.04 % (245233)Time elapsed: 2.222 s
% 121.96/21.04 % (245233)Peak memory usage: 200 MB
% 121.96/21.04 % (245233)Instructions burned: 7346 (million)
% 121.96/21.04 % (245241)Instruction limit reached!
% 121.96/21.04 % (245241)------------------------------
% 121.96/21.04 % (245241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245241)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245241)Termination reason: Instruction limit
% 121.96/21.04 % (245241)Termination phase: Saturation
% 121.96/21.04 % (245241)Time elapsed: 0.951 s
% 121.96/21.04 % (245241)Peak memory usage: 133 MB
% 121.96/21.04 % (245241)Instructions burned: 1504 (million)
% 121.96/21.04 % (245247)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=241565717:i=1876:sd=1:ss=included:sgt=32_2832 on theBenchmark for (2832ds/1876Mi)
% 121.96/21.04 % (245248)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2044713540:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2831 on theBenchmark for (2831ds/1932Mi)
% 121.96/21.04 % (245247)Instruction limit reached!
% 121.96/21.04 % (245247)------------------------------
% 121.96/21.04 % (245247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245247)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245247)Termination reason: Instruction limit
% 121.96/21.04 % (245247)Termination phase: Saturation
% 121.96/21.04 % (245247)Time elapsed: 0.644 s
% 121.96/21.04 % (245247)Peak memory usage: 135 MB
% 121.96/21.04 % (245247)Instructions burned: 1876 (million)
% 121.96/21.04 % (245248)Refutation not found, incomplete strategy
% 121.96/21.04 % (245248)------------------------------
% 121.96/21.04 % (245248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245248)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245248)Termination reason: Refutation not found, incomplete strategy
% 121.96/21.04 % (245248)Time elapsed: 0.589 s
% 121.96/21.04 % (245248)Peak memory usage: 127 MB
% 121.96/21.04 % (245248)Instructions burned: 897 (million)
% 121.96/21.04 % (245251)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2289573973:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2824 on theBenchmark for (2824ds/1980Mi)
% 121.96/21.04 % (245248)------------------------------
% 121.96/21.04 % (245248)------------------------------
% 121.96/21.04 % (245253)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1413024232:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2821 on theBenchmark for (2821ds/3902Mi)
% 121.96/21.04 % (245251)Instruction limit reached!
% 121.96/21.04 % (245251)------------------------------
% 121.96/21.04 % (245251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245251)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245251)Termination reason: Instruction limit
% 121.96/21.04 % (245251)Termination phase: Saturation
% 121.96/21.04 % (245251)Time elapsed: 0.831 s
% 121.96/21.04 % (245251)Peak memory usage: 134 MB
% 121.96/21.04 % (245251)Instructions burned: 1982 (million)
% 121.96/21.04 % (245245)Instruction limit reached!
% 121.96/21.04 % (245245)------------------------------
% 121.96/21.04 % (245245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245245)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245245)Termination reason: Instruction limit
% 121.96/21.04 % (245245)Termination phase: Saturation
% 121.96/21.04 % (245245)Time elapsed: 1.938 s
% 121.96/21.04 % (245245)Peak memory usage: 163 MB
% 121.96/21.04 % (245245)Instructions burned: 3606 (million)
% 121.96/21.04 % (245255)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1438676418:avsq=on:i=3916:aac=none:amm=off_2814 on theBenchmark for (2814ds/3916Mi)
% 121.96/21.04 % (245256)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3446411454:cond=on:i=3940:av=off:er=known_2813 on theBenchmark for (2813ds/3940Mi)
% 121.96/21.04 % (245253)Instruction limit reached!
% 121.96/21.04 % (245253)------------------------------
% 121.96/21.04 % (245253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.96/21.04 % (245253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.96/21.04 % (245253)CaDiCaL version: 2.1.3
% 121.96/21.04 % (245253)Termination reason: Instruction limit
% 121.96/21.04 % (245253)Termination phase: Saturation
% 121.96/21.04 % (245253)Time elapsed: 1.574 s
% 121.96/21.04 % (245253)Peak memory usage: 156 MB
% 121.96/21.04 % (245253)Instructions burned: 3904 (million)
% 121.96/21.04 % (245259)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1100427665:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2803 on theBenchmark for (2803ds/3980Mi)
% 121.96/21.04 % (245259)First to succeed.
% 121.96/21.04 % (245259)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-244410"
% 121.96/21.04 % SZS status Satisfiable for theBenchmark
% 121.96/21.04 % SZS output start Saturation.
% See solution above
% 0.21/21.14 % SZS output start Definitions and Model Updates.
% 0.21/21.14 for all groundings,
% 0.21/21.14 whenever intruder_message(X0) | ~intruder_holds(key(X0,X1)) | ~intruder_message(encrypt(X2,X0)) | ~party_of_protocol(X1) is false, set ~intruder_holds(key(X0,X1)) to true
% 0.21/21.14 % SZS output end Definitions and Model Updates.
% 0.21/21.14 % (245259)------------------------------
% 0.21/21.14 % (245259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/21.14 % (245259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/21.14 % (245259)CaDiCaL version: 2.1.3
% 0.21/21.14 % (245259)Termination reason: Satisfiable
% 0.21/21.14 % (245259)Time elapsed: 0.392 s
% 0.21/21.14 % (245259)Peak memory usage: 130 MB
% 0.21/21.14 % (245259)Instructions burned: 1072 (million)
% 0.21/21.14 % (245259)------------------------------
% 0.21/21.14 % (245259)------------------------------
% 0.21/21.14 % (244410)Success in time 20.357 s
% 0.21/21.14 % Vampire exiting
%------------------------------------------------------------------------------