Vampire-SAT---5.0.1.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : SWV795_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT

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

% Result   : CounterSatisfiable 99.51s 19.22s
% Output   : Saturation 99.51s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u962,axiom,
    member(msg,X2,used(X0)) ).

cnf(u1150,axiom,
    ~ member(event,notes(X2,X1),set(event,X0)) ).

cnf(u1286,axiom,
    ~ member(list(event),cons(event,notes(X1,X2),X3),nS_Sha254967238shared) ).

cnf(u1293,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X2,X3),X1)))) ).

cnf(u1540,axiom,
    member(msg,X4,analz(knows(spy,cons(event,says(X3,X2,X1),X0)))) ).

cnf(u1598,axiom,
    ~ member(list(event),cons(event,says(X1,X2,X3),X4),nS_Sha254967238shared) ).

cnf(u1642,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X2,X3,X4),X1)))) ).

cnf(u2511,axiom,
    ~ member(msg,crypt(X0,X1),knows(spy,cons(event,notes(X2,X3),X4))) ).

cnf(u2678,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ).

cnf(u2716,axiom,
    ~ member(msg,mPair(X4,X0),knows(spy,X3)) ).

cnf(u2821,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ).

cnf(u2947,hypothesis,
    ~ member(msg,key(shrK(a)),knows(spy,evs)) ).

cnf(u2950,hypothesis,
    ~ member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),analz(knows(spy,evs))) ).

cnf(u2956,axiom,
    member(msg,crypt(shrK(X1),mPair(X2,mPair(agent1(X3),mPair(key(X4),X5)))),knows(server,X0)) ).

cnf(u3000,axiom,
    member(msg,mPair(X0,mPair(agent1(X1),mPair(key(X2),X3))),analz(knows(server,X4))) ).

cnf(u3097,hypothesis,
    ~ member(msg,key(shrK(a)),analz(knows(spy,evs))) ).

cnf(u3181,axiom,
    ~ member(event,says(X5,X4,crypt(X3,nonce(X2))),set(event,X6)) ).

cnf(u3208,axiom,
    ~ member(event,says(X5,server,mPair(agent1(X5),mPair(agent1(X2),nonce(X3)))),set(event,X6)) ).

cnf(u5375,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ).

cnf(u5418,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ).

cnf(u5459,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ).

cnf(u5500,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ).

cnf(u5740,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ).

cnf(u6069,axiom,
    ~ member(msg,crypt(shrK(X0),mPair(key(X2),agent1(X3))),knows(spy,X1)) ).

cnf(u6198,axiom,
    ~ member(msg,crypt(shrK(X0),X2),knows(spy,cons(event,says(X3,X4,X5),X1))) ).

cnf(u6369,hypothesis,
    ~ member(msg,crypt(shrK(X0),mPair(key(k),agent1(X1))),parts(knows(spy,evs))) ).

cnf(u6570,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ).

cnf(u6624,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ).

cnf(u6671,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ).

cnf(u6718,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ).

cnf(u6770,axiom,
    member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ).

cnf(u7132,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ).

cnf(u7194,axiom,
    member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ).

cnf(u7499,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ).

cnf(u7701,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ).

cnf(u8030,axiom,
    ~ member(msg,crypt(shrK(X4),X0),knows(spy,cons(event,notes(X1,X2),X3))) ).

cnf(u8464,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ).

cnf(u8800,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ).

cnf(u8894,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ).

cnf(u9070,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ).

cnf(u9248,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ).

cnf(u9507,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ).

cnf(u10421,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X10))))))) ).

cnf(u10607,axiom,
    ~ member(msg,crypt(shrK(spy),mPair(X4,X0)),knows(spy,X3)) ).

cnf(u10778,axiom,
    ~ member(msg,crypt(shrK(spy),crypt(X5,X0)),knows(spy,X4)) ).

cnf(u11213,axiom,
    ~ member(msg,crypt(shrK(spy),key(shrK(X4))),knows(spy,X3)) ).

cnf(u15630,axiom,
    ~ member(msg,crypt(shrK(spy),key(X0)),knows(spy,X4)) ).

cnf(u16933,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ).

cnf(u18628,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ).

cnf(u19954,axiom,
    ~ member(msg,crypt(X0,X1),knows(spy,cons(event,says(X2,X3,X4),X5))) ).

cnf(u21511,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ).

cnf(u22917,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ).

cnf(u27024,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ).

cnf(u28103,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X11))))))) ).

cnf(u32097,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ).

cnf(u33320,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11))))))) ).

cnf(u33714,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ).

cnf(u39639,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,says(X10,X11,X12),X13))))))) ).

cnf(u41169,axiom,
    ~ member(event,says(server,X2,crypt(shrK(X2),mPair(X1,mPair(agent1(X5),mPair(key(X3),crypt(shrK(X5),mPair(key(X3),agent1(X2)))))))),set(event,X4)) ).

cnf(u41280,axiom,
    ~ member(msg,crypt(shrK(X0),mPair(X2,mPair(agent1(X3),mPair(key(X4),crypt(shrK(X3),mPair(key(X4),agent1(X0))))))),knows(spy,X1)) ).

cnf(u51979,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12)))))))) ).

cnf(u53107,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12)))))))) ).

cnf(u53799,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))) ).

cnf(u56281,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))) ).

cnf(u59990,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X13)))))))) ).

cnf(u8465,axiom,
    ( ~ member(msg,mPair(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u2680,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X9)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u10380,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X2)))))) ) ).

cnf(u9808,axiom,
    ( ~ member(msg,crypt(shrK(X9),X0),knows(spy,X8))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u11186,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u1074,hypothesis,
    member(msg,agent1(b),used(evs)) ).

cnf(u10324,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X2)))))) ) ).

cnf(u9397,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2))))) ) ).

cnf(u9800,axiom,
    ( ~ member(msg,crypt(shrK(X11),X0),analz(knows(spy,X10)))
    | ~ member(agent,X11,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u6127,axiom,
    ( ~ member(msg,key(X4),analz(knows(spy,X3)))
    | ~ member(nat,X4,symKeys)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,crypt(X4,X0),knows(spy,X3)) ) ).

cnf(u9404,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

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

cnf(u44159,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2))))) ) ).

cnf(u9389,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X1)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X2,analz(knows(spy,cons(event,notes(X3,X4),X1))))
    | ~ member(msg,crypt(X0,X2),analz(knows(spy,X1))) ) ).

cnf(u3008,axiom,
    member(msg,X0,analz(knows(server,X1))) ).

cnf(u8436,axiom,
    ( ~ member(msg,key(shrK(X7)),analz(knows(spy,cons(event,says(X3,X4,X5),X6))))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6))) ) ).

cnf(u9801,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u7707,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u9483,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X12)),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u4358,hypothesis,
    ( ~ member(msg,crypt(shrK(X1),mPair(X0,mPair(agent1(X2),mPair(key(k),X3)))),parts(knows(spy,evs)))
    | member(agent,X1,bad)
    | nonce(na) = X0 ) ).

cnf(u9481,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u58043,axiom,
    ( ~ member(msg,crypt(X0,X1),analz(knows(spy,X6)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),analz(knows(spy,X6))) ) ).

cnf(u251,axiom,
    ( agent1(X1) != agent1(X0)
    | X0 = X1 ) ).

cnf(u1722,axiom,
    ( ~ member(msg,key(X0),analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(nat,X0,symKeys)
    | member(msg,X5,analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(msg,crypt(X0,X5),analz(knows(spy,X4))) ) ).

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

cnf(u5331,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u10407,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u6529,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u1084,hypothesis,
    member(msg,x,used(evs)) ).

cnf(u5306,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u10414,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u8895,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u10365,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X0))),analz(knows(spy,X1)))
    | ~ member(msg,crypt(shrK(X0),X2),analz(knows(spy,X1)))
    | member(msg,X2,analz(knows(spy,cons(event,says(X3,X4,X5),X1)))) ) ).

cnf(u10403,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X2))))))) ) ).

cnf(u8801,axiom,
    ( ~ member(msg,mPair(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u18243,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u9471,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X11)),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u13798,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X8),X0))),analz(knows(spy,X7)))
    | ~ member(agent,X8,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u2674,axiom,
    ( ~ member(msg,crypt(shrK(X8),X0),analz(knows(spy,X7)))
    | ~ member(agent,X8,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

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

cnf(u9802,axiom,
    ( ~ member(msg,crypt(shrK(X9),X0),knows(spy,X8))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

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

cnf(u42277,axiom,
    ( ~ member(msg,crypt(shrK(X6),X0),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,key(shrK(X6)),analz(knows(spy,X5))) ) ).

cnf(u18253,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

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

cnf(u18235,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X8,X0)))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

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

cnf(u1299,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u6541,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u388,hypothesis,
    nS_Sha993195050haredp(evs) ).

cnf(u1077,hypothesis,
    member(msg,key(k),used(evs)) ).

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

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

cnf(u18633,axiom,
    ( ~ member(msg,mPair(X14,X0),analz(knows(spy,X13)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X13)))))))) ) ).

cnf(u8440,axiom,
    ( ~ member(msg,key(shrK(X4)),analz(knows(spy,X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,crypt(shrK(X4),X0),knows(spy,X3)) ) ).

cnf(u1610,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X2))
    | member(msg,X1,analz(knows(spy,X2)))
    | ~ member(agent,X0,bad) ) ).

cnf(u6420,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u42355,axiom,
    ( ~ member(msg,crypt(shrK(X6),X0),knows(spy,X5))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,key(shrK(X6)),knows(spy,X5)) ) ).

cnf(u10286,axiom,
    ( ~ member(msg,key(shrK(X7)),analz(knows(spy,cons(event,notes(X4,X5),X6))))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6))) ) ).

cnf(u6408,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u1681,axiom,
    ( ~ member(msg,mPair(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

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

cnf(u9425,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u42842,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,key(X0),analz(knows(spy,X2))) ) ).

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

cnf(u11171,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X8,X0))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u5743,axiom,
    ( ~ member(msg,mPair(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

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

cnf(u9418,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),cons(event,notes(X11,X12),X2))))))) ) ).

cnf(u1028,hypothesis,
    member(msg,x,parts(knows(spy,evs))) ).

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

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

cnf(u9477,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

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

cnf(u9496,axiom,
    ( ~ member(msg,mPair(X0,X13),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12))))))) ) ).

cnf(u222,axiom,
    ( member(msg,key(shrK(X0)),parts(knows(spy,X1)))
    | ~ member(agent,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u11206,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u7942,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12))))))) ) ).

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

cnf(u1471,axiom,
    ( ~ member(msg,crypt(shrK(X2),X0),X1)
    | member(msg,X0,analz(X1))
    | ~ member(msg,key(shrK(X2)),X1) ) ).

cnf(u11208,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X11))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

cnf(u1402,hypothesis,
    member(msg,mPair(key(k),x),analz(used(evs))) ).

cnf(u6485,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u8433,axiom,
    ( ~ member(msg,key(shrK(X6)),analz(knows(spy,cons(event,notes(X3,X4),X5))))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(shrK(X6),X0),analz(knows(spy,X5))) ) ).

cnf(u9510,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12)))))))) ) ).

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

cnf(u13828,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ) ).

cnf(u5503,axiom,
    ( ~ member(msg,crypt(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

cnf(u18237,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u10377,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2))))) ) ).

cnf(u58062,axiom,
    ( ~ member(msg,key(X0),knows(spy,cons(event,notes(X4,X5),X6)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X6)))
    | ~ member(nat,X0,symKeys) ) ).

cnf(u3051,hypothesis,
    member(msg,crypt(shrK(a),mPair(nonce(na),mPair(agent1(b),mPair(key(k),x)))),analz(knows(spy,evs))) ).

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

cnf(u5273,axiom,
    ( ~ member(msg,mPair(X0,X6),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u59379,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X2))) ) ).

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

cnf(u1371,hypothesis,
    member(msg,key(k),parts(used(evs))) ).

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

cnf(u15478,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X11,X0))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

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

cnf(u6526,axiom,
    ( ~ member(msg,mPair(X0,X10),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

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

cnf(u5294,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u4363,hypothesis,
    ( ~ member(msg,crypt(shrK(X0),mPair(X1,mPair(agent1(X2),mPair(key(k),X3)))),knows(spy,evs))
    | nonce(na) = X1
    | member(agent,X0,bad) ) ).

cnf(u1682,axiom,
    ( ~ member(msg,mPair(X4,X0),knows(spy,X3))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u58190,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X7))),analz(knows(spy,X6)))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

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

cnf(u226,axiom,
    ( ~ member(msg,crypt(shrK(X2),X1),analz(knows(spy,X0)))
    | ~ member(agent,X2,bad)
    | member(msg,X1,analz(knows(spy,X0))) ) ).

cnf(u11201,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u10382,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

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

cnf(u286,axiom,
    agent1(X1) != key(X0) ).

cnf(u21887,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0)))),analz(knows(spy,X1))) ) ).

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

cnf(u1379,hypothesis,
    member(msg,nonce(nb),analz(used(evs))) ).

cnf(u51835,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X11))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u42321,axiom,
    ( ~ member(msg,key(shrK(X6)),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(shrK(X6),X0),knows(spy,X5)) ) ).

cnf(u53309,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),cons(event,notes(X13,X14),X15))))))))) ).

cnf(u5360,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u5460,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u223,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(u7924,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X10)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u6399,axiom,
    ( ~ member(msg,mPair(X0,X8),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u6327,hypothesis,
    ~ member(msg,crypt(k,nonce(X0)),knows(spy,evs)) ).

cnf(u8452,axiom,
    ( ~ member(msg,crypt(shrK(X4),X0),knows(spy,X3))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,key(shrK(X4)),knows(spy,X3)) ) ).

cnf(u9492,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u219,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(knows(spy,X1)))
    | member(agent,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u9423,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X2))))))) ) ).

cnf(u10758,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X7,X0))),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u11173,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u3175,axiom,
    ( ~ member(event,says(X4,X5,crypt(shrK(X5),mPair(nonce(X3),mPair(agent1(X2),mPair(key(X1),X0))))),set(event,X6))
    | ~ member(event,says(X5,server,mPair(agent1(X5),mPair(agent1(X2),nonce(X3)))),set(event,X6))
    | server = X5
    | ~ nS_Sha993195050haredp(X6) ) ).

cnf(u6421,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u6553,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

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

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

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

cnf(u14658,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X9),X0))),analz(knows(spy,X8)))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u23847,axiom,
    ( ~ member(event,says(server,X6,crypt(X5,mPair(X4,mPair(agent1(X3),mPair(key(X2),X1))))),set(event,X0))
    | ~ member(list(event),X0,nS_Sha254967238shared)
    | member(agent,X3,bad)
    | member(agent,X6,bad)
    | ~ member(msg,key(X2),analz(knows(spy,X0))) ) ).

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

cnf(u10397,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u43203,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X6))) ) ).

cnf(u42291,axiom,
    ( ~ member(msg,key(shrK(X6)),knows(spy,cons(event,notes(X3,X4),X5)))
    | ~ member(msg,crypt(shrK(X6),X0),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

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

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

cnf(u5276,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u14673,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X11,X0))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

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

cnf(u54085,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),cons(event,notes(X12,X13),X14))))))))) ).

cnf(u2785,axiom,
    ( ~ member(msg,mPair(X0,X8),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u9400,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X2)))))) ) ).

cnf(u1548,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u6522,axiom,
    ( ~ member(msg,mPair(X0,X9),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u10400,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u9385,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X0))),analz(knows(spy,X1)))
    | member(msg,X2,analz(knows(spy,cons(event,notes(X3,X4),X1))))
    | ~ member(msg,crypt(shrK(X0),X2),analz(knows(spy,X1))) ) ).

cnf(u1235,axiom,
    ( member(msg,X0,parts(knows(spy,cons(event,notes(X2,X3),X1))))
    | ~ member(msg,X0,analz(knows(spy,X1))) ) ).

cnf(u9392,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u10385,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X2)))))) ) ).

cnf(u29800,axiom,
    ( ~ member(msg,crypt(X0,X1),analz(knows(spy,X5)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),analz(knows(spy,X5))) ) ).

cnf(u43272,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0)))),analz(knows(spy,X1))) ) ).

cnf(u9377,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u317,axiom,
    ( aa(X1,X0,X3,sK5(X0,X1,X2,X3)) != aa(X1,X0,X2,sK5(X0,X1,X2,X3))
    | X2 = X3 ) ).

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

cnf(u43125,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,key(shrK(X0)),analz(knows(spy,X2))) ) ).

cnf(u59376,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u23999,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

cnf(u1543,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u354,negated_conjecture,
    ~ member(event,says(a,b,crypt(k,mPair(nonce(nb),nonce(nb)))),set(event,evs)) ).

cnf(u58207,axiom,
    ( ~ member(msg,key(shrK(X7)),knows(spy,cons(event,says(X3,X4,X5),X6)))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u13800,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X9),X0))),analz(knows(spy,X8)))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u51791,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X11))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11)))))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u9422,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X2))))))) ) ).

cnf(u320,axiom,
    ~ member(agent,server,bad) ).

cnf(u9393,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u5225,axiom,
    ( ~ member(msg,crypt(X4,X0),analz(knows(spy,X3)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u56496,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),cons(event,notes(X11,X12),cons(event,notes(X13,X14),X15))))))))) ).

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

cnf(u1648,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X1,parts(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

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

cnf(u2529,axiom,
    ( ~ member(msg,crypt(X0,X1),analz(knows(spy,X4)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),analz(knows(spy,X4))) ) ).

cnf(u1472,axiom,
    ( ~ member(msg,crypt(shrK(X4),X0),knows(spy,cons(event,notes(X1,X2),X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,key(shrK(X4)),analz(knows(spy,X3))) ) ).

cnf(u1649,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u332,axiom,
    ( member(list(event),X0,nS_Sha254967238shared)
    | ~ nS_Sha993195050haredp(X0) ) ).

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

cnf(u5680,axiom,
    ( ~ member(msg,mPair(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u9406,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),cons(event,notes(X11,X12),X2))))))) ) ).

cnf(u9487,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X12)),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u6508,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u9249,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u22320,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u977,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,evs))) ).

cnf(u11176,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X8))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u6496,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u1080,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),used(evs)) ).

cnf(u43205,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X8))) ) ).

cnf(u328,axiom,
    ( member(msg,X3,analz(knows(spy,cons(event,notes(X2,X1),X0))))
    | ~ member(msg,X3,analz(knows(spy,X0))) ) ).

cnf(u59333,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u11181,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u7947,axiom,
    ( ~ member(msg,mPair(X14,X0),analz(knows(spy,X13)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,says(X10,X11,X12),X13))))))) ) ).

cnf(u31149,axiom,
    ( ~ member(msg,crypt(X0,X1),knows(spy,X5))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),knows(spy,X5)) ) ).

cnf(u9421,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X2))))))) ) ).

cnf(u7697,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X7))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),X7)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u18255,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u3296,hypothesis,
    ( ~ member(msg,crypt(shrK(X1),mPair(X2,mPair(agent1(X3),mPair(key(k),X0)))),parts(knows(spy,evs)))
    | member(agent,X1,bad)
    | x = X0 ) ).

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

cnf(u2675,axiom,
    ( ~ member(msg,crypt(shrK(X5),X0),knows(spy,X4))
    | ~ member(agent,X5,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4)))) ) ).

cnf(u2912,hypothesis,
    member(msg,crypt(shrK(a),mPair(nonce(na),mPair(agent1(b),mPair(key(k),x)))),knows(spy,evs)) ).

cnf(u6459,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u10334,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u29799,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X5)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X5)))
    | ~ member(nat,X0,symKeys) ) ).

cnf(u43093,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X10))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u1022,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,evs))) ).

cnf(u42858,axiom,
    ( ~ member(msg,key(X0),knows(spy,cons(event,notes(X3,X4),X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2))) ) ).

cnf(u15198,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X11))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u1434,axiom,
    member(msg,X0,parts(used(X1))) ).

cnf(u59380,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,key(X0),analz(knows(spy,X2))) ) ).

cnf(u9501,axiom,
    ( ~ member(msg,crypt(shrK(X10),X0),analz(knows(spy,X9)))
    | ~ member(agent,X10,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ) ).

cnf(u9380,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

cnf(u257,axiom,
    ( shrK(X0) != shrK(X1)
    | X0 = X1 ) ).

cnf(u9403,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X2)))))) ) ).

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

cnf(u6764,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X9)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9))))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u8807,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u21732,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0)))),analz(knows(spy,X1))) ) ).

cnf(u6433,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u9493,axiom,
    ( ~ member(msg,mPair(X0,X13),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

cnf(u10322,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u58393,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X1))) ) ).

cnf(u9807,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

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

cnf(u11203,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X11,X0))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

cnf(u58042,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X6)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X6)))
    | ~ member(nat,X0,symKeys) ) ).

cnf(u5349,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u10409,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u10383,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X2)))))) ) ).

cnf(u9375,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u1401,hypothesis,
    member(msg,agent1(b),parts(used(evs))) ).

cnf(u8902,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

cnf(u931,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,evs))) ).

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

cnf(u5334,axiom,
    ( ~ member(msg,crypt(X5,X0),knows(spy,X4))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),X4)))) ) ).

cnf(u1075,hypothesis,
    member(msg,crypt(k,mPair(nonce(nb),nonce(nb))),used(evs)) ).

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

cnf(u1600,axiom,
    ~ nS_Sha993195050haredp(cons(event,says(X0,X1,X2),X3)) ).

cnf(u976,hypothesis,
    member(msg,nonce(na),parts(knows(spy,evs))) ).

cnf(u18241,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X8)))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u6003,axiom,
    ( ~ member(msg,mPair(X0,X10),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u8457,axiom,
    ( ~ member(msg,mPair(X0,X11),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X10))))))) ) ).

cnf(u6139,axiom,
    ( ~ member(msg,crypt(X0,X1),knows(spy,X4))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),knows(spy,X4)) ) ).

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

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

cnf(u1403,hypothesis,
    member(msg,agent1(b),analz(used(evs))) ).

cnf(u7500,axiom,
    ( ~ member(msg,mPair(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ) ).

cnf(u9424,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u9381,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X2)))))) ) ).

cnf(u10364,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1))),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

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

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

cnf(u43720,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1)))),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2))))) ) ).

cnf(u58102,axiom,
    ( ~ member(msg,key(X6),analz(knows(spy,X5)))
    | ~ member(nat,X6,symKeys)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(X6,X0),knows(spy,X5)) ) ).

cnf(u10293,axiom,
    ( ~ member(msg,crypt(shrK(X5),X0),knows(spy,X4))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(msg,key(shrK(X5)),knows(spy,X4)) ) ).

cnf(u9814,axiom,
    ( ~ member(msg,crypt(shrK(X9),X0),knows(spy,X8))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u22913,axiom,
    ( ~ member(msg,crypt(shrK(X10),X0),knows(spy,X9))
    | ~ member(agent,X10,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u1609,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X5)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(agent,X0,bad) ) ).

cnf(u18406,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u23866,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1)))),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

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

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

cnf(u6448,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u224,axiom,
    ( member(msg,key(shrK(X1)),knows(spy,X0))
    | ~ member(agent,X1,bad) ) ).

cnf(u5307,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u2681,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X6))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u2670,axiom,
    ( ~ member(msg,crypt(shrK(X6),X0),analz(knows(spy,X5)))
    | ~ member(agent,X6,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u11149,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1))),analz(knows(spy,X6)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u284,axiom,
    mPair(X2,X1) != agent1(X0) ).

cnf(u42431,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X1))) ) ).

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

cnf(u11193,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u9491,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X12)),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u10402,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),cons(event,says(X12,X13,X14),X2))))))) ) ).

cnf(u5377,axiom,
    ( ~ member(msg,crypt(X8,X0),analz(knows(spy,X7)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u221,axiom,
    ( ~ member(msg,key(shrK(X0)),parts(knows(spy,X1)))
    | member(agent,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u9475,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X11)),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u10387,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),cons(event,says(X12,X13,X14),X2))))))) ) ).

cnf(u349,hypothesis,
    member(msg,crypt(shrK(a),mPair(nonce(na),mPair(agent1(b),mPair(key(k),x)))),parts(knows(spy,evs))) ).

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

cnf(u5419,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

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

cnf(u6397,axiom,
    ( ~ member(msg,mPair(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u1298,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X1,parts(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u11196,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u12186,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u6525,axiom,
    ( ~ member(msg,mPair(X0,X9),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u2967,axiom,
    member(msg,mPair(X0,mPair(agent1(X1),mPair(key(X2),X3))),parts(knows(server,X4))) ).

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

cnf(u9488,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u54062,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))) ).

cnf(u10388,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X2)))))) ) ).

cnf(u6460,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u50950,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X1))) ) ).

cnf(u345,axiom,
    ( ~ member(msg,X1,parts(knows(spy,X0)))
    | member(msg,X1,used(X0)) ) ).

cnf(u10373,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

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

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

cnf(u292,axiom,
    nonce(X1) != agent1(X0) ).

cnf(u9480,axiom,
    ( ~ member(msg,mPair(X0,X11),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u5295,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u5332,axiom,
    ( ~ member(msg,crypt(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u1332,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(X1))
    | member(msg,X2,analz(X1))
    | ~ member(msg,crypt(shrK(X0),X2),X1) ) ).

cnf(u1027,hypothesis,
    member(msg,key(k),parts(knows(spy,evs))) ).

cnf(u12167,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1))),analz(knows(spy,X7)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),X7)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u59397,axiom,
    ( ~ member(msg,key(X0),knows(spy,cons(event,says(X3,X4,X5),X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2))) ) ).

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

cnf(u7687,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X9)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u1680,axiom,
    ( ~ member(msg,mPair(X6,X0),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

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

cnf(u9417,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X2))))))) ) ).

cnf(u1438,axiom,
    member(msg,X0,analz(used(X1))) ).

cnf(u21513,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))) ) ).

cnf(u16935,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))) ) ).

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

cnf(u5278,axiom,
    ( ~ member(msg,crypt(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u5421,axiom,
    ( ~ member(msg,crypt(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u6326,hypothesis,
    ~ member(msg,crypt(k,nonce(X0)),parts(knows(spy,evs))) ).

cnf(u11155,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1))),analz(knows(spy,X7)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),X7)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u6540,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u10764,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X7))),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u10599,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,parts(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u225,axiom,
    member(msg,key(shrK(X1)),knows(X1,X0)) ).

cnf(u6528,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u11178,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u22897,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u10752,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X6))),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u9781,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(X0)),knows(spy,X4))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X4)))
    | ~ member(nat,X0,symKeys) ) ).

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

cnf(u327,axiom,
    ( member(msg,X4,analz(knows(spy,cons(event,says(X3,X2,X1),X0))))
    | ~ member(msg,X4,analz(knows(spy,X0))) ) ).

cnf(u9502,axiom,
    ( ~ member(msg,crypt(shrK(X11),X0),analz(knows(spy,X10)))
    | ~ member(agent,X11,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X10))))))) ) ).

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

cnf(u52220,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),cons(event,says(X12,X13,X14),X15))))))))) ).

cnf(u8035,axiom,
    ( ~ member(msg,crypt(shrK(X4),X0),analz(knows(spy,X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,key(shrK(X4)),analz(knows(spy,X3))) ) ).

cnf(u7929,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X11)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X11))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u18249,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u8454,axiom,
    ( ~ member(msg,mPair(X0,X10),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ) ).

cnf(u9079,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

cnf(u352,hypothesis,
    ~ member(agent,b,bad) ).

cnf(u2783,axiom,
    ( ~ member(msg,mPair(X0,X7),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

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

cnf(u43202,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X4)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4)))) ) ).

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

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

cnf(u9766,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X4))),knows(spy,X3))
    | ~ member(msg,crypt(shrK(X4),X0),analz(knows(spy,X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

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

cnf(u43221,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X7))) ) ).

cnf(u43134,axiom,
    ( ~ member(msg,key(shrK(X0)),knows(spy,cons(event,says(X3,X4,X5),X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2))) ) ).

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

cnf(u8040,axiom,
    ( ~ member(msg,key(shrK(X4)),knows(spy,cons(event,notes(X1,X2),X3)))
    | ~ member(msg,crypt(shrK(X4),X0),analz(knows(spy,X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u20259,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),key(shrK(X0))),analz(knows(spy,X2))) ) ).

cnf(u2750,axiom,
    ( ~ member(msg,mPair(X8,X0),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

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

cnf(u50949,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X1))) ) ).

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

cnf(u6484,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u6472,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u10410,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u6400,axiom,
    ( ~ member(msg,mPair(X0,X9),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u10384,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

cnf(u2671,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | ~ member(agent,X7,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u9402,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

cnf(u9476,axiom,
    ( ~ member(msg,mPair(X0,X11),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u51769,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X11))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u58144,axiom,
    ( ~ member(msg,crypt(X0,X1),knows(spy,X6))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),knows(spy,X6)) ) ).

cnf(u1021,hypothesis,
    member(msg,agent1(b),parts(knows(spy,evs))) ).

cnf(u9407,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),cons(event,notes(X12,X13),X2))))))) ) ).

cnf(u9420,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),cons(event,notes(X11,X12),X2))))))) ) ).

cnf(u2825,axiom,
    ( ~ member(msg,mPair(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

cnf(u5501,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u10381,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

cnf(u42391,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),X1)))))
    | ~ member(msg,crypt(shrK(spy),X0),analz(knows(spy,X1))) ) ).

cnf(u1082,hypothesis,
    member(msg,nonce(nb),used(evs)) ).

cnf(u43220,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X7))) ) ).

cnf(u18259,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u54079,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),cons(event,notes(X11,X12),cons(event,notes(X13,X14),X15))))))))) ).

cnf(u1546,axiom,
    ( ~ member(msg,crypt(shrK(X0),X2),knows(spy,cons(event,says(X3,X4,X5),X1)))
    | member(msg,X2,analz(knows(spy,cons(event,says(X3,X4,X5),X1))))
    | ~ member(msg,key(shrK(X0)),analz(knows(spy,X1))) ) ).

cnf(u6409,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u9497,axiom,
    ( ~ member(msg,mPair(X0,X14),analz(knows(spy,X13)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,says(X10,X11,X12),X13))))))) ) ).

cnf(u9376,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u342,axiom,
    ( ~ member(msg,mPair(X2,X1),used(X0))
    | member(msg,X2,used(X0)) ) ).

cnf(u5337,hypothesis,
    member(msg,nonce(na),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u10389,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

cnf(u1547,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u7937,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X8))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),X8)))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u11198,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u9489,axiom,
    ( ~ member(msg,mPair(X0,X13),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

cnf(u58394,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X1))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X1))) ) ).

cnf(u22319,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u11183,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X10,X0))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u22903,axiom,
    ( ~ member(msg,crypt(shrK(X10),X0),knows(spy,X9))
    | ~ member(agent,X10,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

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

cnf(u297,axiom,
    ( ~ member(msg,crypt(shrK(X2),X1),analz(X0))
    | ~ member(msg,key(shrK(X2)),analz(X0))
    | member(msg,X1,analz(X0)) ) ).

cnf(u5319,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u42841,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X2))) ) ).

cnf(u43207,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8))))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0)))),analz(knows(spy,X8))) ) ).

cnf(u5692,axiom,
    ( ~ member(msg,mPair(X0,X8),analz(knows(spy,X7)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u59656,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u9405,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X2)))))) ) ).

cnf(u59699,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u18247,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X9)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u5378,axiom,
    ( ~ member(msg,crypt(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X8)))))) ) ).

cnf(u6006,axiom,
    ( ~ member(msg,mPair(X0,X11),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

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

cnf(u1541,axiom,
    ( member(msg,X0,parts(knows(spy,cons(event,says(X2,X3,X4),X1))))
    | ~ member(msg,X0,analz(knows(spy,X1))) ) ).

cnf(u6552,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,says(X3,X4,X5),evs))))) ).

cnf(u350,hypothesis,
    ~ member(msg,key(k),analz(knows(spy,evs))) ).

cnf(u20260,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,key(shrK(X0)),analz(knows(spy,X2))) ) ).

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

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

cnf(u10761,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X8,X0))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u24000,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

cnf(u5224,axiom,
    ( ~ member(msg,crypt(X5,X0),analz(knows(spy,X4)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),X4)))) ) ).

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

cnf(u18261,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

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

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

cnf(u6447,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u7702,axiom,
    ( ~ member(msg,mPair(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u9379,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

cnf(u10325,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

cnf(u5686,axiom,
    ( ~ member(msg,mPair(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

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

cnf(u10318,axiom,
    ( ~ member(msg,key(X0),analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u1748,axiom,
    ( ~ member(msg,crypt(X0,X1),knows(spy,cons(event,notes(X2,X3),X4)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),analz(knows(spy,X4))) ) ).

cnf(u9479,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X11)),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u9372,axiom,
    ( ~ member(msg,key(X0),analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

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

cnf(u1749,axiom,
    ( ~ member(msg,crypt(X0,X1),knows(spy,cons(event,says(X2,X3,X4),X5)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(nat,X0,symKeys)
    | ~ member(msg,key(X0),analz(knows(spy,X5))) ) ).

cnf(u43924,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2))))) ) ).

cnf(u20311,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X5))) ) ).

cnf(u1377,hypothesis,
    member(msg,nonce(nb),parts(used(evs))) ).

cnf(u10423,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12)))))))) ) ).

cnf(u9485,axiom,
    ( ~ member(msg,mPair(X0,X13),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

cnf(u1167,axiom,
    ( ~ member(msg,key(shrK(X0)),knows(spy,X1))
    | ~ member(list(event),X1,nS_Sha254967238shared)
    | member(agent,X0,bad) ) ).

cnf(u31128,axiom,
    ( ~ member(msg,key(X5),analz(knows(spy,X4)))
    | ~ member(nat,X5,symKeys)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(msg,crypt(X5,X0),knows(spy,X4)) ) ).

cnf(u10404,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u1083,hypothesis,
    member(msg,nonce(na),used(evs)) ).

cnf(u7504,axiom,
    ( ~ member(msg,mPair(X11,X0),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X10))))))) ) ).

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

cnf(u5694,axiom,
    ( ~ member(event,says(server,X4,crypt(shrK(X4),mPair(X3,mPair(agent1(X2),mPair(key(X5),X1))))),set(event,X6))
    | ~ member(msg,crypt(X5,nonce(X0)),parts(knows(spy,X6)))
    | member(msg,key(X5),analz(knows(spy,X6)))
    | ~ member(list(event),X6,nS_Sha254967238shared) ) ).

cnf(u10408,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u5678,axiom,
    ( ~ member(msg,mPair(X6,X0),analz(knows(spy,X5)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

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

cnf(u9812,axiom,
    ( ~ member(msg,crypt(shrK(X11),X0),analz(knows(spy,X10)))
    | ~ member(agent,X11,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u1078,hypothesis,
    member(msg,mPair(nonce(nb),nonce(nb)),used(evs)) ).

cnf(u1607,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X4)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u5348,hypothesis,
    member(msg,mPair(key(k),x),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u5909,axiom,
    ( ~ member(msg,mPair(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u2679,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X8)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8))))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u5333,axiom,
    ( ~ member(msg,crypt(X8,X0),analz(knows(spy,X7)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u5461,axiom,
    ( ~ member(msg,crypt(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u581,hypothesis,
    ~ member(msg,key(k),knows(spy,evs)) ).

cnf(u20310,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X5))) ) ).

cnf(u351,hypothesis,
    ~ member(agent,a,bad) ).

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

cnf(u11191,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u9618,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X4,X0)),knows(spy,X3))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u22907,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u54064,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),cons(event,notes(X11,X12),X13)))))))) ).

cnf(u9820,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,key(shrK(X0)),analz(knows(spy,X2))) ) ).

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

cnf(u6471,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,notes(X0,X1),cons(event,says(X2,X3,X4),evs))))) ).

cnf(u5906,axiom,
    ( ~ member(msg,mPair(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u9821,axiom,
    ( ~ member(msg,key(shrK(X0)),knows(spy,cons(event,says(X3,X4,X5),X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X2))) ) ).

cnf(u5318,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,notes(X0,X1),evs)))) ).

cnf(u10321,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u59290,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u972,hypothesis,
    member(msg,nonce(nb),parts(knows(spy,evs))) ).

cnf(u5274,axiom,
    ( ~ member(msg,mPair(X0,X7),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u5502,axiom,
    ( ~ member(msg,crypt(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u9813,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u1334,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | member(msg,X4,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,crypt(shrK(X0),X4),analz(knows(spy,X3))) ) ).

cnf(u6117,axiom,
    ( ~ member(msg,key(X6),analz(knows(spy,cons(event,notes(X3,X4),X5))))
    | ~ member(nat,X6,symKeys)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5)))))
    | ~ member(msg,crypt(X6,X0),analz(knows(spy,X5))) ) ).

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

cnf(u1239,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u9408,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X2)))))) ) ).

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

cnf(u6366,hypothesis,
    ( ~ member(msg,crypt(shrK(X0),mPair(key(k),agent1(X1))),parts(knows(spy,evs)))
    | member(agent,X0,bad)
    | a = X1 ) ).

cnf(u10405,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,says(X9,X10,X11),X2))))))) ) ).

cnf(u290,axiom,
    agent1(X0) != crypt(X2,X1) ).

cnf(u9806,axiom,
    ( ~ member(msg,crypt(shrK(X11),X0),analz(knows(spy,X10)))
    | ~ member(agent,X11,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u42276,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X6))),analz(knows(spy,X5)))
    | ~ member(msg,crypt(shrK(X6),X0),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u50842,axiom,
    ( ~ member(msg,crypt(shrK(spy),key(shrK(X7))),analz(knows(spy,X6)))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

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

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

cnf(u1721,axiom,
    ( ~ member(msg,key(X0),analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(nat,X0,symKeys)
    | member(msg,X4,analz(knows(spy,cons(event,notes(X1,X2),X3))))
    | ~ member(msg,crypt(X0,X4),analz(knows(spy,X3))) ) ).

cnf(u6523,axiom,
    ( ~ member(msg,mPair(X0,X10),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u10398,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u227,axiom,
    member(agent,spy,bad) ).

cnf(u9350,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),X1))))
    | ~ member(msg,crypt(shrK(spy),X0),analz(knows(spy,X1))) ) ).

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

cnf(u6765,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X10)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u43955,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1)))),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2))))) ) ).

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

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

cnf(u59613,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X12))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u6497,hypothesis,
    member(msg,agent1(b),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u20321,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X6))) ) ).

cnf(u220,axiom,
    ( member(msg,key(shrK(X0)),analz(knows(spy,X1)))
    | ~ member(agent,X0,bad)
    | ~ member(list(event),X1,nS_Sha254967238shared) ) ).

cnf(u10386,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u3174,axiom,
    ( ~ member(event,says(server,X4,crypt(shrK(X4),mPair(nonce(X1),mPair(agent1(X5),mPair(key(X3),X0))))),set(event,X6))
    | ~ member(event,says(X5,X4,crypt(X3,nonce(X2))),set(event,X6))
    | ~ nS_Sha993195050haredp(X6) ) ).

cnf(u6432,hypothesis,
    member(msg,x,parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u2965,axiom,
    ( ~ member(msg,key(shrK(X5)),knows(server,X4))
    | member(msg,mPair(X0,mPair(agent1(X1),mPair(key(X2),X3))),analz(knows(server,X4))) ) ).

cnf(u8468,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u1400,hypothesis,
    member(msg,mPair(key(k),x),parts(used(evs))) ).

cnf(u5279,axiom,
    ( ~ member(msg,crypt(X4,X0),knows(spy,X3))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u333,axiom,
    ( ~ member(list(event),X0,nS_Sha254967238shared)
    | nS_Sha993195050haredp(X0) ) ).

cnf(u1373,hypothesis,
    member(msg,key(k),analz(used(evs))) ).

cnf(u50851,axiom,
    ( ~ member(msg,key(shrK(X7)),knows(spy,cons(event,notes(X4,X5),X6)))
    | ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u29535,axiom,
    ( ~ member(msg,crypt(shrK(X11),X0),knows(spy,X10))
    | ~ member(agent,X11,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),X10)))))) ) ).

cnf(u10299,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(msg,crypt(shrK(spy),X0),analz(knows(spy,X4))) ) ).

cnf(u9472,axiom,
    ( ~ member(msg,mPair(X0,X11),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u9614,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X6,X0))),analz(knows(spy,X5)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u10326,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,says(X8,X9,X10),X2)))))) ) ).

cnf(u10372,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),X2))))) ) ).

cnf(u3304,hypothesis,
    ( ~ member(msg,crypt(shrK(X0),mPair(X2,mPair(agent1(X3),mPair(key(k),X1)))),knows(spy,evs))
    | x = X1
    | member(agent,X0,bad) ) ).

cnf(u5277,axiom,
    ( ~ member(msg,crypt(X6,X0),analz(knows(spy,X5)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

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

cnf(u6396,axiom,
    ( ~ member(msg,mPair(X8,X0),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u58249,axiom,
    ( ~ member(msg,key(shrK(X7)),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(X7),X0),knows(spy,X6)) ) ).

cnf(u9409,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

cnf(u1370,hypothesis,
    member(msg,x,parts(used(evs))) ).

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

cnf(u6509,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,says(X0,X1,X2),cons(event,notes(X3,X4),evs))))) ).

cnf(u43923,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2))))) ) ).

cnf(u2970,axiom,
    member(msg,X0,parts(knows(server,X1))) ).

cnf(u20306,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X3)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

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

cnf(u15243,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X9),X0))),analz(knows(spy,X8)))
    | ~ member(agent,X9,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

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

cnf(u10767,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X8))),analz(knows(spy,X7)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u10401,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),cons(event,says(X11,X12,X13),X2))))))) ) ).

cnf(u58296,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),knows(spy,X6))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,key(shrK(X7)),knows(spy,X6)) ) ).

cnf(u54068,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),cons(event,notes(X12,X13),cons(event,notes(X14,X15),X16))))))))) ).

cnf(u51813,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X11))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11)))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u50869,axiom,
    ( ~ member(msg,key(shrK(X7)),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(X7),X0),knows(spy,X6)) ) ).

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

cnf(u50843,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,key(shrK(X7)),analz(knows(spy,X6))) ) ).

cnf(u1238,axiom,
    ( ~ member(msg,mPair(X0,X1),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u2823,axiom,
    ( ~ member(msg,mPair(X10,X0),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

cnf(u5688,axiom,
    ( ~ member(msg,mPair(X8,X0),analz(knows(spy,X7)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),X7))))) ) ).

cnf(u20268,axiom,
    ( ~ member(msg,key(shrK(X0)),knows(spy,cons(event,notes(X3,X4),X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2))) ) ).

cnf(u9484,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u10413,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2)))) ) ).

cnf(u9071,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u54081,axiom,
    member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),cons(event,notes(X11,X12),cons(event,notes(X13,X14),X15))))))))) ).

cnf(u58345,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),X1)))))
    | ~ member(msg,crypt(shrK(spy),X0),analz(knows(spy,X1))) ) ).

cnf(u9378,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X2)))))) ) ).

cnf(u22893,axiom,
    ( ~ member(msg,crypt(shrK(X10),X0),knows(spy,X9))
    | ~ member(agent,X10,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u336,axiom,
    member(nat,shrK(X0),symKeys) ).

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

cnf(u10406,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u2672,axiom,
    ( ~ member(msg,crypt(shrK(X4),X0),knows(spy,X3))
    | ~ member(agent,X4,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),X3)))) ) ).

cnf(u20320,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),X0))),analz(knows(spy,X6))) ) ).

cnf(u1073,axiom,
    ( ~ member(msg,X0,knows(spy,X1))
    | member(msg,X0,used(X1)) ) ).

cnf(u13918,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),X9))))))) ) ).

cnf(u9401,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X2)))))) ) ).

cnf(u9772,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11)))))))) ) ).

cnf(u29809,axiom,
    ( ~ member(msg,key(X0),knows(spy,cons(event,says(X2,X3,X4),X5)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),X5))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X5)))
    | ~ member(nat,X0,symKeys) ) ).

cnf(u9383,axiom,
    ( ~ member(msg,key(shrK(X0)),analz(knows(spy,cons(event,notes(X3,X4),X2))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),X2)))) ) ).

cnf(u2673,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | ~ member(agent,X7,bad)
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u44158,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X1)))),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2))))) ) ).

cnf(u10288,axiom,
    ( ~ member(msg,key(shrK(X5)),analz(knows(spy,X4)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),X4))))
    | ~ member(msg,crypt(shrK(X5),X0),knows(spy,X4)) ) ).

cnf(u348,hypothesis,
    member(msg,crypt(k,mPair(nonce(nb),nonce(nb))),parts(knows(spy,evs))) ).

cnf(u11188,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),X9)))))) ) ).

cnf(u9419,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,notes(X10,X11),X2))))))) ) ).

cnf(u1388,hypothesis,
    member(msg,mPair(nonce(nb),nonce(nb)),parts(used(evs))) ).

cnf(u18413,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X10)))),analz(knows(spy,X9)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,notes(X7,X8),X9)))))) ) ).

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

cnf(u10327,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X2)))))) ) ).

cnf(u9503,axiom,
    ( ~ member(msg,crypt(shrK(X8),X0),knows(spy,X7))
    | ~ member(agent,X8,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),X7)))))) ) ).

cnf(u5741,axiom,
    ( ~ member(msg,mPair(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u15523,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X11))),analz(knows(spy,X10)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,notes(X8,X9),X10))))))) ) ).

cnf(u5376,hypothesis,
    member(msg,mPair(nonce(na),mPair(agent1(b),mPair(key(k),x))),parts(knows(spy,cons(event,notes(X0,X1),cons(event,notes(X2,X3),evs))))) ).

cnf(u9360,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,parts(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u344,axiom,
    member(msg,key(shrK(X1)),used(X0)) ).

cnf(u5420,axiom,
    ( ~ member(msg,crypt(X9,X0),analz(knows(spy,X8)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u1081,hypothesis,
    member(msg,mPair(key(k),x),used(evs)) ).

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

cnf(u9473,axiom,
    ( ~ member(msg,mPair(X0,X12),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,says(X5,X6,X7),cons(event,says(X8,X9,X10),X11))))))) ) ).

cnf(u12172,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1))),analz(knows(spy,X8)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,says(X5,X6,X7),X8)))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u5379,axiom,
    ( ~ member(msg,crypt(X6,X0),knows(spy,X5))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u9391,axiom,
    ( ~ member(msg,crypt(X0,X2),knows(spy,cons(event,notes(X3,X4),X1)))
    | ~ member(nat,X0,symKeys)
    | member(msg,X2,analz(knows(spy,cons(event,notes(X3,X4),X1))))
    | ~ member(msg,crypt(shrK(spy),key(X0)),analz(knows(spy,X1))) ) ).

cnf(u52185,axiom,
    member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),cons(event,says(X11,X12,X13),X14))))))))) ).

cnf(u43124,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),X2))))
    | ~ member(msg,crypt(shrK(spy),key(shrK(X0))),analz(knows(spy,X2))) ) ).

cnf(u6766,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),knows(spy,X7))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),cons(event,says(X4,X5,X6),X7)))))
    | ~ member(agent,X0,bad) ) ).

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

cnf(u2530,axiom,
    ( ~ member(msg,key(X0),knows(spy,cons(event,notes(X2,X3),X4)))
    | member(msg,X1,analz(knows(spy,cons(event,notes(X2,X3),X4))))
    | ~ member(msg,crypt(X0,X1),analz(knows(spy,X4)))
    | ~ member(nat,X0,symKeys) ) ).

cnf(u22195,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(X0),X1)))),analz(knows(spy,X2)))
    | ~ member(agent,X0,bad)
    | member(msg,X1,analz(knows(spy,cons(event,notes(X3,X4),cons(event,notes(X5,X6),X2))))) ) ).

cnf(u5336,hypothesis,
    member(msg,mPair(agent1(b),mPair(key(k),x)),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

cnf(u1372,hypothesis,
    member(msg,x,analz(used(evs))) ).

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

cnf(u2748,axiom,
    ( ~ member(msg,mPair(X7,X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u10376,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2))))) ) ).

cnf(u43204,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),X0)),analz(knows(spy,X6))) ) ).

cnf(u9495,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X13)),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,says(X4,X5,X6),cons(event,says(X7,X8,X9),cons(event,notes(X10,X11),X12))))))) ) ).

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

cnf(u12181,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),crypt(shrK(spy),mPair(X9,X0)))),analz(knows(spy,X8)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X8)))))) ) ).

cnf(u9396,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),X2))))) ) ).

cnf(u5361,hypothesis,
    member(msg,key(k),parts(knows(spy,cons(event,says(X0,X1,X2),evs)))) ).

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

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

cnf(u10755,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(spy),mPair(X0,X7))),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6))))) ) ).

cnf(u5682,axiom,
    ( ~ member(msg,mPair(X0,X6),analz(knows(spy,X5)))
    | member(msg,X0,parts(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),X5))))) ) ).

cnf(u930,hypothesis,
    member(msg,mPair(nonce(nb),nonce(nb)),parts(knows(spy,evs))) ).

cnf(u22887,axiom,
    ( ~ member(msg,crypt(shrK(X12),X0),analz(knows(spy,X11)))
    | ~ member(agent,X12,bad)
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),cons(event,notes(X9,X10),X11))))))) ) ).

cnf(u9509,axiom,
    ( ~ member(msg,mPair(X12,X0),analz(knows(spy,X11)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,notes(X3,X4),cons(event,notes(X5,X6),cons(event,notes(X7,X8),cons(event,notes(X9,X10),X11)))))))) ) ).

cnf(u7692,axiom,
    ( ~ member(msg,crypt(shrK(X0),X1),analz(knows(spy,X10)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),cons(event,says(X7,X8,X9),X10))))))
    | ~ member(agent,X0,bad) ) ).

cnf(u50907,axiom,
    ( member(msg,X0,analz(knows(spy,cons(event,says(X2,X3,X4),cons(event,notes(X5,X6),X1)))))
    | ~ member(msg,crypt(shrK(spy),X0),analz(knows(spy,X1))) ) ).

cnf(u10775,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(X5,X0)),knows(spy,X4))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),X4)))) ) ).

cnf(u58191,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),analz(knows(spy,X6)))
    | member(msg,X0,analz(knows(spy,cons(event,notes(X1,X2),cons(event,says(X3,X4,X5),X6)))))
    | ~ member(msg,key(shrK(X7)),analz(knows(spy,X6))) ) ).

cnf(u10323,axiom,
    ( ~ member(msg,crypt(shrK(spy),crypt(shrK(X0),X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,says(X6,X7,X8),X2)))))
    | ~ member(agent,X0,bad) ) ).

cnf(u9258,axiom,
    ( ~ member(msg,mPair(X13,X0),analz(knows(spy,X12)))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),cons(event,says(X6,X7,X8),cons(event,says(X9,X10,X11),X12))))))) ) ).

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

cnf(u10399,axiom,
    ( ~ member(msg,crypt(shrK(spy),mPair(X0,X1)),analz(knows(spy,X2)))
    | member(msg,X1,analz(knows(spy,cons(event,says(X3,X4,X5),cons(event,notes(X6,X7),cons(event,notes(X8,X9),cons(event,says(X10,X11,X12),X2))))))) ) ).

cnf(u5690,axiom,
    ( ~ member(msg,mPair(X0,X7),analz(knows(spy,X6)))
    | member(msg,X0,parts(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6))))) ) ).

cnf(u50887,axiom,
    ( ~ member(msg,crypt(shrK(X7),X0),knows(spy,X6))
    | member(msg,X0,analz(knows(spy,cons(event,says(X1,X2,X3),cons(event,notes(X4,X5),X6)))))
    | ~ member(msg,key(shrK(X7)),knows(spy,X6)) ) ).

cnf(u1325,axiom,
    ~ nS_Sha993195050haredp(cons(event,notes(X0,X1),X2)) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWV795_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.04  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.16  % Computer : n004.cluster.edu
% 0.07/0.16  % Model    : x86_64 x86_64
% 0.07/0.16  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.16  % Memory   : 8046.5625MB
% 0.07/0.16  % OS       : Linux 6.8.0-71-generic
% 0.07/0.16  % CPULimit : 300
% 0.07/0.16  % WCLimit  : 300
% 0.07/0.16  % DateTime : Mon Sep 28 12:34:52 UTC 2026
% 0.07/0.16  % CPUTime  : 
% 0.07/0.16  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19  Running first-order model finding
% 0.07/0.19  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.06/1.48  % (323482)Will run a generic schedule for satisfiability detection.
% 8.06/1.48  % (323491)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1273089711:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.06/1.48  % (323488)% WARNING: option uhcvi not known.
% 8.06/1.48  % (323487)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3905923386_2999 on theBenchmark for (2999ds/0Mi)
% 8.06/1.48  % (323489)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=511234496:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.06/1.48  % (323493)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1122220176:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.06/1.48  % (323490)dis+10_1_sil=32000:sp=arity:random_seed=2153832739:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.06/1.48  % (323492)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1147726923:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.06/1.48  % (323488)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1354998196:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.06/1.48  % Exception at run slice level
% 8.06/1.48  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.06/1.48  % (323501)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2086242872:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.06/1.48  % (323491)Instruction limit reached! 
% 8.06/1.48  % (323491)------------------------------
% 8.06/1.48  % (323491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.06/1.48  % (323491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/1.48  % (323491)CaDiCaL version: 2.1.3
% 8.06/1.48  % (323491)Termination reason: Instruction limit
% 8.06/1.48  % (323491)Termination phase: Saturation
% 8.06/1.48  % (323491)Time elapsed: 0.035 s
% 8.06/1.48  % (323491)Peak memory usage: 12 MB
% 8.06/1.48  % (323491)Instructions burned: 117 (million)
% 8.06/1.48  % Exception at run slice level
% 8.06/1.48  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.06/1.48  % (323503)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3561534312:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.06/1.48  % (323504)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=576401652:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 8.06/1.48  % (323490)Instruction limit reached! 
% 8.06/1.48  % (323490)------------------------------
% 8.06/1.48  % (323490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.06/1.48  % (323490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/1.48  % (323490)CaDiCaL version: 2.1.3
% 8.06/1.48  % (323490)Termination reason: Instruction limit
% 8.06/1.48  % (323490)Termination phase: Saturation
% 8.06/1.48  % (323490)Time elapsed: 0.061 s
% 8.06/1.48  % (323490)Peak memory usage: 12 MB
% 8.06/1.48  % (323490)Instructions burned: 104 (million)
% 8.06/1.48  % (323492)Instruction limit reached! 
% 8.06/1.48  % (323492)------------------------------
% 8.06/1.48  % (323492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.06/1.48  % (323492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/1.48  % (323492)CaDiCaL version: 2.1.3
% 8.06/1.48  % (323492)Termination reason: Instruction limit
% 8.06/1.48  % (323492)Termination phase: Saturation
% 8.06/1.48  % (323492)Time elapsed: 0.073 s
% 8.06/1.48  % (323492)Peak memory usage: 12 MB
% 8.06/1.48  % (323492)Instructions burned: 131 (million)
% 8.06/1.48  % (323507)ott-21_1_sil=16000:fs=off:random_seed=696677482:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 8.06/1.48  % (323508)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=291731270:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.06/1.48  % (323493)Instruction limit reached! 
% 8.06/1.48  % (323493)------------------------------
% 8.06/1.48  % (323493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.06/1.48  % (323493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/1.48  % (323493)CaDiCaL version: 2.1.3
% 8.06/1.48  % (323493)Termination reason: Instruction limit
% 8.06/1.48  % (323493)Termination phase: Saturation
% 8.06/1.48  % (323493)Time elapsed: 0.096 s
% 8.06/1.48  % (323493)Peak memory usage: 13 MB
% 21.92/3.33  % (323493)Instructions burned: 159 (million)
% 21.92/3.33  % (323511)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3676712270:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 21.92/3.33  % Exception at run slice level
% 21.92/3.33  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.92/3.33  % (323503)Instruction limit reached! 
% 21.92/3.33  % (323503)------------------------------
% 21.92/3.33  % (323503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.92/3.33  % (323503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.92/3.33  % (323503)CaDiCaL version: 2.1.3
% 21.92/3.33  % (323503)Termination reason: Instruction limit
% 21.92/3.33  % (323503)Termination phase: Saturation
% 21.92/3.33  % (323503)Time elapsed: 0.075 s
% 21.92/3.33  % (323503)Peak memory usage: 13 MB
% 21.92/3.33  % (323503)Instructions burned: 132 (million)
% 21.92/3.33  % (323513)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=421922755:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 21.92/3.33  % (323514)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1687939054:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 21.92/3.33  % Exception at run slice level
% 21.92/3.33  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.92/3.33  % (323507)Instruction limit reached! 
% 21.92/3.33  % (323507)------------------------------
% 21.92/3.33  % (323507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.92/3.33  % (323507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.92/3.33  % (323507)CaDiCaL version: 2.1.3
% 21.92/3.33  % (323507)Termination reason: Instruction limit
% 21.92/3.33  % (323507)Termination phase: Saturation
% 21.92/3.33  % (323507)Time elapsed: 0.067 s
% 21.92/3.33  % (323507)Peak memory usage: 11 MB
% 21.92/3.33  % (323507)Instructions burned: 182 (million)
% 21.92/3.33  % (323517)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3440163108:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 21.92/3.33  % (323518)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2077543153:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 21.92/3.33  % (323508)Instruction limit reached! 
% 21.92/3.33  % (323508)------------------------------
% 21.92/3.33  % (323508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.92/3.33  % (323508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.92/3.33  % (323508)CaDiCaL version: 2.1.3
% 21.92/3.33  % (323508)Termination reason: Instruction limit
% 21.92/3.33  % (323508)Termination phase: Saturation
% 21.92/3.33  % (323508)Time elapsed: 0.282 s
% 21.92/3.33  % (323508)Peak memory usage: 14 MB
% 21.92/3.33  % (323508)Instructions burned: 479 (million)
% 21.92/3.33  % (323521)fmb+10_1_sil=64000:random_seed=1273986875:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 21.92/3.33  % (323521)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 21.92/3.33  % Exception at run slice level
% 21.92/3.33  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.92/3.33  % (323523)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3576377947:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 21.92/3.33  % Exception at run slice level
% 21.92/3.33  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.92/3.33  % (323525)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1343262992:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 21.92/3.33  % (323504)Instruction limit reached! 
% 21.92/3.33  % (323504)------------------------------
% 21.92/3.33  % (323504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.92/3.33  % (323504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.92/3.33  % (323504)CaDiCaL version: 2.1.3
% 21.92/3.33  % (323504)Termination reason: Instruction limit
% 21.92/3.33  % (323504)Termination phase: Saturation
% 21.92/3.33  % (323504)Time elapsed: 0.392 s
% 21.92/3.33  % (323504)Peak memory usage: 16 MB
% 21.92/3.33  % (323504)Instructions burned: 684 (million)
% 21.92/3.33  % Exception at run slice level
% 21.92/3.33  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 84.67/12.14  % (323527)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=85865319:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 84.67/12.14  % (323528)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=105292229:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 84.67/12.14  % (323528)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 84.67/12.14  % (323517)Instruction limit reached! 
% 84.67/12.14  % (323517)------------------------------
% 84.67/12.14  % (323517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.67/12.14  % (323517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.67/12.14  % (323517)CaDiCaL version: 2.1.3
% 84.67/12.14  % (323517)Termination reason: Instruction limit
% 84.67/12.14  % (323517)Termination phase: Saturation
% 84.67/12.14  % (323517)Time elapsed: 0.376 s
% 84.67/12.14  % (323517)Peak memory usage: 18 MB
% 84.67/12.14  % (323517)Instructions burned: 694 (million)
% 84.67/12.14  % (323531)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=444624595:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 84.67/12.14  % Exception at run slice level
% 84.67/12.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 84.67/12.14  % (323533)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3599769370:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 84.67/12.14  % Exception at run slice level
% 84.67/12.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 84.67/12.14  % (323535)ott-2_1_sil=16000:newcnf=on:random_seed=1346694653:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 84.67/12.14  % (323518)Instruction limit reached! 
% 84.67/12.14  % (323518)------------------------------
% 84.67/12.14  % (323518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.67/12.14  % (323518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.67/12.14  % (323518)CaDiCaL version: 2.1.3
% 84.67/12.14  % (323518)Termination reason: Instruction limit
% 84.67/12.14  % (323518)Termination phase: Saturation
% 84.67/12.14  % (323518)Time elapsed: 0.472 s
% 84.67/12.14  % (323518)Peak memory usage: 17 MB
% 84.67/12.14  % (323518)Instructions burned: 881 (million)
% 84.67/12.14  % (323537)ott+10_1_sil=32000:tgt=ground:random_seed=1708087458:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 84.67/12.14  % (323513)Instruction limit reached! 
% 84.67/12.14  % (323513)------------------------------
% 84.67/12.14  % (323513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.67/12.14  % (323513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.67/12.14  % (323513)CaDiCaL version: 2.1.3
% 84.67/12.14  % (323513)Termination reason: Instruction limit
% 84.67/12.14  % (323513)Termination phase: Saturation
% 84.67/12.14  % (323513)Time elapsed: 0.664 s
% 84.67/12.14  % (323513)Peak memory usage: 21 MB
% 84.67/12.14  % (323513)Instructions burned: 1179 (million)
% 84.67/12.14  % (323539)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3125926839:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 84.67/12.14  % Exception at run slice level
% 84.67/12.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 84.67/12.14  % (323541)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1892619106:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 84.67/12.14  % (323535)Instruction limit reached! 
% 84.67/12.14  % (323535)------------------------------
% 84.67/12.14  % (323535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.67/12.14  % (323535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.67/12.14  % (323535)CaDiCaL version: 2.1.3
% 84.67/12.14  % (323535)Termination reason: Instruction limit
% 84.67/12.14  % (323535)Termination phase: Saturation
% 84.67/12.14  % (323535)Time elapsed: 0.476 s
% 84.67/12.14  % (323535)Peak memory usage: 17 MB
% 84.67/12.14  % (323535)Instructions burned: 870 (million)
% 84.67/12.14  % (323543)dis+21_1_sil=32000:sas=cadical:random_seed=2383063517:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 84.67/12.14  % (323528)Instruction limit reached! 
% 84.67/12.14  % (323528)------------------------------
% 84.67/12.14  % (323528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.67/12.14  % (323528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.67/12.14  % (323528)CaDiCaL version: 2.1.3
% 134.31/19.19  % (323528)Termination reason: Instruction limit
% 134.31/19.19  % (323528)Termination phase: Saturation
% 134.31/19.19  % (323528)Time elapsed: 0.781 s
% 134.31/19.19  % (323528)Peak memory usage: 30 MB
% 134.31/19.19  % (323528)Instructions burned: 1473 (million)
% 134.31/19.19  % (323545)ott+11_1_sil=16000:gs=on:random_seed=3875859995:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 134.31/19.19  % (323545)Instruction limit reached! 
% 134.31/19.19  % (323545)------------------------------
% 134.31/19.19  % (323545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.31/19.19  % (323545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.31/19.19  % (323545)CaDiCaL version: 2.1.3
% 134.31/19.19  % (323545)Termination reason: Instruction limit
% 134.31/19.19  % (323545)Termination phase: Saturation
% 134.31/19.19  % (323545)Time elapsed: 1.216 s
% 134.31/19.19  % (323545)Peak memory usage: 30 MB
% 134.31/19.19  % (323545)Instructions burned: 2251 (million)
% 134.31/19.19  % (323547)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2980565868:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi)
% 134.31/19.19  % Exception at run slice level
% 134.31/19.19  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.31/19.19  % (323549)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3529610337:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi)
% 134.31/19.19  % (323541)Instruction limit reached! 
% 134.31/19.19  % (323541)------------------------------
% 134.31/19.19  % (323541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.31/19.19  % (323541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.31/19.19  % (323541)CaDiCaL version: 2.1.3
% 134.31/19.19  % (323541)Termination reason: Instruction limit
% 134.31/19.19  % (323541)Termination phase: Saturation
% 134.31/19.19  % (323541)Time elapsed: 1.699 s
% 134.31/19.19  % (323541)Peak memory usage: 26 MB
% 134.31/19.19  % (323541)Instructions burned: 3513 (million)
% 134.31/19.19  % (323551)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3647752898:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 134.31/19.19  % (323527)Instruction limit reached! 
% 134.31/19.19  % (323527)------------------------------
% 134.31/19.19  % (323527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.31/19.19  % (323527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.31/19.19  % (323527)CaDiCaL version: 2.1.3
% 134.31/19.19  % (323527)Termination reason: Instruction limit
% 134.31/19.19  % (323527)Termination phase: Saturation
% 134.31/19.19  % (323527)Time elapsed: 2.541 s
% 134.31/19.19  % (323527)Peak memory usage: 29 MB
% 134.31/19.19  % (323527)Instructions burned: 5133 (million)
% 134.31/19.19  % (323543)Instruction limit reached! 
% 134.31/19.19  % (323543)------------------------------
% 134.31/19.19  % (323543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.31/19.19  % (323543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.31/19.19  % (323543)CaDiCaL version: 2.1.3
% 134.31/19.19  % (323543)Termination reason: Instruction limit
% 134.31/19.19  % (323543)Termination phase: Saturation
% 134.31/19.19  % (323543)Time elapsed: 1.903 s
% 134.31/19.19  % (323543)Peak memory usage: 25 MB
% 134.31/19.19  % (323543)Instructions burned: 3774 (million)
% 134.31/19.19  % (323553)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2521539071:i=5211_2969 on theBenchmark for (2969ds/5211Mi)
% 134.31/19.19  % (323554)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=62281573:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 134.31/19.19  % Exception at run slice level
% 134.31/19.19  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.31/19.19  % (323557)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2594398721:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 134.31/19.19  % Exception at run slice level
% 134.31/19.19  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.31/19.19  % (323559)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4013469113:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 134.31/19.19  % Exception at run slice level
% 134.31/19.19  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.31/19.19  % (323561)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=798664963:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi)
% 99.51/19.22  % (323537)Instruction limit reached! 
% 99.51/19.22  % (323537)------------------------------
% 99.51/19.22  % (323537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323537)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323537)Termination reason: Instruction limit
% 99.51/19.22  % (323537)Termination phase: Saturation
% 99.51/19.22  % (323537)Time elapsed: 2.650 s
% 99.51/19.22  % (323537)Peak memory usage: 42 MB
% 99.51/19.22  % (323537)Instructions burned: 5114 (million)
% 99.51/19.22  % (323563)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4254545418:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi)
% 99.51/19.22  % (323549)Instruction limit reached! 
% 99.51/19.22  % (323549)------------------------------
% 99.51/19.22  % (323549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323549)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323549)Termination reason: Instruction limit
% 99.51/19.22  % (323549)Termination phase: Saturation
% 99.51/19.22  % (323549)Time elapsed: 2.467 s
% 99.51/19.22  % (323549)Peak memory usage: 61 MB
% 99.51/19.22  % (323549)Instructions burned: 4592 (million)
% 99.51/19.22  % (323565)dis+10_16:1_sil=16000:random_seed=4186204640:i=9155:fsr=off_2949 on theBenchmark for (2949ds/9155Mi)
% 99.51/19.22  % (323553)Instruction limit reached! 
% 99.51/19.22  % (323553)------------------------------
% 99.51/19.22  % (323553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323553)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323553)Termination reason: Instruction limit
% 99.51/19.22  % (323553)Termination phase: Saturation
% 99.51/19.22  % (323553)Time elapsed: 2.503 s
% 99.51/19.22  % (323553)Peak memory usage: 35 MB
% 99.51/19.22  % (323553)Instructions burned: 5211 (million)
% 99.51/19.22  % (323567)ott-3_8_sil=64000:random_seed=2146133144:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi)
% 99.51/19.22  % (323563)Instruction limit reached! 
% 99.51/19.22  % (323563)------------------------------
% 99.51/19.22  % (323563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323563)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323563)Termination reason: Instruction limit
% 99.51/19.22  % (323563)Termination phase: Saturation
% 99.51/19.22  % (323563)Time elapsed: 4.477 s
% 99.51/19.22  % (323563)Peak memory usage: 73 MB
% 99.51/19.22  % (323563)Instructions burned: 8173 (million)
% 99.51/19.22  % (323569)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3601004156:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi)
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % (323571)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1174849282:i=11404_2921 on theBenchmark for (2921ds/11404Mi)
% 99.51/19.22  % (323565)Instruction limit reached! 
% 99.51/19.22  % (323565)------------------------------
% 99.51/19.22  % (323565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323565)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323565)Termination reason: Instruction limit
% 99.51/19.22  % (323565)Termination phase: Saturation
% 99.51/19.22  % (323565)Time elapsed: 4.271 s
% 99.51/19.22  % (323565)Peak memory usage: 36 MB
% 99.51/19.22  % (323565)Instructions burned: 9156 (million)
% 99.51/19.22  % (323573)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4017022820:i=14134_2906 on theBenchmark for (2906ds/14134Mi)
% 99.51/19.22  % (323561)Instruction limit reached! 
% 99.51/19.22  % (323561)------------------------------
% 99.51/19.22  % (323561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323561)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323561)Termination reason: Instruction limit
% 99.51/19.22  % (323561)Termination phase: Saturation
% 99.51/19.22  % (323561)Time elapsed: 8.791 s
% 99.51/19.22  % (323561)Peak memory usage: 26 MB
% 99.51/19.22  % (323561)Instructions burned: 22566 (million)
% 99.51/19.22  % (323575)dis+33_16_sil=32000:sac=on:random_seed=3771527691:i=15851:nm=0_2880 on theBenchmark for (2880ds/15851Mi)
% 99.51/19.22  % (323571)Instruction limit reached! 
% 99.51/19.22  % (323571)------------------------------
% 99.51/19.22  % (323571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323571)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323571)Termination reason: Instruction limit
% 99.51/19.22  % (323571)Termination phase: Saturation
% 99.51/19.22  % (323571)Time elapsed: 5.462 s
% 99.51/19.22  % (323571)Peak memory usage: 66 MB
% 99.51/19.22  % (323571)Instructions burned: 11405 (million)
% 99.51/19.22  % (323577)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2693269613:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi)
% 99.51/19.22  % (323567)Instruction limit reached! 
% 99.51/19.22  % (323567)------------------------------
% 99.51/19.22  % (323567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323567)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323567)Termination reason: Instruction limit
% 99.51/19.22  % (323567)Termination phase: Saturation
% 99.51/19.22  % (323567)Time elapsed: 10.170 s
% 99.51/19.22  % (323567)Peak memory usage: 104 MB
% 99.51/19.22  % (323567)Instructions burned: 20141 (million)
% 99.51/19.22  % (323579)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=343380173:s2a=on:i=53295_2842 on theBenchmark for (2842ds/53295Mi)
% 99.51/19.22  % (323573)Instruction limit reached! 
% 99.51/19.22  % (323573)------------------------------
% 99.51/19.22  % (323573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323573)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323573)Termination reason: Instruction limit
% 99.51/19.22  % (323573)Termination phase: Saturation
% 99.51/19.22  % (323573)Time elapsed: 7.109 s
% 99.51/19.22  % (323573)Peak memory usage: 82 MB
% 99.51/19.22  % (323573)Instructions burned: 14136 (million)
% 99.51/19.22  % (323581)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=469450129:i=26857:ins=20_2835 on theBenchmark for (2835ds/26857Mi)
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % (323583)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2628051600:i=28120:bs=on:fsr=off_2835 on theBenchmark for (2835ds/28120Mi)
% 99.51/19.22  % (323551)Instruction limit reached! 
% 99.51/19.22  % (323551)------------------------------
% 99.51/19.22  % (323551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.22  % (323551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.22  % (323551)CaDiCaL version: 2.1.3
% 99.51/19.22  % (323551)Termination reason: Instruction limit
% 99.51/19.22  % (323551)Termination phase: Saturation
% 99.51/19.22  % (323551)Time elapsed: 16.274 s
% 99.51/19.22  % (323551)Peak memory usage: 174 MB
% 99.51/19.22  % (323551)Instructions burned: 29342 (million)
% 99.51/19.22  % (323585)fmb+10_1_sil=256000:fmbss=7:random_seed=327764022:fmbsr=1.6:i=182295_2811 on theBenchmark for (2811ds/182295Mi)
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % (323587)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3965428411:i=44625:gsp=on_2810 on theBenchmark for (2810ds/44625Mi)
% 99.51/19.22  % (323587)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % (323589)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=94661884:i=160505_2810 on theBenchmark for (2810ds/160505Mi)
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % (323489) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-323482-323489"...
% 99.51/19.22  % (323489)...printing done.
% 99.51/19.22  % (323591)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1860707570:fmbsr=1.3:i=225729_2810 on theBenchmark for (2810ds/225729Mi)
% 99.51/19.22  % Exception at run slice level
% 99.51/19.22  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 99.51/19.22  % SZS status CounterSatisfiable for theBenchmark
% 99.51/19.22  % SZS output start Saturation.
% See solution above
% 99.51/19.23  % SZS output start Definitions and Model Updates.
% 99.51/19.23  for all inputs,
% 99.51/19.23      define nS_Sha512322870Issues(X0,X1,X2,X3) := $true
% 99.51/19.23  % SZS output end Definitions and Model Updates.
% 99.51/19.23  % (323489)------------------------------
% 99.51/19.23  % (323489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.51/19.23  % (323489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.51/19.23  % (323489)CaDiCaL version: 2.1.3
% 99.51/19.23  % (323489)Termination reason: Satisfiable
% 99.51/19.23  % (323489)Time elapsed: 18.952 s
% 99.51/19.23  % (323489)Peak memory usage: 37 MB
% 99.51/19.23  % (323489)Instructions burned: 48041 (million)
% 99.51/19.23  % (323482)Success in time 19.019 s
% 99.51/19.23  % Vampire exiting
%------------------------------------------------------------------------------