Vampire---5.0.1.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWV743_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 01:19:23 PM UTC 2026

% Result   : CounterSatisfiable 5.68s 1.13s
% Output   : Saturation 5.94s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u576,negated_conjecture,
    ~ member(msg,key(aa(agent1,nat,shrK,a)),analz(knows(spy,evs))) ).

cnf(u669,negated_conjecture,
    ~ member(nat,k,symKeys) ).

cnf(u725,negated_conjecture,
    ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,evs)) ).

cnf(u1179,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | member(msg,X1,analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0)) ) ).

cnf(u263,axiom,
    agent(X1) != key(X0) ).

cnf(u1182,axiom,
    ( ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X16,X17),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X3 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u702,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool))))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared) ) ).

cnf(u1009,axiom,
    ( ~ member(event,says(X3,X1,crypt(X4,nonce(X8))),set(event,cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0)))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X2),mPair(nonce(X8),key(X4)))),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared) ) ).

cnf(u340,axiom,
    ( ~ member(msg,crypt(X2,X1),analz(X0))
    | ~ member(msg,key(X2),analz(X0))
    | ~ member(nat,X2,symKeys)
    | member(msg,X1,analz(X0)) ) ).

cnf(u877,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X4,mPair(agent(X5),mPair(key(X6),X7)))),knows(spy,X2))
    | member(agent1,X3,bad)
    | member(msg,mPair(X4,mPair(agent(X5),mPair(key(X6),X7))),parts(knows(server,cons(event,gets(X0,X1),X2))))
    | ~ member(list(event),cons(event,gets(X0,X1),X2),nS_Sha254967238shared) ) ).

cnf(u853,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),mPair(X3,mPair(agent(X1),mPair(key(X4),X5)))),parts(knows(spy,X6)))
    | member(agent1,X2,bad)
    | X0 = X1
    | member(agent1,X7,bad)
    | ~ member(list(event),X6,nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X0),mPair(key(X4),X9)))),knows(spy,X6)) ) ).

cnf(u682,axiom,
    ( ~ member(list(event),cons(event,gets(X4,X5),cons(event,gets(X2,X3),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,key(aa(agent1,nat,shrK,X1)),parts(knows(spy,X0))) ) ).

cnf(u809,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0))) ) ).

cnf(u1164,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared)
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0)))))) ) ).

cnf(u1155,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared)
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0)))))) ) ).

cnf(u1234,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X13),mPair(X14,mPair(agent(X8),mPair(key(X4),X15)))),knows(spy,X0))
    | X3 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X13,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u1158,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X14),mPair(key(X4),X15)))),knows(spy,X0)) ) ).

cnf(u833,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5 ) ).

cnf(u907,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),knows(spy,X0)) ) ).

cnf(u1083,negated_conjecture,
    ( member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u751,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u1129,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4)))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | member(msg,mPair(agent(X6),mPair(key(X7),X8)),analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4))))) ) ).

cnf(u579,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X0)),analz(X1))
    | member(msg,X2,analz(X1))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X0),X2),X1) ) ).

cnf(u503,axiom,
    ( ~ member(list(event),cons(event,gets(X2,X3),X0),nS_Sha254967238shared)
    | ~ member(agent1,X1,bad)
    | member(msg,key(aa(agent1,nat,shrK,X1)),parts(knows(spy,X0))) ) ).

cnf(u1154,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X8,mPair(agent(X5),mPair(key(X6),X7)))),knows(spy,X4))
    | member(msg,mPair(agent(X5),mPair(key(X6),X7)),analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u996,axiom,
    ( ~ member(event,says(X1,server,mPair(agent(X1),mPair(agent(X3),nonce(X2)))),set(event,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))
    | server = X1
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(list(event),cons(event,says(X1,X3,X5),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u1153,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X14,mPair(agent(X8),mPair(key(X4),X15)))),knows(spy,X0)) ) ).

cnf(u1109,negated_conjecture,
    ( member(msg,agent(a),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u1300,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X16,mPair(agent(X8),mPair(key(X4),X17)))),knows(spy,X0)) ) ).

cnf(u1259,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X16,mPair(agent(X17),mPair(key(X4),X8)))),knows(spy,X0)) ) ).

cnf(u1082,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u703,axiom,
    ( ~ member(msg,key(sK1(X0)),X0)
    | ~ member(nat,sK1(X0),symKeys)
    | member(msg,sK0(X0),analz(X0))
    | analz(X0) = X0
    | member(msg,sK2(X0),analz(X0)) ) ).

cnf(u540,negated_conjecture,
    member(msg,mPair(key(k),agent(a)),parts(knows(spy,evs))) ).

cnf(u976,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X9,mPair(agent(X10),mPair(key(X4),X11)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X1 = X8
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X8,bad) ) ).

cnf(u336,axiom,
    member(msg,key(aa(agent1,nat,shrK,X0)),initState(X0)) ).

cnf(u1068,negated_conjecture,
    ( member(msg,agent(b),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u693,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X3,mPair(agent(X4),mPair(key(X5),X2)))),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(msg,X2,parts(knows(spy,X1)))
    | member(agent1,X0,bad) ) ).

cnf(u880,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | server = X1
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(event,says(X1,server,mPair(agent(X1),mPair(agent(X3),nonce(X2)))),set(event,cons(event,gets(X6,X7),X0)))
    | member(list(event),cons(event,says(X1,X3,X5),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u1011,negated_conjecture,
    ( ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | member(msg,key(k),analz(knows(server,cons(event,gets(X0,X1),evs)))) ) ).

cnf(u330,axiom,
    member(msg,key(aa(agent1,nat,publicKey(X2),X1)),analz(knows(spy,X0))) ).

cnf(u896,negated_conjecture,
    ( member(msg,agent(b),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u332,axiom,
    ( gets(X3,X2) != gets(X1,X0)
    | X0 = X2 ) ).

cnf(u835,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u288,axiom,
    ( aa(agent1,nat,shrK,X1) != aa(agent1,nat,shrK,X0)
    | X0 = X1 ) ).

cnf(u326,axiom,
    member(msg,key(aa(agent1,nat,publicKey(X2),X1)),initState(X0)) ).

cnf(u948,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X4,mPair(agent(X5),mPair(key(X6),X7)))),knows(spy,X2))
    | ~ member(list(event),cons(event,gets(X0,X1),X2),nS_Sha254967238shared)
    | member(agent1,X3,bad)
    | member(msg,mPair(X4,mPair(agent(X5),mPair(key(X6),X7))),analz(knows(server,cons(event,gets(X0,X1),X2))))
    | ~ member(msg,key(aa(agent1,nat,shrK,X3)),knows(server,cons(event,gets(X0,X1),X2))) ) ).

cnf(u216,axiom,
    ( ~ member(event,says(server,X6,crypt(X5,mPair(X4,mPair(agent(X3),mPair(key(X2),X1))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | ~ member(nat,X2,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u516,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X1)),analz(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X2,X3),X0),nS_Sha254967238shared) ) ).

cnf(u440,negated_conjecture,
    member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),parts(knows(server,evs))) ).

cnf(u635,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X0),mPair(key(k),X3)))),parts(knows(spy,evs)))
    | member(agent1,X1,bad)
    | b = X0 ) ).

cnf(u959,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),analz(knows(spy,X0))) ) ).

cnf(u284,axiom,
    ( ~ member(msg,mPair(X2,X1),parts(X0))
    | member(msg,X1,parts(X0)) ) ).

cnf(u464,negated_conjecture,
    member(msg,key(k),parts(knows(server,evs))) ).

cnf(u278,axiom,
    mPair(X2,X1) != key(X0) ).

cnf(u983,negated_conjecture,
    ( member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs))) ) ).

cnf(u436,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,a),mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))))),knows(server,evs)) ).

cnf(u631,axiom,
    ( ~ member(event,says(server,X1,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | X3 = X6
    | member(agent1,X7,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X6),mPair(key(X4),X9)))),parts(knows(spy,X0))) ) ).

cnf(u232,axiom,
    ( says(X5,X4,X3) != says(X2,X1,X0)
    | X2 = X5 ) ).

cnf(u397,axiom,
    ( ~ member(msg,mPair(X2,X0),X1)
    | member(msg,X0,analz(X1)) ) ).

cnf(u783,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X1),mPair(key(X5),X9)))),parts(knows(spy,X0)))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X4,mPair(agent(X2),mPair(key(X5),X6)))),parts(knows(spy,X0)))
    | member(agent1,X7,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared) ) ).

cnf(u928,negated_conjecture,
    ( member(msg,mPair(key(k),agent(a)),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u353,axiom,
    ( member(nat,aa(agent1,nat,publicKey(X3),X2),image(agent1,nat,publicKey(X3),X0))
    | ~ member(agent1,X2,X0) ) ).

cnf(u1139,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4)))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | member(msg,mPair(agent(X6),mPair(key(X7),X8)),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4))))) ) ).

cnf(u868,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X2),mPair(nonce(X8),key(X4)))),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | ~ member(event,says(X3,X1,crypt(X4,nonce(X8))),set(event,cons(event,gets(X6,X7),X0))) ) ).

cnf(u985,negated_conjecture,
    ( ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | member(msg,na,analz(knows(server,cons(event,gets(X0,X1),evs)))) ) ).

cnf(u228,axiom,
    ( ~ member(event,says(X7,X6,crypt(X5,mPair(X4,mPair(X3,mPair(X2,X1))))),set(event,X0))
    | member(msg,X1,parts(knows(spy,X0))) ) ).

cnf(u1141,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared)
    | member(msg,X1,analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0)))))) ) ).

cnf(u219,axiom,
    ( ~ member(event,says(server,X9,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X7),mPair(key(X6),X5))))),set(event,X4))
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | ~ member(event,says(server,X3,crypt(aa(agent1,nat,shrK,X3),mPair(X2,mPair(agent(X1),mPair(key(X6),X0))))),set(event,X4))
    | X1 = X7 ) ).

cnf(u862,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(msg,key(X4),parts(knows(spy,X0))) ) ).

cnf(u505,negated_conjecture,
    member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),parts(knows(spy,evs))) ).

cnf(u501,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X1)),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X2,X3),X0),nS_Sha254967238shared) ) ).

cnf(u1298,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X16,mPair(agent(X17),mPair(key(X4),X8)))),knows(spy,X0)) ) ).

cnf(u299,axiom,
    ( ~ member(nat,aa(agent1,nat,publicKey(X3),X2),image(agent1,nat,publicKey(X1),X0))
    | X1 = X3 ) ).

cnf(u653,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X2,mPair(agent(X1),mPair(key(k),X3)))),knows(spy,evs))
    | b = X1
    | member(agent1,X0,bad) ) ).

cnf(u610,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),analz(knows(spy,X0))) ) ).

cnf(u961,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),knows(spy,X0))
    | X5 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u301,axiom,
    ( ~ member(nat,aa(agent1,nat,shrK,X1),image(agent1,nat,shrK,X0))
    | member(agent1,X1,X0) ) ).

cnf(u838,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u295,axiom,
    parts(X0) = parts(parts(X0)) ).

cnf(u325,axiom,
    member(msg,key(aa(agent1,nat,publicKey(X2),X1)),knows(spy,X0)) ).

cnf(u794,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X5),mPair(agent(X0),mPair(key(X2),X6)))),knows(spy,X4))
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X5),mPair(nonce(X3),key(X2)))),X4),nS_Sha254967238shared)
    | ~ member(event,says(X0,X1,crypt(X2,nonce(X3))),set(event,X4)) ) ).

cnf(u606,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0))) ) ).

cnf(u1235,negated_conjecture,
    ( member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u1037,negated_conjecture,
    ( ~ member(msg,key(aa(agent1,nat,shrK,b)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | member(msg,mPair(key(k),agent(a)),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u1095,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u275,axiom,
    ( crypt(X3,X2) != crypt(X1,X0)
    | X1 = X3 ) ).

cnf(u856,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(msg,key(X4),parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u1209,axiom,
    ( member(msg,mPair(X5,mPair(agent(X6),mPair(key(X7),X8))),analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),knows(spy,X4)) ) ).

cnf(u1196,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0))))))) ) ).

cnf(u333,axiom,
    ( gets(X3,X2) != gets(X1,X0)
    | X1 = X3 ) ).

cnf(u909,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X5,mPair(agent(X1),mPair(key(X6),X7)))),knows(spy,X4))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X8,mPair(agent(X2),mPair(key(X6),X9)))),knows(spy,X4)) ) ).

cnf(u1040,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X12,mPair(agent(X8),mPair(key(X4),X13)))),knows(spy,X0)) ) ).

cnf(u910,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),knows(spy,X0)) ) ).

cnf(u865,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X9,mPair(agent(X10),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X1 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X8,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u655,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(nonce(X2),mPair(agent(X1),mPair(key(X5),X4)))),parts(knows(spy,X3)))
    | member(list(event),cons(event,says(X0,X1,X4),X3),nS_Sha254967238shared)
    | server = X0
    | ~ member(list(event),X3,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | ~ member(event,says(X0,server,mPair(agent(X0),mPair(agent(X1),nonce(X2)))),set(event,X3)) ) ).

cnf(u1199,negated_conjecture,
    ( member(msg,na,parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u937,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5 ) ).

cnf(u1186,axiom,
    ( ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X16,X17),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X2 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u1142,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0))
    | member(msg,X1,analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))))))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared) ) ).

cnf(u817,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u600,axiom,
    ( member(msg,sK3(X0),parts(X0))
    | member(msg,sK0(X0),parts(X0))
    | analz(X0) = X0 ) ).

cnf(u221,axiom,
    ( ~ member(event,says(server,X9,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X7),mPair(key(X6),X5))))),set(event,X4))
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | ~ member(event,says(server,X3,crypt(aa(agent1,nat,shrK,X3),mPair(X2,mPair(agent(X1),mPair(key(X6),X0))))),set(event,X4))
    | X3 = X9 ) ).

cnf(u984,negated_conjecture,
    ( member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u208,axiom,
    member(agent1,spy,bad) ).

cnf(u1144,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u956,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u215,axiom,
    ( ~ member(event,says(server,X6,crypt(X5,mPair(X4,mPair(agent(X3),mPair(key(X2),X1))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X2),agent(X6))) = X1 ) ).

cnf(u202,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X5),mPair(X4,mPair(agent(X3),mPair(key(X2),X1)))),parts(knows(spy,X0)))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(agent1,X5,bad)
    | ~ member(nat,X2,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u1138,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4)))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4))))) ) ).

cnf(u201,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X5),mPair(X4,mPair(agent(X3),mPair(key(X2),X1)))),parts(knows(spy,X0)))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(agent1,X5,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X2),agent(X5))) = X1 ) ).

cnf(u204,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X0)),parts(knows(spy,X1)))
    | member(agent1,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u911,negated_conjecture,
    ( member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u195,hypothesis,
    ~ member(agent1,a,bad) ).

cnf(u1289,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0)) ) ).

cnf(u867,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u198,negated_conjecture,
    member(msg,key(k),analz(knows(spy,evs))) ).

cnf(u197,hypothesis,
    member(list(event),evs,nS_Sha254967238shared) ).

cnf(u583,negated_conjecture,
    ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(spy,evs)) ).

cnf(u314,axiom,
    ( nonce(X1) != nonce(X0)
    | X0 = X1 ) ).

cnf(u477,negated_conjecture,
    member(msg,agent(a),parts(knows(server,evs))) ).

cnf(u316,axiom,
    pp(fTrue) ).

cnf(u310,axiom,
    mPair(X1,X0) != nonce(X2) ).

cnf(u533,axiom,
    ( member(msg,crypt(sK1(X0),sK0(X0)),X0)
    | analz(X0) = X0
    | member(msg,sK3(X0),parts(X0)) ) ).

cnf(u535,axiom,
    ( member(msg,crypt(sK1(X0),sK0(X0)),X0)
    | analz(X0) = X0
    | member(msg,sK3(X0),analz(X0)) ) ).

cnf(u271,axiom,
    mPair(X3,X2) != crypt(X1,X0) ).

cnf(u296,axiom,
    ~ member(nat,aa(agent1,nat,publicKey(X2),X1),image(agent1,nat,shrK,X0)) ).

cnf(u429,axiom,
    member(msg,key(aa(agent1,nat,publicKey(X0),X1)),parts(knows(spy,X2))) ).

cnf(u770,axiom,
    ( ~ member(list(event),cons(event,gets(X4,X5),cons(event,gets(X2,X3),X0)),nS_Sha254967238shared)
    | ~ member(msg,key(aa(agent1,nat,shrK,X1)),knows(spy,X0))
    | member(agent1,X1,bad) ) ).

cnf(u451,negated_conjecture,
    member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),parts(knows(server,evs))) ).

cnf(u815,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u257,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),X1),analz(X0))
    | ~ member(msg,key(aa(agent1,nat,shrK,X2)),analz(X0))
    | member(msg,X1,analz(X0)) ) ).

cnf(u966,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),knows(spy,X0))
    | X3 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u290,axiom,
    ( aa(X1,X0,X3,sK4(X0,X1,X2,X3)) != aa(X1,X0,X2,sK4(X0,X1,X2,X3))
    | X2 = X3 ) ).

cnf(u922,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X1,mPair(agent(X5),mPair(key(X6),X7)))),knows(spy,X4))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X2,mPair(agent(X8),mPair(key(X6),X9)))),knows(spy,X4)) ) ).

cnf(u292,axiom,
    ( ~ pp(aa(X0,bool,X1,X2))
    | member(X0,X2,X1) ) ).

cnf(u613,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(server,X0)) ) ).

cnf(u894,axiom,
    ( ~ member(event,says(X1,server,mPair(agent(X1),mPair(agent(X3),nonce(X2)))),set(event,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))
    | member(list(event),cons(event,says(X1,X3,X5),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | server = X1
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u1216,axiom,
    ( member(msg,mPair(X5,mPair(agent(X6),mPair(key(X7),X8))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),knows(spy,X4))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u795,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(event,says(X3,X1,crypt(X4,nonce(X8))),set(event,cons(event,gets(X6,X7),X0)))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X2),mPair(nonce(X8),key(X4)))),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u690,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X2,mPair(agent(X3),mPair(key(k),X1)))),knows(spy,evs))
    | crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))) = X1
    | member(agent1,X0,bad) ) ).

cnf(u286,axiom,
    ( mPair(X3,X2) != mPair(X1,X0)
    | X1 = X3 ) ).

cnf(u534,axiom,
    ( member(msg,crypt(sK1(X0),sK0(X0)),X0)
    | analz(X0) = X0
    | member(msg,sK2(X0),parts(X0)) ) ).

cnf(u1163,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X8,mPair(agent(X5),mPair(key(X6),X7)))),knows(spy,X4))
    | member(msg,mPair(agent(X5),mPair(key(X6),X7)),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u1296,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0))))))) ) ).

cnf(u375,axiom,
    ~ member(msg,nonce(X0),initState(X1)) ).

cnf(u874,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X4,mPair(agent(X5),mPair(key(X6),X7)))),parts(knows(spy,X3)))
    | ~ member(list(event),cons(event,gets(X1,X2),X3),nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | member(msg,mPair(X4,mPair(agent(X5),mPair(key(X6),X7))),parts(knows(server,cons(event,gets(X1,X2),X3)))) ) ).

cnf(u1165,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0))
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))))))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared) ) ).

cnf(u1124,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X12,mPair(agent(X8),mPair(key(X4),X13)))),knows(spy,X0))
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u1162,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X8,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X1 = X8
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X13,mPair(agent(X14),mPair(key(X4),X15)))),knows(spy,X0)) ) ).

cnf(u793,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),mPair(X3,mPair(agent(X4),mPair(key(X5),X6)))),parts(knows(spy,X0)))
    | X1 = X2
    | member(agent1,X2,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X7,mPair(agent(X8),mPair(key(X5),X9)))),parts(knows(spy,X0))) ) ).

cnf(u638,axiom,
    ( ~ member(event,says(server,X1,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | X2 = X6
    | member(agent1,X7,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X6,mPair(agent(X8),mPair(key(X4),X9)))),parts(knows(spy,X0))) ) ).

cnf(u313,axiom,
    ~ member(msg,nonce(X1),parts(initState(X0))) ).

cnf(u1120,axiom,
    ( member(msg,mPair(X5,mPair(agent(X6),mPair(key(X7),X8))),analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4))) ) ).

cnf(u1302,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X16),mPair(key(X4),X17)))),knows(spy,X0)) ) ).

cnf(u1067,negated_conjecture,
    ( member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u735,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u822,axiom,
    ( member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(server,cons(event,gets(X6,X7),X0)))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad) ) ).

cnf(u1272,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X16,mPair(agent(X8),mPair(key(X4),X17)))),knows(spy,X0)) ) ).

cnf(u1304,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X14,bad)
    | X1 = X14
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X14),mPair(X15,mPair(agent(X16),mPair(key(X4),X17)))),knows(spy,X0))
    | member(agent1,X1,bad) ) ).

cnf(u1100,negated_conjecture,
    ( member(msg,mPair(key(k),agent(a)),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u912,negated_conjecture,
    ( member(msg,key(k),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u490,negated_conjecture,
    member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),parts(knows(spy,evs))) ).

cnf(u452,negated_conjecture,
    member(msg,agent(b),parts(knows(server,evs))) ).

cnf(u1193,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | member(msg,X1,parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0))))))) ) ).

cnf(u1079,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),parts(knows(spy,X0)))
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u1066,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),analz(knows(spy,X0))) ) ).

cnf(u1128,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X10),mPair(X11,mPair(agent(X12),mPair(key(X4),X13)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X10,bad)
    | X1 = X10
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad) ) ).

cnf(u339,axiom,
    member(nat,aa(agent1,nat,shrK,X0),symKeys) ).

cnf(u1052,negated_conjecture,
    ( member(msg,na,parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u704,axiom,
    ( ~ member(msg,key(sK1(X0)),X0)
    | ~ member(nat,sK1(X0),symKeys)
    | member(msg,sK0(X0),analz(X0))
    | analz(X0) = X0
    | member(msg,sK3(X0),analz(X0)) ) ).

cnf(u1043,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X12),mPair(key(X4),X13)))),knows(spy,X0)) ) ).

cnf(u676,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),X0),X1)
    | member(msg,X0,analz(X1))
    | ~ member(msg,key(aa(agent1,nat,shrK,X2)),X1) ) ).

cnf(u1046,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X8,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X1 = X8
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X11,mPair(agent(X12),mPair(key(X4),X13)))),knows(spy,X0)) ) ).

cnf(u1291,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u804,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0))) ) ).

cnf(u199,negated_conjecture,
    ~ member(event,notes(spy,mPair(na,mPair(X0,key(k)))),set(event,evs)) ).

cnf(u253,axiom,
    ( ~ member(msg,X1,analz(X0))
    | member(msg,X1,parts(X0)) ) ).

cnf(u639,negated_conjecture,
    ( ~ member(event,says(server,X0,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3))))),set(event,evs))
    | na = X1 ) ).

cnf(u240,axiom,
    spy != server ).

cnf(u995,axiom,
    ( ~ member(event,says(X3,X1,crypt(X4,nonce(X10))),set(event,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X2),mPair(nonce(X10),key(X4)))),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u813,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u247,axiom,
    parts(X0) = analz(parts(X0)) ).

cnf(u438,negated_conjecture,
    member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),parts(knows(server,evs))) ).

cnf(u234,axiom,
    ( ~ member(event,says(X3,X2,X1),set(event,X0))
    | member(msg,X1,knows(X3,X0)) ) ).

cnf(u213,axiom,
    ( ~ member(event,says(X4,X5,crypt(aa(agent1,nat,shrK,X5),mPair(nonce(X3),mPair(agent(X2),mPair(key(X1),X0))))),set(event,X6))
    | ~ member(event,says(X5,server,mPair(agent(X5),mPair(agent(X2),nonce(X3)))),set(event,X6))
    | member(list(event),cons(event,says(X5,X2,X0),X6),nS_Sha254967238shared)
    | server = X5
    | ~ member(list(event),X6,nS_Sha254967238shared) ) ).

cnf(u266,axiom,
    ( agent(X1) != agent(X0)
    | X0 = X1 ) ).

cnf(u971,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),knows(spy,X0))
    | X2 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u619,axiom,
    ( member(msg,sK2(X0),analz(X0))
    | analz(X0) = X0
    | member(msg,sK0(X0),parts(X0)) ) ).

cnf(u236,axiom,
    ( ~ member(event,says(X3,X2,X1),set(event,X0))
    | member(msg,X1,analz(knows(spy,X0))) ) ).

cnf(u227,axiom,
    ( ~ member(event,notes(X2,X1),set(event,X0))
    | member(msg,X1,knows(X2,X0)) ) ).

cnf(u624,axiom,
    ( ~ member(event,says(server,X1,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | X5 = X6
    | member(agent1,X7,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X9),mPair(key(X4),X6)))),parts(knows(spy,X0))) ) ).

cnf(u230,axiom,
    ( says(X5,X4,X3) != says(X2,X1,X0)
    | X0 = X3 ) ).

cnf(u843,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),analz(knows(spy,X0))) ) ).

cnf(u229,axiom,
    ( ~ member(event,says(X3,X2,X1),set(event,X0))
    | member(msg,X1,parts(knows(spy,X0))) ) ).

cnf(u1022,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u923,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),knows(spy,X0)) ) ).

cnf(u223,axiom,
    notes(X1,X0) != says(X4,X3,X2) ).

cnf(u895,negated_conjecture,
    ( member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u210,axiom,
    ( member(msg,key(aa(agent1,nat,shrK,X1)),knows(spy,X0))
    | ~ member(agent1,X1,bad) ) ).

cnf(u209,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),X1),analz(knows(spy,X0)))
    | ~ member(agent1,X2,bad)
    | member(msg,X1,analz(knows(spy,X0))) ) ).

cnf(u969,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X3 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u212,axiom,
    ( member(msg,key(aa(agent1,nat,shrK,X0)),analz(knows(spy,X1)))
    | ~ member(agent1,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u1188,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | member(msg,X1,analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0))))))) ) ).

cnf(u331,axiom,
    says(X2,X1,X0) != gets(X4,X3) ).

cnf(u203,axiom,
    ~ member(agent1,server,bad) ).

cnf(u642,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X0,mPair(agent(X2),mPair(key(k),X3)))),parts(knows(spy,evs)))
    | member(agent1,X1,bad)
    | na = X0 ) ).

cnf(u506,negated_conjecture,
    member(msg,agent(b),parts(knows(spy,evs))) ).

cnf(u1232,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X13),mPair(X14,mPair(agent(X15),mPair(key(X4),X8)))),knows(spy,X0))
    | X5 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X13,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u614,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0))) ) ).

cnf(u998,negated_conjecture,
    ( ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | member(msg,agent(b),analz(knows(server,cons(event,gets(X0,X1),evs)))) ) ).

cnf(u327,axiom,
    ( aa(agent1,nat,publicKey(X3),X2) != aa(agent1,nat,publicKey(X1),X0)
    | X0 = X2 ) ).

cnf(u1246,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X13),mPair(X8,mPair(agent(X14),mPair(key(X4),X15)))),knows(spy,X0))
    | X2 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X13,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u954,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u283,axiom,
    ( ~ member(msg,mPair(X2,X1),parts(X0))
    | member(msg,X2,parts(X0)) ) ).

cnf(u766,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(server,X1))
    | member(agent1,X0,bad) ) ).

cnf(u441,negated_conjecture,
    member(msg,na,parts(knows(server,evs))) ).

cnf(u1248,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X12),mPair(X13,mPair(agent(X14),mPair(key(X4),X15)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X1 = X12
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X12,bad) ) ).

cnf(u827,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u594,axiom,
    ( member(msg,sK3(X0),analz(X0))
    | analz(X0) = X0
    | member(msg,sK0(X0),parts(X0)) ) ).

cnf(u1122,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X12,mPair(agent(X13),mPair(key(X4),X8)))),knows(spy,X0))
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u285,axiom,
    ( mPair(X3,X2) != mPair(X1,X0)
    | X0 = X2 ) ).

cnf(u279,axiom,
    ( key(X1) != key(X0)
    | X0 = X1 ) ).

cnf(u1198,negated_conjecture,
    ( member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u437,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,a),mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))))),knows(spy,evs)) ).

cnf(u778,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X9),mPair(key(X6),X1)))),parts(knows(spy,X0)))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X4,mPair(agent(X5),mPair(key(X6),X2)))),parts(knows(spy,X0)))
    | member(agent1,X7,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared) ) ).

cnf(u1197,negated_conjecture,
    ( member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u265,axiom,
    mPair(X2,X1) != agent(X0) ).

cnf(u589,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X1)),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X2,X3),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad) ) ).

cnf(u1222,negated_conjecture,
    ( member(msg,agent(b),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u546,negated_conjecture,
    member(msg,agent(a),parts(knows(spy,evs))) ).

cnf(u1221,negated_conjecture,
    ( member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u259,axiom,
    ( ~ member(msg,mPair(X2,X1),analz(X0))
    | member(msg,X1,analz(X0)) ) ).

cnf(u1084,negated_conjecture,
    ( member(msg,key(k),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u840,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(msg,X5,parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u1150,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0))
    | member(msg,X1,parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))))))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared) ) ).

cnf(u261,axiom,
    agent(X0) != crypt(X2,X1) ).

cnf(u864,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X3,mPair(agent(X4),mPair(key(X5),X6)))),parts(knows(spy,X2)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X2,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | X0 = X1
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X7,mPair(agent(X8),mPair(key(X5),X9)))),knows(spy,X2)) ) ).

cnf(u1149,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X14,mPair(agent(X15),mPair(key(X4),X8)))),knows(spy,X0)) ) ).

cnf(u737,axiom,
    ( ~ member(msg,key(sK1(X0)),X0)
    | member(msg,sK3(X0),parts(X0))
    | member(msg,sK0(X0),analz(X0))
    | ~ member(nat,sK1(X0),symKeys)
    | analz(X0) = X0 ) ).

cnf(u256,axiom,
    ( member(msg,X1,analz(X0))
    | ~ member(msg,X1,X0) ) ).

cnf(u1146,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared)
    | member(msg,X1,parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0)))))) ) ).

cnf(u767,axiom,
    ( member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(server,cons(event,gets(X6,X7),X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u1145,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),knows(spy,X4))
    | member(msg,X5,parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u1183,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | member(msg,X1,parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0)) ) ).

cnf(u521,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),parts(knows(spy,evs))) ).

cnf(u845,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u394,axiom,
    ( ~ member(msg,mPair(X0,X2),X1)
    | member(msg,X0,analz(X1)) ) ).

cnf(u1126,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X12),mPair(key(X4),X13)))),knows(spy,X0))
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u206,axiom,
    ( member(event,says(server,X5,crypt(aa(agent1,nat,shrK,X5),mPair(X4,mPair(agent(X3),mPair(key(X2),X1))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(agent1,X5,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X5),mPair(X4,mPair(agent(X3),mPair(key(X2),X1)))),parts(knows(spy,X0))) ) ).

cnf(u224,axiom,
    ( notes(X3,X2) != notes(X1,X0)
    | X0 = X2 ) ).

cnf(u205,axiom,
    ( member(msg,key(aa(agent1,nat,shrK,X0)),parts(knows(spy,X1)))
    | ~ member(agent1,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u1275,axiom,
    ( ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X16),mPair(key(X4),X17)))),knows(spy,X0)) ) ).

cnf(u591,negated_conjecture,
    ~ member(nat,k,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ).

cnf(u556,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),X1),knows(spy,X2))
    | member(msg,X1,analz(knows(spy,X2)))
    | ~ member(agent1,X0,bad) ) ).

cnf(u1191,axiom,
    ( ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X13,X14),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X1 = X8
    | member(agent1,X8,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X15,mPair(agent(X16),mPair(key(X4),X17)))),parts(knows(spy,X0))) ) ).

cnf(u1098,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X13,mPair(agent(X14),mPair(key(X4),X15)))),parts(knows(spy,X0)))
    | X1 = X8
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X8,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u1135,axiom,
    ( member(msg,mPair(X5,mPair(agent(X6),mPair(key(X7),X8))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4)))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u871,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u797,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(list(event),cons(event,says(X1,X3,X5),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | server = X1
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(event,says(X1,server,mPair(agent(X1),mPair(agent(X3),nonce(X2)))),set(event,cons(event,gets(X6,X7),X0))) ) ).

cnf(u743,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5 ) ).

cnf(u220,axiom,
    ( ~ member(event,says(server,X9,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X7),mPair(key(X6),X5))))),set(event,X4))
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | ~ member(event,says(server,X3,crypt(aa(agent1,nat,shrK,X3),mPair(X2,mPair(agent(X1),mPair(key(X6),X0))))),set(event,X4))
    | X2 = X8 ) ).

cnf(u1108,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X1)),knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),analz(knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u536,axiom,
    ( member(msg,crypt(sK1(X0),sK0(X0)),X0)
    | analz(X0) = X0
    | member(msg,sK2(X0),analz(X0)) ) ).

cnf(u1023,negated_conjecture,
    ( ~ member(msg,key(aa(agent1,nat,shrK,b)),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | member(msg,mPair(key(k),agent(a)),analz(knows(server,cons(event,gets(X0,X1),evs)))) ) ).

cnf(u543,axiom,
    ( ~ member(msg,key(X0),analz(X1))
    | ~ member(nat,X0,symKeys)
    | member(msg,X2,analz(X1))
    | ~ member(msg,crypt(X0,X2),X1) ) ).

cnf(u732,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared) ) ).

cnf(u851,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(msg,X5,parts(knows(spy,X0))) ) ).

cnf(u304,axiom,
    knows(spy,X0) = knows(spy,cons(event,gets(X2,X1),X0)) ).

cnf(u1178,axiom,
    ( ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X14,X15),cons(event,gets(X16,X17),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | X5 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u688,axiom,
    ( ~ member(list(event),cons(event,gets(X4,X5),cons(event,gets(X2,X3),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,key(aa(agent1,nat,shrK,X1)),analz(knows(spy,X0))) ) ).

cnf(u500,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X0)),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(agent1,X0,bad) ) ).

cnf(u695,axiom,
    ( member(msg,sK2(X0),parts(X0))
    | member(msg,sK0(X0),parts(X0))
    | analz(X0) = X0 ) ).

cnf(u974,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X2 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u298,axiom,
    ( ~ member(nat,aa(agent1,nat,publicKey(X3),X2),image(agent1,nat,publicKey(X1),X0))
    | member(agent1,X2,X0) ) ).

cnf(u328,axiom,
    ( aa(agent1,nat,publicKey(X3),X2) != aa(agent1,nat,publicKey(X1),X0)
    | X1 = X3 ) ).

cnf(u1130,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),parts(knows(spy,X4)))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared)
    | member(msg,X5,analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4))))) ) ).

cnf(u847,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),mPair(X3,mPair(agent(X4),mPair(key(X5),X1)))),parts(knows(spy,X6)))
    | member(agent1,X2,bad)
    | X0 = X1
    | member(agent1,X7,bad)
    | ~ member(list(event),X6,nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X8,mPair(agent(X9),mPair(key(X5),X0)))),knows(spy,X6)) ) ).

cnf(u207,axiom,
    ( ~ member(event,notes(X2,X1),set(event,X0))
    | ~ member(agent1,X2,bad)
    | member(msg,X1,knows(spy,X0)) ) ).

cnf(u684,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3)))),knows(spy,evs))
    | a = X0
    | member(agent1,X0,bad) ) ).

cnf(u294,axiom,
    ( member(msg,X1,parts(X0))
    | ~ member(msg,X1,X0) ) ).

cnf(u324,axiom,
    ~ member(nat,aa(agent1,nat,publicKey(X1),X0),symKeys) ).

cnf(u519,axiom,
    ( ~ member(list(event),cons(event,gets(X2,X3),X0),nS_Sha254967238shared)
    | ~ member(agent1,X1,bad)
    | member(msg,key(aa(agent1,nat,shrK,X1)),analz(knows(spy,X0))) ) ).

cnf(u248,axiom,
    parts(X0) = parts(analz(X0)) ).

cnf(u255,axiom,
    analz(X0) = analz(analz(X0)) ).

cnf(u882,negated_conjecture,
    ( member(msg,na,parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u799,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u694,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0))) ) ).

cnf(u274,axiom,
    ( crypt(X3,X2) != crypt(X1,X0)
    | X0 = X2 ) ).

cnf(u241,axiom,
    ( member(msg,mPair(sK2(X0),sK3(X0)),X0)
    | member(msg,crypt(sK1(X0),sK0(X0)),X0)
    | analz(X0) = X0 ) ).

cnf(u906,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X5,mPair(agent(X6),mPair(key(X7),X1)))),knows(spy,X4))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X8,mPair(agent(X9),mPair(key(X7),X2)))),knows(spy,X4)) ) ).

cnf(u878,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))) ) ).

cnf(u674,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3)))),knows(spy,evs))
    | na = X1
    | member(agent1,X0,bad) ) ).

cnf(u1051,negated_conjecture,
    ( member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u997,negated_conjecture,
    ( member(msg,mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared)
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs))) ) ).

cnf(u858,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),mPair(X1,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X6)))
    | member(agent1,X2,bad)
    | X0 = X1
    | member(agent1,X7,bad)
    | ~ member(list(event),X6,nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X0,mPair(agent(X8),mPair(key(X4),X9)))),knows(spy,X6)) ) ).

cnf(u830,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0))) ) ).

cnf(u964,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),parts(knows(spy,X0)))
    | X5 = X8
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared) ) ).

cnf(u317,axiom,
    ~ pp(fFalse) ).

cnf(u1159,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0))
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))))))
    | ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X5,X6),X0))),nS_Sha254967238shared) ) ).

cnf(u625,negated_conjecture,
    ( ~ member(event,says(server,X0,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3))))),set(event,evs))
    | crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))) = X3 ) ).

cnf(u854,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X8),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X3 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared) ) ).

cnf(u1294,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),parts(knows(spy,X0)))
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),analz(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0))))))) ) ).

cnf(u1260,negated_conjecture,
    ( member(msg,agent(a),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u649,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3)))),parts(knows(spy,evs)))
    | member(agent1,X0,bad)
    | a = X0 ) ).

cnf(u1292,axiom,
    ( ~ member(list(event),cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))),nS_Sha254967238shared)
    | member(msg,mPair(agent(X2),mPair(key(X3),X4)),parts(knows(server,cons(event,gets(X7,X8),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X5,X6),X0)))))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X1,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0)) ) ).

cnf(u297,axiom,
    ~ member(nat,aa(agent1,nat,shrK,X2),image(agent1,nat,publicKey(X1),X0)) ).

cnf(u291,axiom,
    ( pp(aa(X0,bool,X1,X2))
    | ~ member(X0,X2,X1) ) ).

cnf(u1050,negated_conjecture,
    ( member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),evs)),nS_Sha254967238shared) ) ).

cnf(u773,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),analz(knows(spy,X0))) ) ).

cnf(u892,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(nonce(X2),mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(event,says(X3,X1,crypt(X4,nonce(X8))),set(event,cons(event,gets(X9,X10),cons(event,gets(X6,X7),X0))))
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X2),mPair(nonce(X8),key(X4)))),cons(event,gets(X9,X10),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared) ) ).

cnf(u806,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u926,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X8,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | X1 = X8
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X9,mPair(agent(X10),mPair(key(X4),X11)))),knows(spy,X0)) ) ).

cnf(u602,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X5,mPair(agent(X2),mPair(key(X3),X4)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X2),mPair(key(X3),agent(X1))) = X4
    | ~ member(list(event),X0,nS_Sha254967238shared) ) ).

cnf(u1288,axiom,
    ( ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X11,X12),cons(event,gets(X13,X14),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X8,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X1 = X8
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X15,mPair(agent(X16),mPair(key(X4),X17)))),knows(spy,X0)) ) ).

cnf(u1250,negated_conjecture,
    ( member(msg,mPair(key(k),agent(a)),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u474,negated_conjecture,
    member(msg,mPair(key(k),agent(a)),parts(knows(server,evs))) ).

cnf(u881,negated_conjecture,
    ( member(msg,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u1236,negated_conjecture,
    ( member(msg,key(k),parts(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),cons(event,gets(X4,X5),evs))),nS_Sha254967238shared) ) ).

cnf(u1063,axiom,
    ( ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X12,X13),cons(event,gets(X6,X7),X0)))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u824,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u979,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X8),mPair(X11,mPair(agent(X12),mPair(key(X4),X13)))),parts(knows(spy,X0)))
    | X1 = X8
    | member(agent1,X8,bad)
    | ~ member(list(event),cons(event,gets(X9,X10),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u1049,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),parts(knows(server,cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)))))) ) ).

cnf(u1036,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(list(event),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X12,mPair(agent(X13),mPair(key(X4),X8)))),knows(spy,X0)) ) ).

cnf(u632,negated_conjecture,
    ( ~ member(event,says(server,X0,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3))))),set(event,evs))
    | b = X2 ) ).

cnf(u848,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X10,mPair(agent(X11),mPair(key(X4),X8)))),parts(knows(spy,X0)))
    | X5 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared) ) ).

cnf(u235,axiom,
    ( ~ member(event,says(X3,X2,X1),set(event,X0))
    | member(msg,X1,knows(spy,X0)) ) ).

cnf(u660,axiom,
    ( ~ member(msg,crypt(X0,X1),X2)
    | member(msg,X1,analz(X2))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),X2) ) ).

cnf(u745,axiom,
    ( ~ member(msg,key(sK1(X0)),X0)
    | member(msg,sK2(X0),parts(X0))
    | member(msg,sK0(X0),analz(X0))
    | ~ member(nat,sK1(X0),symKeys)
    | analz(X0) = X0 ) ).

cnf(u238,axiom,
    ( ~ member(event,says(server,X5,crypt(aa(agent1,nat,shrK,X5),mPair(X4,mPair(X3,mPair(X2,X1))))),set(event,X0))
    | member(msg,X2,parts(knows(spy,X0))) ) ).

cnf(u820,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X10,X11),cons(event,gets(X6,X7),X0))),nS_Sha254967238shared)
    | member(msg,X5,parts(knows(spy,X0))) ) ).

cnf(u651,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X5),mPair(nonce(X0),mPair(agent(X4),mPair(key(X2),X6)))),parts(knows(spy,X3)))
    | ~ member(event,says(X4,X5,crypt(X2,nonce(X1))),set(event,X3))
    | ~ member(list(event),X3,nS_Sha254967238shared)
    | member(agent1,X5,bad)
    | member(list(event),cons(event,notes(spy,mPair(nonce(X0),mPair(nonce(X1),key(X2)))),X3),nS_Sha254967238shared) ) ).

cnf(u237,axiom,
    member(msg,key(aa(agent1,nat,shrK,X1)),knows(X1,X0)) ).

cnf(u801,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u450,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,a),mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))))),analz(knows(spy,evs))) ).

cnf(u628,negated_conjecture,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(k),X0)))),parts(knows(spy,evs)))
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))) = X0 ) ).

cnf(u231,axiom,
    ( says(X5,X4,X3) != says(X2,X1,X0)
    | X1 = X4 ) ).

cnf(u1140,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,server),mPair(X5,mPair(agent(X6),mPair(key(X7),X8)))),knows(spy,X4))
    | member(msg,X5,analz(knows(server,cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)))))
    | ~ member(list(event),cons(event,gets(X0,X1),cons(event,gets(X2,X3),X4)),nS_Sha254967238shared) ) ).

cnf(u788,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X7),mPair(X1,mPair(agent(X8),mPair(key(X5),X9)))),parts(knows(spy,X0)))
    | X1 = X2
    | member(agent1,X3,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X3),mPair(X2,mPair(agent(X4),mPair(key(X5),X6)))),parts(knows(spy,X0)))
    | member(agent1,X7,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared) ) ).

cnf(u218,axiom,
    ( ~ member(event,says(server,X9,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X7),mPair(key(X6),X5))))),set(event,X4))
    | ~ member(list(event),X4,nS_Sha254967238shared)
    | ~ member(event,says(server,X3,crypt(aa(agent1,nat,shrK,X3),mPair(X2,mPair(agent(X1),mPair(key(X6),X0))))),set(event,X4))
    | X0 = X5 ) ).

cnf(u258,axiom,
    ( ~ member(msg,mPair(X2,X1),analz(X0))
    | member(msg,X2,analz(X0)) ) ).

cnf(u612,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0)) ) ).

cnf(u217,axiom,
    ( ~ member(event,says(server,X4,crypt(aa(agent1,nat,shrK,X4),mPair(nonce(X1),mPair(agent(X5),mPair(key(X3),X0))))),set(event,X6))
    | member(list(event),cons(event,notes(spy,mPair(nonce(X1),mPair(nonce(X2),key(X3)))),X6),nS_Sha254967238shared)
    | ~ member(event,says(X5,X4,crypt(X3,nonce(X2))),set(event,X6))
    | ~ member(list(event),X6,nS_Sha254967238shared) ) ).

cnf(u603,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | crypt(aa(agent1,nat,shrK,X3),mPair(key(X4),agent(X1))) = X5 ) ).

cnf(u1010,negated_conjecture,
    ( member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),analz(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(msg,key(aa(agent1,nat,shrK,a)),knows(server,cons(event,gets(X0,X1),evs)))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u380,negated_conjecture,
    member(msg,key(k),parts(knows(spy,evs))) ).

cnf(u211,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X0)),analz(knows(spy,X1)))
    | member(agent1,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u402,axiom,
    ( ~ member(msg,mPair(X0,X2),X1)
    | member(msg,X0,parts(X1)) ) ).

cnf(u214,axiom,
    ( ~ member(event,says(server,X6,crypt(X5,mPair(X4,mPair(agent(X3),mPair(key(X2),X1))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | aa(agent1,nat,shrK,X6) = X5 ) ).

cnf(u796,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(nonce(X4),mPair(agent(X1),mPair(key(X5),X2)))),knows(spy,X3))
    | server = X0
    | ~ member(list(event),X3,nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | ~ member(event,says(X0,server,mPair(agent(X0),mPair(agent(X1),nonce(X4)))),set(event,X3))
    | member(list(event),cons(event,says(X0,X1,X2),X3),nS_Sha254967238shared) ) ).

cnf(u491,negated_conjecture,
    member(msg,na,parts(knows(spy,evs))) ).

cnf(u404,axiom,
    ( ~ member(msg,crypt(X2,X0),X1)
    | member(msg,X0,parts(X1)) ) ).

cnf(u599,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | ~ member(nat,X4,image(agent1,nat,shrK,top_top(fun(agent1,bool)))) ) ).

cnf(u200,negated_conjecture,
    member(event,says(server,a,crypt(aa(agent1,nat,shrK,a),mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))))),set(event,evs)) ).

cnf(u335,axiom,
    ( ~ member(event,gets(X2,X1),set(event,X0))
    | member(msg,X1,knows(X2,X0))
    | spy = X2 ) ).

cnf(u225,axiom,
    ( notes(X3,X2) != notes(X1,X0)
    | X1 = X3 ) ).

cnf(u879,negated_conjecture,
    ( member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u646,negated_conjecture,
    ( ~ member(event,says(server,X0,crypt(aa(agent1,nat,shrK,X0),mPair(X1,mPair(agent(X2),mPair(key(k),X3))))),set(event,evs))
    | a = X0 ) ).

cnf(u321,axiom,
    aa(agent1,nat,shrK,X2) != aa(agent1,nat,publicKey(X1),X0) ).

cnf(u925,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X2),mPair(X7,mPair(agent(X8),mPair(key(X5),X9)))),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(agent1,X2,bad)
    | X0 = X2
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X3,mPair(agent(X4),mPair(key(X5),X6)))),knows(spy,X1))
    | member(agent1,X0,bad) ) ).

cnf(u645,axiom,
    ( ~ member(event,says(server,X1,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | X1 = X6
    | member(agent1,X6,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X6),mPair(X7,mPair(agent(X8),mPair(key(X4),X9)))),parts(knows(spy,X0))) ) ).

cnf(u698,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0))) ) ).

cnf(u196,hypothesis,
    ~ member(agent1,b,bad) ).

cnf(u697,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X3,mPair(agent(X4),mPair(key(X2),X5)))),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(msg,key(X2),parts(knows(spy,X1)))
    | member(agent1,X0,bad) ) ).

cnf(u859,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X9),mPair(X8,mPair(agent(X10),mPair(key(X4),X11)))),parts(knows(spy,X0)))
    | X2 = X8
    | member(agent1,X9,bad)
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0)))
    | member(agent1,X1,bad)
    | ~ member(list(event),cons(event,gets(X6,X7),X0),nS_Sha254967238shared) ) ).

cnf(u312,axiom,
    key(X1) != nonce(X0) ).

cnf(u598,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X3,mPair(agent(X4),mPair(key(X2),X5)))),knows(spy,X0))
    | member(agent1,X1,bad)
    | ~ member(nat,X2,image(agent1,nat,shrK,top_top(fun(agent1,bool))))
    | ~ member(list(event),X0,nS_Sha254967238shared) ) ).

cnf(u273,axiom,
    ( ~ member(msg,crypt(X2,X1),parts(X0))
    | member(msg,X1,parts(X0)) ) ).

cnf(u982,axiom,
    ( ~ member(msg,key(aa(agent1,nat,shrK,X1)),knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0))))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(agent1,X1,bad)
    | member(msg,mPair(X2,mPair(agent(X3),mPair(key(X4),X5))),analz(knows(server,cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)))))
    | ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),parts(knows(spy,X0))) ) ).

cnf(u306,axiom,
    agent(X1) != nonce(X0) ).

cnf(u439,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,a),mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))))))),parts(knows(spy,evs))) ).

cnf(u409,axiom,
    ( ~ member(msg,mPair(X2,X0),X1)
    | member(msg,X0,parts(X1)) ) ).

cnf(u938,negated_conjecture,
    ( member(msg,agent(a),parts(knows(server,cons(event,gets(X0,X1),evs))))
    | ~ member(list(event),cons(event,gets(X0,X1),evs),nS_Sha254967238shared) ) ).

cnf(u308,axiom,
    crypt(X1,X0) != nonce(X2) ).

cnf(u872,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X0),mPair(X4,mPair(agent(X5),mPair(key(X6),X7)))),parts(knows(spy,X3)))
    | ~ member(list(event),cons(event,gets(X1,X2),X3),nS_Sha254967238shared)
    | member(agent1,X0,bad)
    | member(msg,mPair(X4,mPair(agent(X5),mPair(key(X6),X7))),analz(knows(server,cons(event,gets(X1,X2),X3))))
    | ~ member(msg,key(aa(agent1,nat,shrK,X0)),knows(server,cons(event,gets(X1,X2),X3))) ) ).

cnf(u463,negated_conjecture,
    member(msg,crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a))),parts(knows(server,evs))) ).

cnf(u811,axiom,
    ( ~ member(msg,crypt(aa(agent1,nat,shrK,X1),mPair(X2,mPair(agent(X3),mPair(key(X4),X5)))),knows(spy,X0))
    | ~ member(list(event),cons(event,gets(X8,X9),cons(event,gets(X6,X7),X0)),nS_Sha254967238shared)
    | member(msg,key(X4),parts(knows(spy,X0)))
    | member(agent1,X1,bad) ) ).

cnf(u269,axiom,
    key(X0) != crypt(X2,X1) ).

cnf(u302,axiom,
    ( member(nat,aa(agent1,nat,shrK,X1),image(agent1,nat,shrK,X0))
    | ~ member(agent1,X1,X0) ) ).

cnf(u487,negated_conjecture,
    member(msg,mPair(na,mPair(agent(b),mPair(key(k),crypt(aa(agent1,nat,shrK,b),mPair(key(k),agent(a)))))),parts(knows(spy,evs))) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : SWV743_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.03  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.11  % Computer : n012.cluster.edu
% 0.00/0.11  % Model    : x86_64 x86_64
% 0.00/0.11  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11  % Memory   : 8046.5625MB
% 0.00/0.11  % OS       : Linux 6.8.0-71-generic
% 0.00/0.11  % CPULimit : 300
% 0.00/0.11  % WCLimit  : 300
% 0.00/0.11  % DateTime : Mon Sep 28 12:24:49 UTC 2026
% 0.00/0.11  % CPUTime  : 
% 0.00/0.11  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.13  Running first-order theorem proving
% 0.08/0.13  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.98/1.08  % (3344235)Detected formulas, will run a generic FOF schedule.
% 4.98/1.08  % (3344240)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=4020870371:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.98/1.08  % (3344241)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3116764637:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.98/1.08  % (3344246)dis-21_1_sil=8000:lcm=predicate:random_seed=505429535:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.98/1.08  % (3344243)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2655936918:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.98/1.08  % (3344245)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1917381649:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.98/1.08  % (3344242)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2195625332:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.98/1.08  % (3344244)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1480231659:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.98/1.08  % (3344243)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.98/1.08  % (3344242)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.98/1.08  % (3344243)Refutation not found, incomplete strategy
% 4.98/1.08  % (3344243)------------------------------
% 4.98/1.08  % (3344243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.98/1.08  % (3344243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.08  % (3344243)CaDiCaL version: 2.1.3
% 4.98/1.08  % (3344243)Termination reason: Refutation not found, incomplete strategy
% 4.98/1.08  % (3344243)Time elapsed: 0.004 s
% 4.98/1.08  % (3344243)Peak memory usage: 88 MB
% 4.98/1.08  % (3344243)Instructions burned: 10 (million)
% 4.98/1.08  % (3344245)Refutation not found, incomplete strategy
% 4.98/1.08  % (3344245)------------------------------
% 4.98/1.08  % (3344245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.98/1.08  % (3344245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.08  % (3344245)CaDiCaL version: 2.1.3
% 4.98/1.08  % (3344245)Termination reason: Refutation not found, incomplete strategy
% 4.98/1.08  % (3344245)Time elapsed: 0.011 s
% 4.98/1.08  % (3344245)Peak memory usage: 88 MB
% 4.98/1.08  % (3344245)Instructions burned: 33 (million)
% 4.98/1.08  % (3344244)Refutation not found, incomplete strategy
% 4.98/1.08  % (3344244)------------------------------
% 4.98/1.08  % (3344244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.98/1.08  % (3344244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.08  % (3344244)CaDiCaL version: 2.1.3
% 4.98/1.08  % (3344244)Termination reason: Refutation not found, incomplete strategy
% 4.98/1.08  % (3344244)Time elapsed: 0.017 s
% 4.98/1.08  % (3344244)Peak memory usage: 88 MB
% 4.98/1.08  % (3344244)Instructions burned: 51 (million)
% 4.98/1.08  % (3344246)Instruction limit reached! 
% 4.98/1.08  % (3344246)------------------------------
% 4.98/1.08  % (3344246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.98/1.08  % (3344246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.08  % (3344246)CaDiCaL version: 2.1.3
% 4.98/1.08  % (3344246)Termination reason: Instruction limit
% 4.98/1.08  % (3344246)Termination phase: Saturation
% 4.98/1.08  % (3344246)Time elapsed: 0.039 s
% 4.98/1.08  % (3344246)Peak memory usage: 89 MB
% 4.98/1.08  % (3344246)Instructions burned: 130 (million)
% 4.98/1.08  % (3344243)------------------------------
% 4.98/1.08  % (3344243)------------------------------
% 4.98/1.08  % (3344245)------------------------------
% 4.98/1.08  % (3344245)------------------------------
% 4.98/1.08  % (3344244)------------------------------
% 4.98/1.08  % (3344244)------------------------------
% 4.98/1.08  % (3344254)lrs+10_1_sil=8000:sp=occurrence:random_seed=3032404666:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.98/1.08  % Exception at run slice level% Exception at run slice level
% 5.68/1.13  
% 5.68/1.13  User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL.
% 5.68/1.13  
% 5.68/1.13  % Exception at run slice level
% 5.68/1.13  User error: GNN currently only supports monomorphic FOL.
% 5.68/1.13  % (3344254)Refutation not found, incomplete strategy
% 5.68/1.13  % (3344254)------------------------------
% 5.68/1.13  % (3344254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344254)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344254)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.13  % (3344254)Time elapsed: 0.035 s
% 5.68/1.13  % (3344254)Peak memory usage: 89 MB
% 5.68/1.13  % (3344254)Instructions burned: 95 (million)
% 5.68/1.13  % (3344255)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3312976951:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.68/1.13  % (3344256)lrs+1011_1_sil=32000:sp=occurrence:random_seed=730556818:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.68/1.13  % (3344257)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=600143492:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 5.68/1.13  % (3344260)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=217723251:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 5.68/1.13  % (3344259)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1321614461:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 5.68/1.13  % (3344261)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2869099000:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 5.68/1.13  % (3344259)Refutation not found, incomplete strategy
% 5.68/1.13  % (3344259)------------------------------
% 5.68/1.13  % (3344259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344259)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344259)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.13  % (3344259)Time elapsed: 0.006 s
% 5.68/1.13  % (3344259)Peak memory usage: 88 MB
% 5.68/1.13  % (3344259)Instructions burned: 18 (million)
% 5.68/1.13  % (3344255)Instruction limit reached! 
% 5.68/1.13  % (3344255)------------------------------
% 5.68/1.13  % (3344255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344255)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344255)Termination reason: Instruction limit
% 5.68/1.13  % (3344255)Termination phase: Saturation
% 5.68/1.13  % (3344255)Time elapsed: 0.046 s
% 5.68/1.13  % (3344255)Peak memory usage: 89 MB
% 5.68/1.13  % (3344255)Instructions burned: 161 (million)
% 5.68/1.13  % (3344261)Instruction limit reached! 
% 5.68/1.13  % (3344261)------------------------------
% 5.68/1.13  % (3344261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344261)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344261)Termination reason: Instruction limit
% 5.68/1.13  % (3344261)Termination phase: Saturation
% 5.68/1.13  % (3344261)Time elapsed: 0.041 s
% 5.68/1.13  % (3344261)Peak memory usage: 89 MB
% 5.68/1.13  % (3344261)Instructions burned: 114 (million)
% 5.68/1.13  % (3344254)------------------------------
% 5.68/1.13  % (3344254)------------------------------
% 5.68/1.13  % (3344257)Instruction limit reached! 
% 5.68/1.13  % (3344257)------------------------------
% 5.68/1.13  % (3344257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344257)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344257)Termination reason: Instruction limit
% 5.68/1.13  % (3344257)Termination phase: Saturation
% 5.68/1.13  % (3344257)Time elapsed: 0.082 s
% 5.68/1.13  % (3344257)Peak memory usage: 90 MB
% 5.68/1.13  % (3344257)Instructions burned: 249 (million)
% 5.68/1.13  % (3344256)Instruction limit reached! 
% 5.68/1.13  % (3344256)------------------------------
% 5.68/1.13  % (3344256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344256)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344256)Termination reason: Instruction limit
% 5.68/1.13  % (3344256)Termination phase: Saturation
% 5.68/1.13  % (3344256)Time elapsed: 0.102 s
% 5.68/1.13  % (3344256)Peak memory usage: 89 MB
% 5.68/1.13  % (3344256)Instructions burned: 328 (million)
% 5.68/1.13  % (3344268)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4187762089:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 5.68/1.13  % (3344269)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1846726152:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2995 on theBenchmark for (2995ds/114Mi)
% 5.68/1.13  % (3344259)------------------------------
% 5.68/1.13  % (3344259)------------------------------
% 5.68/1.13  % (3344270)lrs+10_1_sil=8000:sp=occurrence:random_seed=2648368281:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 5.68/1.13  % (3344271)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=565501644:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi)
% 5.68/1.13  % (3344268)Instruction limit reached! 
% 5.68/1.13  % (3344268)------------------------------
% 5.68/1.13  % (3344268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344268)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344268)Termination reason: Instruction limit
% 5.68/1.13  % (3344268)Termination phase: Saturation
% 5.68/1.13  % (3344268)Time elapsed: 0.033 s
% 5.68/1.13  % (3344268)Peak memory usage: 88 MB
% 5.68/1.13  % (3344268)Instructions burned: 128 (million)
% 5.68/1.13  % (3344271)Refutation not found, incomplete strategy
% 5.68/1.13  % (3344271)------------------------------
% 5.68/1.13  % (3344271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344271)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344271)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.13  % (3344271)Time elapsed: 0.007 s
% 5.68/1.13  % (3344271)Peak memory usage: 88 MB
% 5.68/1.13  % (3344271)Instructions burned: 21 (million)
% 5.68/1.13  % (3344269)Instruction limit reached! 
% 5.68/1.13  % (3344269)------------------------------
% 5.68/1.13  % (3344269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344269)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344269)Termination reason: Instruction limit
% 5.68/1.13  % (3344269)Termination phase: Saturation
% 5.68/1.13  % (3344269)Time elapsed: 0.032 s
% 5.68/1.13  % (3344269)Peak memory usage: 89 MB
% 5.68/1.13  % (3344269)Instructions burned: 115 (million)
% 5.68/1.13  % (3344272)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=180537028:i=5202:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/5202Mi)
% 5.68/1.13  % (3344270)First to succeed.
% 5.68/1.13  % (3344270)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3344235"
% 5.68/1.13  % Exception at run slice level
% 5.68/1.13  User error: GNN currently only supports monomorphic FOL.
% 5.68/1.13  % (3344277)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=82617655:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi)
% 5.68/1.13  % (3344278)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3666238567:st=8:i=592:sd=3:ep=RST:ss=axioms_2993 on theBenchmark for (2993ds/592Mi)
% 5.68/1.13  % (3344279)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3799424049:st=3:i=13193:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/13193Mi)
% 5.68/1.13  % (3344278)Refutation not found, incomplete strategy
% 5.68/1.13  % (3344278)------------------------------
% 5.68/1.13  % (3344278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344278)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344278)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.13  % (3344278)Time elapsed: 0.005 s
% 5.68/1.13  % (3344278)Peak memory usage: 88 MB
% 5.68/1.13  % (3344278)Instructions burned: 14 (million)
% 5.68/1.13  % (3344277)Instruction limit reached! 
% 5.68/1.13  % (3344277)------------------------------
% 5.68/1.13  % (3344277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.13  % (3344277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.13  % (3344277)CaDiCaL version: 2.1.3
% 5.68/1.13  % (3344277)Termination reason: Instruction limit
% 5.68/1.13  % (3344277)Termination phase: Saturation
% 5.68/1.13  % (3344277)Time elapsed: 0.044 s
% 5.68/1.13  % (3344277)Peak memory usage: 90 MB
% 5.68/1.13  % (3344277)Instructions burned: 136 (million)
% 5.68/1.13  % (3344271)------------------------------
% 5.68/1.13  % (3344271)------------------------------
% 5.68/1.13  % (3344281)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2295814195:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/125Mi)
% 5.68/1.13  % (3344281)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.68/1.13  % SZS status CounterSatisfiable for theBenchmark
% 5.68/1.13  % SZS output start Saturation.
% See solution above
% 5.94/1.23  % SZS output start Definitions and Model Updates.
% 5.94/1.23  % SZS output end Definitions and Model Updates.
% 5.94/1.23  % (3344270)------------------------------
% 5.94/1.23  % (3344270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.94/1.23  % (3344270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.23  % (3344270)CaDiCaL version: 2.1.3
% 5.94/1.23  % (3344270)Termination reason: Satisfiable
% 5.94/1.23  % (3344270)Time elapsed: 0.042 s
% 5.94/1.23  % (3344270)Peak memory usage: 89 MB
% 5.94/1.23  % (3344270)Instructions burned: 119 (million)
% 5.94/1.23  % (3344270)------------------------------
% 5.94/1.23  % (3344270)------------------------------
% 5.94/1.23  % (3344235)Success in time 0.813 s
% 5.94/1.23  % Vampire exiting
%------------------------------------------------------------------------------