%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV296-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:18 AM UTC 2026
% Result : Unsatisfiable 0.23s 0.67s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 24
% Syntax : Number of formulae : 152 ( 42 unt; 0 def)
% Number of atoms : 422 ( 278 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 487 ( 217 ~; 270 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 18 con; 0-3 aty)
% Number of variables : 135 ( 63 sgn 39 !; 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_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0,axiom,
! [VAR_0,VAR_1] :
( c_in(VAR_0,c_Event_Oused(VAR_1),tc_Message_Omsg)
| ~ c_in(VAR_0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_0) ).
cnf(c_2,plain,
( c_in(A,c_Event_Oused(B),tc_Message_Omsg)
| ~ c_in(A,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,B)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Event_Oc_A_58_Aparts_A_Iknows_ASpy_Aevs1_J_A_61_61_62_Ac_A_58_Aused_Aevs1_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_3,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_4,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_5,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_Message_Oparts_OBody__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_in(VAR_1,c_Message_Oparts(VAR_2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(VAR_0,VAR_1),c_Message_Oparts(VAR_2),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Message_Oparts_OBody__dest_0) ).
cnf(c_6,plain,
( c_in(B,c_Message_Oparts(C),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(A,B),c_Message_Oparts(C),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Message_Oparts_OBody__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_7,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_8,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__NA__dest_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( VAR_4 = VAR_3
| 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_2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_1),c_Message_Omsg_OAgent(VAR_4)))),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(c_Message_Omsg_OAgent(VAR_1),c_Message_Omsg_OAgent(VAR_3)))),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__NA__dest_0) ).
cnf(c_9,plain,
( E = D
| c_in(B,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(B),c_Message_Omsg_OMPair(C,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(E)))),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(c_Message_Omsg_OAgent(B),c_Message_Omsg_OAgent(D)))),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__NA__dest_0]) ).
fof(cls_Public_OMPair__used_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_in(VAR_1,c_Event_Oused(VAR_2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(VAR_0,VAR_1),c_Event_Oused(VAR_2),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Public_OMPair__used_0) ).
cnf(c_10,plain,
( c_in(B,c_Event_Oused(C),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(A,B),c_Event_Oused(C),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Public_OMPair__used_0]) ).
fof(cls_conjecture_0,axiom,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_11,plain,
~ c_in(v_A,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_12,plain,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
fof(cls_conjecture_15,axiom,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| v_A = v_Ba
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_conjecture_15) ).
cnf(c_13,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| v_A = v_Ba
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_conjecture_15]) ).
cnf(c_693,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| v_Ba = v_A
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_13]) ).
cnf(c_14,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| v_Ba = v_A
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_693]) ).
fof(cls_conjecture_17,axiom,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_conjecture_17) ).
cnf(c_15,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_conjecture_17]) ).
cnf(c_694,plain,
( v_NA = c_Message_Omsg_ONonce(v_NAa)
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_15]) ).
cnf(c_16,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_694]) ).
fof(cls_conjecture_2,axiom,
~ c_in(c_Message_Omsg_OKey(v_KAB),c_Event_Oused(v_evs3),tc_Message_Omsg),
file('theBenchmark.p',cls_conjecture_2) ).
cnf(c_17,plain,
~ c_in(c_Message_Omsg_OKey(v_KAB),c_Event_Oused(v_evs3),tc_Message_Omsg),
inference(clausify,[status(thm)],[cls_conjecture_2]) ).
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_NB),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_18,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_NB),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_37,axiom,
( ~ c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('theBenchmark.p',cls_conjecture_37) ).
cnf(c_19,plain,
( ~ c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(clausify,[status(thm)],[cls_conjecture_37]) ).
fof(cls_conjecture_4,axiom,
c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('theBenchmark.p',cls_conjecture_4) ).
cnf(c_20,plain,
c_in(c_Event_Oevent_OSays(v_A,v_B,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_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(clausify,[status(thm)],[cls_conjecture_4]) ).
fof(cls_conjecture_5,axiom,
( v_K = v_KAB
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_conjecture_5) ).
cnf(c_21,plain,
( v_K = v_KAB
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_conjecture_5]) ).
cnf(c_22,plain,
( v_KAB = v_K
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_21]) ).
fof(cls_conjecture_6,axiom,
! [VAR_0] :
( v_K = v_KAB
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(VAR_0,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
file('theBenchmark.p',cls_conjecture_6) ).
cnf(c_23,plain,
( v_K = v_KAB
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(A,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(clausify,[status(thm)],[cls_conjecture_6]) ).
cnf(c_24,plain,
( v_KAB = v_K
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(A,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(copy,[status(thm)],[c_23]) ).
fof(cls_conjecture_68,axiom,
! [VAR_0,VAR_1] :
( v_B != v_Ba
| VAR_1 != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| VAR_0 != c_Message_Omsg_ONonce(v_NB) ),
file('theBenchmark.p',cls_conjecture_68) ).
cnf(c_25,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| A != c_Message_Omsg_ONonce(v_NB) ),
inference(clausify,[status(thm)],[cls_conjecture_68]) ).
cnf(c_695,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_25]) ).
cnf(c_696,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_695]) ).
cnf(c_697,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_696]) ).
cnf(c_698,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_A = v_Ba
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_697]) ).
cnf(c_699,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_698]) ).
cnf(c_700,plain,
( v_B != v_Ba
| c_Message_Omsg_ONonce(v_NB) != B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_699]) ).
cnf(c_701,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) != B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_700]) ).
cnf(c_702,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) != B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K ),
inference(copy,[status(thm)],[c_701]) ).
cnf(c_26,plain,
( v_Ba != v_B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K ),
inference(copy,[status(thm)],[c_702]) ).
fof(cls_conjecture_69,axiom,
! [VAR_0,VAR_1] :
( v_B != v_Ba
| VAR_1 != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| VAR_0 != c_Message_Omsg_ONonce(v_NB) ),
file('theBenchmark.p',cls_conjecture_69) ).
cnf(c_27,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| A != c_Message_Omsg_ONonce(v_NB) ),
inference(clausify,[status(thm)],[cls_conjecture_69]) ).
cnf(c_703,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_K != v_KAB
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_704,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_A != v_Aa
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_703]) ).
cnf(c_705,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| v_NA != c_Message_Omsg_ONonce(v_NAa)
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_704]) ).
cnf(c_706,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_707,plain,
( v_B != v_Ba
| B != c_Message_Omsg_ONonce(v_NB)
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_706]) ).
cnf(c_708,plain,
( v_B != v_Ba
| c_Message_Omsg_ONonce(v_NB) != B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_707]) ).
cnf(c_709,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) != B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K
| c_Message_Omsg_ONonce(v_NB) != A ),
inference(copy,[status(thm)],[c_708]) ).
cnf(c_710,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) != B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K ),
inference(copy,[status(thm)],[c_709]) ).
cnf(c_28,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_KAB != v_K ),
inference(copy,[status(thm)],[c_710]) ).
fof(cls_conjecture_7,axiom,
( v_A = v_Aa
| v_A = v_Ba
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_conjecture_7) ).
cnf(c_29,plain,
( v_A = v_Aa
| v_A = v_Ba
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_conjecture_7]) ).
cnf(c_711,plain,
( v_A = v_Aa
| v_Ba = v_A
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_29]) ).
cnf(c_30,plain,
( v_Aa = v_A
| v_Ba = v_A
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_711]) ).
fof(cls_conjecture_9,axiom,
( v_A = v_Aa
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_conjecture_9) ).
cnf(c_31,plain,
( v_A = v_Aa
| v_NA = c_Message_Omsg_ONonce(v_NB)
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_conjecture_9]) ).
cnf(c_712,plain,
( v_A = v_Aa
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_31]) ).
cnf(c_32,plain,
( v_Aa = v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(copy,[status(thm)],[c_712]) ).
cnf(c_33,plain,
( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolve,[status(thm)],[c_20,c_19]) ).
cnf(c_34,plain,
( D = C
| c_in(A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(A),c_Message_Omsg_OMPair(B,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),c_Message_Omsg_OAgent(D)))),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_Message_Omsg_OAgent(A),c_Message_Omsg_OAgent(C)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_12,c_9]) ).
cnf(c_35,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_12,c_8]) ).
cnf(c_41,plain,
~ c_in(c_Message_Omsg_OMPair(A,c_Message_Omsg_OKey(v_KAB)),c_Event_Oused(v_evs3),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_10,c_17]) ).
cnf(c_713,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_NB),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_NB),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_18,c_7]) ).
cnf(c_43,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_NB),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_NB),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_12,c_713]) ).
cnf(c_44,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_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_20,c_1]) ).
cnf(c_53,plain,
( v_KAB = v_K
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_B,c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OKey(v_K))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(v_x,c_Message_Omsg_OKey(v_K)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolve,[status(thm)],[c_33,c_22]) ).
cnf(c_57,plain,
~ c_in(c_Message_Omsg_OMPair(A,c_Message_Omsg_OKey(v_KAB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_2,c_41]) ).
cnf(c_67,plain,
~ c_in(c_Message_Omsg_OCrypt(A,c_Message_Omsg_OMPair(B,c_Message_Omsg_OKey(v_KAB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_6,c_57]) ).
cnf(c_107,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_44,c_3]) ).
cnf(c_109,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_NB),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_43,c_1]) ).
cnf(c_120,plain,
c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_107,c_3]) ).
cnf(c_137,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_120,c_3]) ).
cnf(c_714,plain,
( v_KAB = v_K
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_53,c_24]) ).
cnf(c_183,plain,
v_KAB = v_K,
inference(copy,[status(thm)],[c_714]) ).
cnf(c_235,plain,
~ c_in(c_Message_Omsg_OCrypt(A,c_Message_Omsg_OMPair(B,c_Message_Omsg_OKey(v_K))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_183,c_67]) ).
cnf(c_715,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_K != v_K ),
inference(paramod,[status(thm)],[c_183,c_28]) ).
cnf(c_247,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A ),
inference(copy,[status(thm)],[c_715]) ).
cnf(c_716,plain,
( v_Ba != v_B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A
| v_K != v_K ),
inference(paramod,[status(thm)],[c_183,c_26]) ).
cnf(c_248,plain,
( v_Ba != v_B
| v_Ba = v_A
| c_Message_Omsg_ONonce(v_NAa) != v_NA
| v_Aa != v_A ),
inference(copy,[status(thm)],[c_716]) ).
cnf(c_250,plain,
( v_Aa = v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(resolve,[status(thm)],[c_235,c_32]) ).
cnf(c_251,plain,
( v_Aa = v_A
| v_Ba = v_A ),
inference(resolve,[status(thm)],[c_235,c_30]) ).
cnf(c_252,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(resolve,[status(thm)],[c_235,c_16]) ).
cnf(c_253,plain,
( c_Message_Omsg_ONonce(v_NAa) = v_NA
| v_Ba = v_A ),
inference(resolve,[status(thm)],[c_235,c_14]) ).
cnf(c_717,plain,
( v_Ba = v_A
| v_Ba != v_B
| v_Ba = v_A
| v_Aa != v_A ),
inference(resolve,[status(thm)],[c_248,c_253]) ).
cnf(c_288,plain,
( v_Ba != v_B
| v_Ba = v_A
| v_Aa != v_A ),
inference(copy,[status(thm)],[c_717]) ).
cnf(c_718,plain,
( v_Ba = v_A
| v_Ba != v_B
| v_Ba = v_A ),
inference(resolve,[status(thm)],[c_288,c_251]) ).
cnf(c_289,plain,
( v_Ba != v_B
| v_Ba = v_A ),
inference(copy,[status(thm)],[c_718]) ).
cnf(c_292,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_NB),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_109,c_3]) ).
cnf(c_719,plain,
( c_Message_Omsg_ONonce(v_NB) = v_NA
| v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| v_Aa != v_A ),
inference(resolve,[status(thm)],[c_247,c_252]) ).
cnf(c_306,plain,
( v_Ba != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| v_Aa != v_A ),
inference(copy,[status(thm)],[c_719]) ).
cnf(c_308,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_137,c_5]) ).
cnf(c_720,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),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_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolve,[status(thm)],[c_308,c_35]) ).
cnf(c_309,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),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_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_11,c_720]) ).
cnf(c_721,plain,
( v_B = A
| c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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_308,c_34]) ).
cnf(c_310,plain,
( v_B = A
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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_11,c_721]) ).
cnf(c_321,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_NB),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_292,c_3]) ).
cnf(c_337,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_NB),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_321,c_3]) ).
cnf(c_352,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_337,c_4]) ).
cnf(c_353,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_NB),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_337,c_3]) ).
cnf(c_371,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_352,c_5]) ).
cnf(c_382,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_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_Ba = v_A ),
inference(paramod,[status(thm)],[c_253,c_371]) ).
cnf(c_383,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_OAgent(v_Aa),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_NB) = v_NA ),
inference(paramod,[status(thm)],[c_252,c_371]) ).
cnf(c_722,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,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_Ba = v_A
| v_Ba = v_A ),
inference(paramod,[status(thm)],[c_251,c_382]) ).
cnf(c_460,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,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_Ba = v_A ),
inference(copy,[status(thm)],[c_722]) ).
cnf(c_723,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,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_Ba = v_A
| v_Ba = v_A ),
inference(paramod,[status(thm)],[c_251,c_460]) ).
cnf(c_464,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,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_Ba = v_A ),
inference(copy,[status(thm)],[c_723]) ).
cnf(c_724,plain,
( v_B = v_Ba
| v_Ba = v_A ),
inference(resolve,[status(thm)],[c_464,c_310]) ).
cnf(c_474,plain,
( v_Ba = v_B
| v_Ba = v_A ),
inference(copy,[status(thm)],[c_724]) ).
cnf(c_725,plain,
( v_Ba = v_A
| v_Ba = v_A ),
inference(resolve,[status(thm)],[c_474,c_289]) ).
cnf(c_477,plain,
v_Ba = v_A,
inference(copy,[status(thm)],[c_725]) ).
cnf(c_483,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_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(paramod,[status(thm)],[c_477,c_383]) ).
cnf(c_726,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),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(paramod,[status(thm)],[c_477,c_353]) ).
cnf(c_492,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_477,c_726]) ).
cnf(c_727,plain,
( v_A != v_B
| c_Message_Omsg_ONonce(v_NB) = v_NA
| v_Aa != v_A ),
inference(paramod,[status(thm)],[c_477,c_306]) ).
cnf(c_505,plain,
( v_B != v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA
| v_Aa != v_A ),
inference(copy,[status(thm)],[c_727]) ).
cnf(c_528,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),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_A))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_5,c_309]) ).
cnf(c_570,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_492,c_5]) ).
cnf(c_728,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_Aa = v_A ),
inference(paramod,[status(thm)],[c_250,c_492]) ).
cnf(c_571,plain,
v_Aa = v_A,
inference(resolve,[status(thm)],[c_528,c_728]) ).
cnf(c_573,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_571,c_570]) ).
cnf(c_729,plain,
( v_B != v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA
| v_A != v_A ),
inference(paramod,[status(thm)],[c_571,c_505]) ).
cnf(c_592,plain,
( v_B != v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(copy,[status(thm)],[c_729]) ).
cnf(c_730,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(paramod,[status(thm)],[c_571,c_483]) ).
cnf(c_611,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(paramod,[status(thm)],[c_571,c_730]) ).
cnf(c_731,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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_573,c_35]) ).
cnf(c_643,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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_11,c_731]) ).
cnf(c_669,plain,
( v_B = v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(resolve,[status(thm)],[c_611,c_310]) ).
cnf(c_732,plain,
( c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_A))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| v_B = v_A ),
inference(paramod,[status(thm)],[c_669,c_573]) ).
cnf(c_670,plain,
v_B = v_A,
inference(resolve,[status(thm)],[c_309,c_732]) ).
cnf(c_733,plain,
( v_A != v_A
| c_Message_Omsg_ONonce(v_NB) = v_NA ),
inference(paramod,[status(thm)],[c_670,c_592]) ).
cnf(c_671,plain,
c_Message_Omsg_ONonce(v_NB) = v_NA,
inference(copy,[status(thm)],[c_733]) ).
cnf(c_677,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(paramod,[status(thm)],[c_670,c_308]) ).
cnf(c_691,plain,
~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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_671,c_643]) ).
cnf(c_692,plain,
$false,
inference(resolve,[status(thm)],[c_691,c_677]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV296-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n009.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:14 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 271869 was started by sandbox on n009,
% 0.19/0.45 % Sat Sep 26 13:29:14 2026
% 0.19/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.46
% 0.19/0.46 % From the command line: assign(max_seconds, 300).
% 0.23/0.67
% 0.23/0.67 % SZS status Unsatisfiable for theBenchmark
% 0.23/0.67
% 0.23/0.67 % Proof 1 at 0.15 (+ 0.03) seconds.
% 0.23/0.67 % Length of proof is 87.
% 0.23/0.67 % Level of proof is 20.
% 0.23/0.67 % Maximum clause weight is 80.000.
% 0.23/0.67 % Given clauses 321.
% 0.23/0.67
% 0.23/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------