%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV303-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:07:20 AM UTC 2026
% Result : Unsatisfiable 0.23s 0.64s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 18
% Syntax : Number of formulae : 149 ( 33 unt; 0 def)
% Number of atoms : 327 ( 163 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 263 ( 85 ~; 178 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 17 con; 0-3 aty)
% Number of variables : 117 ( 40 sgn 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_Event_OSays__imp__analz__Spy__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( c_in(VAR_2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(VAR_0,VAR_1,VAR_2),c_List_Oset(VAR_3,tc_Event_Oevent),tc_Event_Oevent) ),
file('theBenchmark.p',cls_Event_OSays__imp__analz__Spy__dest_0) ).
cnf(c_1,plain,
( c_in(C,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,D)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(A,B,C),c_List_Oset(D,tc_Event_Oevent),tc_Event_Oevent) ),
inference(clausify,[status(thm)],[cls_Event_OSays__imp__analz__Spy__dest_0]) ).
fof(cls_Message_OMPair__analz_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_in(VAR_1,c_Message_Oanalz(VAR_2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(VAR_0,VAR_1),c_Message_Oanalz(VAR_2),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Message_OMPair__analz_0) ).
cnf(c_2,plain,
( c_in(B,c_Message_Oanalz(C),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(A,B),c_Message_Oanalz(C),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Message_OMPair__analz_0]) ).
fof(cls_Message_OMPair__analz_1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_in(VAR_0,c_Message_Oanalz(VAR_2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(VAR_0,VAR_1),c_Message_Oanalz(VAR_2),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Message_OMPair__analz_1) ).
cnf(c_3,plain,
( c_in(A,c_Message_Oanalz(C),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(A,B),c_Message_Oanalz(C),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Message_OMPair__analz_1]) ).
fof(cls_Message_Oanalz__into__parts__dest_0,axiom,
! [VAR_0,VAR_1] :
( c_in(VAR_0,c_Message_Oparts(VAR_1),tc_Message_Omsg)
| ~ c_in(VAR_0,c_Message_Oanalz(VAR_1),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Message_Oanalz__into__parts__dest_0) ).
cnf(c_4,plain,
( c_in(A,c_Message_Oparts(B),tc_Message_Omsg)
| ~ c_in(A,c_Message_Oanalz(B),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Message_Oanalz__into__parts__dest_0]) ).
fof(cls_OtwayRees_OGets__imp__Says__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_in(c_Event_Oevent_OSays(v_sko__usf(VAR_1,VAR_2,VAR_0),VAR_1,VAR_2),c_List_Oset(VAR_0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(VAR_1,VAR_2),c_List_Oset(VAR_0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(VAR_0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('theBenchmark.p',cls_OtwayRees_OGets__imp__Says__dest_0) ).
cnf(c_5,plain,
( c_in(c_Event_Oevent_OSays(v_sko__usf(B,C,A),B,C),c_List_Oset(A,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(B,C),c_List_Oset(A,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(clausify,[status(thm)],[cls_OtwayRees_OGets__imp__Says__dest_0]) ).
fof(cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( c_in(VAR_1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_1),c_Message_Omsg_OAgent(VAR_5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_2,c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_4),c_Message_Omsg_OAgent(VAR_1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(VAR_0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('theBenchmark.p',cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0) ).
cnf(c_6,plain,
( c_in(B,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(F)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(clausify,[status(thm)],[cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0]) ).
fof(cls_OtwayRees_Ounique__NB__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( VAR_2 = VAR_5
| c_in(VAR_1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_5,c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_6),c_Message_Omsg_OAgent(VAR_1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_2,c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_4),c_Message_Omsg_OAgent(VAR_1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(VAR_0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('theBenchmark.p',cls_OtwayRees_Ounique__NB__dest_0) ).
cnf(c_7,plain,
( C = F
| c_in(B,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V6),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(clausify,[status(thm)],[cls_OtwayRees_Ounique__NB__dest_0]) ).
fof(cls_OtwayRees_Ounique__NB__dest_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( VAR_4 = VAR_6
| c_in(VAR_1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_5,c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_6),c_Message_Omsg_OAgent(VAR_1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(VAR_1),c_Message_Omsg_OMPair(VAR_2,c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_4),c_Message_Omsg_OAgent(VAR_1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_0)),tc_Message_Omsg)
| ~ c_in(VAR_0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('theBenchmark.p',cls_OtwayRees_Ounique__NB__dest_1) ).
cnf(c_8,plain,
( E = V6
| c_in(B,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V6),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(E),c_Message_Omsg_OAgent(B))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)
| ~ c_in(A,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(clausify,[status(thm)],[cls_OtwayRees_Ounique__NB__dest_1]) ).
fof(cls_conjecture_0,axiom,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_9,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_conjecture_1,axiom,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(c_10,plain,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
fof(cls_conjecture_13,axiom,
( v_NB = c_Message_Omsg_ONonce(v_NAa)
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('theBenchmark.p',cls_conjecture_13) ).
cnf(c_11,plain,
( v_NB = c_Message_Omsg_ONonce(v_NAa)
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(clausify,[status(thm)],[cls_conjecture_13]) ).
cnf(c_12,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NB
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(copy,[status(thm)],[c_11]) ).
fof(cls_conjecture_19,axiom,
( c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_B = v_Ba ),
file('theBenchmark.p',cls_conjecture_19) ).
cnf(c_13,plain,
( c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_B = v_Ba ),
inference(clausify,[status(thm)],[cls_conjecture_19]) ).
fof(cls_conjecture_20,axiom,
( c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_NB = c_Message_Omsg_ONonce(v_NBa) ),
file('theBenchmark.p',cls_conjecture_20) ).
cnf(c_14,plain,
( c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| v_NB = c_Message_Omsg_ONonce(v_NBa) ),
inference(clausify,[status(thm)],[cls_conjecture_20]) ).
cnf(c_15,plain,
( c_in(c_Event_Oevent_OSays(v_Aa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(copy,[status(thm)],[c_14]) ).
fof(cls_conjecture_3,axiom,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('theBenchmark.p',cls_conjecture_3) ).
cnf(c_16,plain,
c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(clausify,[status(thm)],[cls_conjecture_3]) ).
fof(cls_conjecture_30,axiom,
( v_B = v_Aa
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa ),
file('theBenchmark.p',cls_conjecture_30) ).
cnf(c_17,plain,
( v_B = v_Aa
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa ),
inference(clausify,[status(thm)],[cls_conjecture_30]) ).
cnf(c_18,plain,
( v_B = v_Aa
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_A != v_Aa ),
inference(copy,[status(thm)],[c_17]) ).
fof(cls_conjecture_31,axiom,
( v_NB = c_Message_Omsg_ONonce(v_NAa)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa ),
file('theBenchmark.p',cls_conjecture_31) ).
cnf(c_19,plain,
( v_NB = c_Message_Omsg_ONonce(v_NAa)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa ),
inference(clausify,[status(thm)],[cls_conjecture_31]) ).
cnf(c_562,plain,
( v_NB = c_Message_Omsg_ONonce(v_NAa)
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_A != v_Aa ),
inference(copy,[status(thm)],[c_19]) ).
cnf(c_20,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NB
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_A != v_Aa ),
inference(copy,[status(thm)],[c_562]) ).
fof(cls_conjecture_5,axiom,
( v_B = v_Aa
| v_B = v_Ba ),
file('theBenchmark.p',cls_conjecture_5) ).
cnf(c_21,plain,
( v_B = v_Aa
| v_B = v_Ba ),
inference(clausify,[status(thm)],[cls_conjecture_5]) ).
fof(cls_conjecture_8,axiom,
( v_B = v_Aa
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('theBenchmark.p',cls_conjecture_8) ).
cnf(c_22,plain,
( v_B = v_Aa
| c_in(c_Event_Oevent_OSays(v_Ba,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(clausify,[status(thm)],[cls_conjecture_8]) ).
cnf(c_23,plain,
( D = F
| c_in(A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(E,c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(F),c_Message_Omsg_OAgent(A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(B,c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(D),c_Message_Omsg_OAgent(A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_10,c_8]) ).
cnf(c_24,plain,
( B = E
| c_in(A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(E,c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(F),c_Message_Omsg_OAgent(A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(B,c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(D),c_Message_Omsg_OAgent(A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_10,c_7]) ).
cnf(c_25,plain,
( c_in(A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),c_Message_Omsg_OAgent(E)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(B,c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(D),c_Message_Omsg_OAgent(A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_10,c_6]) ).
cnf(c_27,plain,
( c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_12,c_1]) ).
cnf(c_28,plain,
( c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_13,c_1]) ).
cnf(c_29,plain,
( c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_15,c_1]) ).
cnf(c_563,plain,
( c_in(c_Event_Oevent_OSays(v_sko__usf(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))))))),v_evs3),c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolve,[status(thm)],[c_16,c_5]) ).
cnf(c_30,plain,
c_in(c_Event_Oevent_OSays(v_sko__usf(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))))))),v_evs3),c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(resolve,[status(thm)],[c_10,c_563]) ).
cnf(c_31,plain,
( ~ c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| v_B = v_Aa ),
inference(paramod,[status(thm)],[c_21,c_9]) ).
cnf(c_32,plain,
( c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_22,c_1]) ).
cnf(c_35,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_28,c_2]) ).
cnf(c_39,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_35,c_2]) ).
cnf(c_43,plain,
( c_in(c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_39,c_2]) ).
cnf(c_47,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_43,c_2]) ).
cnf(c_50,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_27,c_2]) ).
cnf(c_55,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_29,c_2]) ).
cnf(c_57,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_47,c_4]) ).
cnf(c_58,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_57,c_25]) ).
cnf(c_61,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_30,c_1]) ).
cnf(c_64,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_32,c_2]) ).
cnf(c_68,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_64,c_2]) ).
cnf(c_72,plain,
( c_in(c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_68,c_2]) ).
cnf(c_76,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_72,c_2]) ).
cnf(c_80,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_50,c_2]) ).
cnf(c_82,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_76,c_4]) ).
cnf(c_564,plain,
( A = v_NA
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_82,c_24]) ).
cnf(c_84,plain,
( v_NA = A
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_564]) ).
cnf(c_565,plain,
( B = v_A
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_82,c_23]) ).
cnf(c_85,plain,
( v_A = B
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_565]) ).
cnf(c_88,plain,
( c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_55,c_2]) ).
cnf(c_92,plain,
( c_in(c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_80,c_2]) ).
cnf(c_96,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_61,c_2]) ).
cnf(c_100,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_92,c_2]) ).
cnf(c_102,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_100,c_4]) ).
cnf(c_566,plain,
( A = v_NA
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_102,c_24]) ).
cnf(c_104,plain,
( v_NA = A
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(copy,[status(thm)],[c_566]) ).
cnf(c_567,plain,
( B = v_A
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_102,c_23]) ).
cnf(c_105,plain,
( v_A = B
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(copy,[status(thm)],[c_567]) ).
cnf(c_108,plain,
( c_in(c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_88,c_2]) ).
cnf(c_112,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_108,c_2]) ).
cnf(c_114,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_112,c_4]) ).
cnf(c_115,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_114,c_25]) ).
cnf(c_120,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_96,c_2]) ).
cnf(c_124,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_120,c_2]) ).
cnf(c_127,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_124,c_3]) ).
cnf(c_128,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_124,c_2]) ).
cnf(c_129,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_127,c_4]) ).
cnf(c_130,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_ONonce(v_NBa) = v_NB ),
inference(resolve,[status(thm)],[c_129,c_115]) ).
cnf(c_131,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| v_B = v_Ba ),
inference(resolve,[status(thm)],[c_129,c_58]) ).
cnf(c_132,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_129,c_25]) ).
cnf(c_133,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_128,c_4]) ).
cnf(c_134,plain,
( v_A = v_Aa
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_133,c_105]) ).
cnf(c_568,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_133,c_104]) ).
cnf(c_135,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(copy,[status(thm)],[c_568]) ).
cnf(c_136,plain,
( v_A = v_Aa
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_133,c_85]) ).
cnf(c_569,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_133,c_84]) ).
cnf(c_137,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_569]) ).
cnf(c_138,plain,
( c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_133,c_25]) ).
cnf(c_570,plain,
( v_B = v_Aa
| v_A = v_Aa
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_136,c_31]) ).
cnf(c_141,plain,
( v_A = v_Aa
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_570]) ).
cnf(c_142,plain,
( ~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| v_A = v_Aa ),
inference(paramod,[status(thm)],[c_141,c_9]) ).
cnf(c_143,plain,
( v_B = v_Ba
| v_A = v_Aa ),
inference(resolve,[status(thm)],[c_142,c_131]) ).
cnf(c_145,plain,
( ~ c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| v_A = v_Aa ),
inference(paramod,[status(thm)],[c_143,c_9]) ).
cnf(c_571,plain,
( v_A = v_Aa
| v_Ba = v_Aa
| v_A = v_Aa ),
inference(paramod,[status(thm)],[c_143,c_141]) ).
cnf(c_146,plain,
( v_Ba = v_Aa
| v_A = v_Aa ),
inference(copy,[status(thm)],[c_571]) ).
cnf(c_572,plain,
( v_A = v_Aa
| v_A = v_Aa
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_134,c_145]) ).
cnf(c_235,plain,
( v_A = v_Aa
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(copy,[status(thm)],[c_572]) ).
cnf(c_262,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Aa ),
inference(paramod,[status(thm)],[c_235,c_129]) ).
cnf(c_573,plain,
( v_B = v_Aa
| c_Message_Omsg_ONonce(v_NAa) = v_NA
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_137,c_31]) ).
cnf(c_271,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_573]) ).
cnf(c_574,plain,
( v_B = v_Aa
| v_A != v_Aa
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_271,c_18]) ).
cnf(c_273,plain,
( v_A != v_Aa
| v_B = v_Aa ),
inference(copy,[status(thm)],[c_574]) ).
cnf(c_318,plain,
( v_Ba = v_Aa
| v_B = v_Aa ),
inference(resolve,[status(thm)],[c_273,c_146]) ).
cnf(c_319,plain,
( ~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| v_Ba = v_Aa ),
inference(paramod,[status(thm)],[c_318,c_9]) ).
cnf(c_320,plain,
( v_B = v_Ba
| v_Ba = v_Aa ),
inference(resolve,[status(thm)],[c_319,c_131]) ).
cnf(c_575,plain,
( v_Ba = v_Aa
| v_Ba = v_Aa
| v_Ba = v_Aa ),
inference(paramod,[status(thm)],[c_320,c_318]) ).
cnf(c_576,plain,
( v_Ba = v_Aa
| v_Ba = v_Aa ),
inference(copy,[status(thm)],[c_575]) ).
cnf(c_323,plain,
v_Ba = v_Aa,
inference(copy,[status(thm)],[c_576]) ).
cnf(c_362,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_A = v_Aa ),
inference(paramod,[status(thm)],[c_323,c_262]) ).
cnf(c_577,plain,
( c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(paramod,[status(thm)],[c_323,c_138]) ).
cnf(c_578,plain,
( c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(paramod,[status(thm)],[c_323,c_577]) ).
cnf(c_402,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(paramod,[status(thm)],[c_323,c_578]) ).
cnf(c_403,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(paramod,[status(thm)],[c_323,c_135]) ).
cnf(c_579,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Ba))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_323,c_133]) ).
cnf(c_404,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_323,c_579]) ).
cnf(c_406,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_323,c_129]) ).
cnf(c_580,plain,
( v_B = v_Aa
| v_B = v_Aa ),
inference(paramod,[status(thm)],[c_323,c_21]) ).
cnf(c_452,plain,
v_B = v_Aa,
inference(copy,[status(thm)],[c_580]) ).
cnf(c_455,plain,
~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent),
inference(paramod,[status(thm)],[c_452,c_9]) ).
cnf(c_458,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_Message_Omsg_ONonce(v_NAa) = v_NB ),
inference(resolve,[status(thm)],[c_455,c_403]) ).
cnf(c_459,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NBa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_455,c_402]) ).
cnf(c_464,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_455,c_132]) ).
cnf(c_465,plain,
c_Message_Omsg_ONonce(v_NBa) = v_NB,
inference(resolve,[status(thm)],[c_455,c_130]) ).
cnf(c_468,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_465,c_459]) ).
cnf(c_493,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_465,c_404]) ).
cnf(c_523,plain,
v_A = v_Aa,
inference(resolve,[status(thm)],[c_468,c_362]) ).
cnf(c_581,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NB
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_Aa ),
inference(paramod,[status(thm)],[c_523,c_20]) ).
cnf(c_535,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NB
| c_Message_Omsg_ONonce(v_NAa) != v_NA ),
inference(copy,[status(thm)],[c_581]) ).
cnf(c_582,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NAa) = v_NA ),
inference(paramod,[status(thm)],[c_458,c_406]) ).
cnf(c_545,plain,
c_Message_Omsg_ONonce(v_NAa) = v_NA,
inference(resolve,[status(thm)],[c_468,c_582]) ).
cnf(c_583,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NB
| v_NA != v_NA ),
inference(paramod,[status(thm)],[c_545,c_535]) ).
cnf(c_584,plain,
( v_NA = v_NB
| v_NA != v_NA ),
inference(paramod,[status(thm)],[c_545,c_583]) ).
cnf(c_585,plain,
( v_NB = v_NA
| v_NA != v_NA ),
inference(copy,[status(thm)],[c_584]) ).
cnf(c_546,plain,
v_NB = v_NA,
inference(copy,[status(thm)],[c_585]) ).
cnf(c_586,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_NB,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_545,c_493]) ).
cnf(c_547,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_546,c_586]) ).
cnf(c_560,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(A,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(v_Aa))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_545,c_464]) ).
cnf(c_561,plain,
$false,
inference(resolve,[status(thm)],[c_560,c_547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV303-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n014.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 13:29:46 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.45 % Process 3264097 was started by sandbox2 on n014,
% 0.19/0.45 % Sat Sep 26 13:29:46 2026
% 0.19/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/0.46
% 0.19/0.46 % From the command line: assign(max_seconds, 300).
% 0.23/0.64
% 0.23/0.64 % SZS status Unsatisfiable for theBenchmark
% 0.23/0.64
% 0.23/0.64 % Proof 1 at 0.14 (+ 0.03) seconds.
% 0.23/0.64 % Length of proof is 106.
% 0.23/0.64 % Level of proof is 25.
% 0.23/0.64 % Maximum clause weight is 80.000.
% 0.23/0.64 % Given clauses 158.
% 0.23/0.64
% 0.23/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------