%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV354-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 : Thu Sep 24 02:47:27 PM UTC 2026
% Result : Unsatisfiable 129.67s 17.18s
% Output : CNFRefutation 129.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 21
% Syntax : Number of formulae : 77 ( 14 unt; 10 def)
% Number of atoms : 218 ( 44 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 262 ( 121 ~; 131 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 11 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 16 con; 0-3 aty)
% Number of variables : 198 ( 198 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2951,axiom,
! [V_evs,V_A,V_B,V_x,V_na,V_nb,V_X] :
( ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(c_Public_OshrK(V_x)),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2955,axiom,
! [V_evs,V_A,V_B,V_k,V_na,V_nb,V_X] :
( c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(V_na,V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(V_k,c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2956,axiom,
! [V_evs,V_S_H,V_X_H,V_B_H,V_A_H,V_NA_H,V_nb,V_C,V_S,V_X,V_B,V_A,V_NA] :
( V_NA_H = V_NA
| c_in(V_nb,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(V_C,V_S,c_Message_Omsg_OMPair(V_X,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(V_S_H,c_Message_Omsg_OMPair(V_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA_H),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2958,axiom,
! [V_evs,V_S_H,V_X_H,V_B_H,V_A_H,V_NA_H,V_nb,V_C,V_S,V_X,V_B,V_A,V_NA] :
( V_B_H = V_B
| c_in(V_nb,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(V_C,V_S,c_Message_Omsg_OMPair(V_X,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(V_S_H,c_Message_Omsg_OMPair(V_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA_H),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2961,axiom,
! [V_evs,V_A,V_B,V_KAB,V_na,V_NB_H,V_X,V_NB] :
( V_KAB = c_Public_OshrK(v_sko__2VY(V_KAB))
| V_NB = V_NB_H
| c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(V_KAB),c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_KAB),c_Message_Omsg_OMPair(V_na,c_Message_Omsg_ONonce(V_NB_H))))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2969,negated_conjecture,
c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2970,negated_conjecture,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2972,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2973,negated_conjecture,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2974,negated_conjecture,
c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evso),tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2975,negated_conjecture,
! [V_U] :
( v_NB != v_NBa
| v_NA != v_NAa
| V_U != c_Message_Omsg_OKey(v_K) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6591,plain,
! [V_evs] :
( ! [V_A,V_B,V_x,V_na,V_nb,V_X] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(c_Public_OshrK(V_x)),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(miniscoping,[status(thm)],[f2951]) ).
fof(f6592,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ c_in(X6,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(c_Public_OshrK(X2)),c_Message_Omsg_OMPair(X3,X4)))),X5)),c_List_Oset(X6,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f6591]) ).
fof(f6598,plain,
! [V_evs,V_A,V_B,V_na,V_nb] :
( c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(V_na,V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ! [V_k,V_X] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(V_k,c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(miniscoping,[status(thm)],[f2955]) ).
fof(f6599,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ c_in(X4,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(X2,X3)))),X6)),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent)
| c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(X2,X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f6598]) ).
fof(f6600,plain,
! [V_NA_H,V_NA] :
( V_NA_H = V_NA
| ! [V_evs,V_nb] :
( c_in(V_nb,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ! [V_C,V_S,V_X,V_B,V_A] : ~ c_in(c_Event_Oevent_OSays(V_C,V_S,c_Message_Omsg_OMPair(V_X,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ! [V_S_H,V_X_H,V_B_H,V_A_H] : ~ c_in(c_Event_Oevent_OGets(V_S_H,c_Message_Omsg_OMPair(V_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA_H),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ) ),
inference(miniscoping,[status(thm)],[f2956]) ).
fof(f6601,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ c_in(X6,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(X8,X9,c_Message_Omsg_OMPair(X10,c_Message_Omsg_OCrypt(c_Public_OshrK(X11),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X12),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X7),X5))))),c_List_Oset(X6,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X5,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X6)),tc_Message_Omsg)
| X4 = X7
| ~ c_in(c_Event_Oevent_OGets(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OCrypt(c_Public_OshrK(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),X5))))),c_List_Oset(X6,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f6600]) ).
fof(f6604,plain,
! [V_B_H,V_B] :
( V_B_H = V_B
| ! [V_evs,V_nb] :
( c_in(V_nb,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ! [V_C,V_S,V_X,V_A,V_NA] : ~ c_in(c_Event_Oevent_OSays(V_C,V_S,c_Message_Omsg_OMPair(V_X,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ! [V_S_H,V_X_H,V_A_H,V_NA_H] : ~ c_in(c_Event_Oevent_OGets(V_S_H,c_Message_Omsg_OMPair(V_X_H,c_Message_Omsg_OCrypt(c_Public_OshrK(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(V_NA_H),V_nb))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ) ),
inference(miniscoping,[status(thm)],[f2958]) ).
fof(f6605,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( c_in(X5,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X6)),tc_Message_Omsg)
| X2 = X10
| ~ c_in(X6,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(X7,X8,c_Message_Omsg_OMPair(X9,c_Message_Omsg_OCrypt(c_Public_OshrK(X10),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X11),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X12),X5))))),c_List_Oset(X6,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Event_Oevent_OGets(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OCrypt(c_Public_OshrK(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),X5))))),c_List_Oset(X6,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f6604]) ).
fof(f6610,plain,
! [V_KAB] :
( V_KAB = c_Public_OshrK(v_sko__2VY(V_KAB))
| ! [V_NB_H,V_NB] :
( V_NB = V_NB_H
| ! [V_evs] :
( c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_ONonce(V_NB),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(V_KAB),c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)),tc_Message_Omsg)
| ! [V_A,V_B,V_na,V_X] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_KAB),c_Message_Omsg_OMPair(V_na,c_Message_Omsg_ONonce(V_NB_H))))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ) ) ),
inference(miniscoping,[status(thm)],[f2961]) ).
fof(f6611,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_in(X3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X6,c_Message_Omsg_ONonce(X0))))),X7)),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_ONonce(X1),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(X2),c_Event_Oknows(c_Message_Oagent_OSpy,X3),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| c_Public_OshrK(v_sko__2VY(X2)) = X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f6610]) ).
fof(f6624,plain,
c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f2969]) ).
fof(f6625,plain,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f2970]) ).
fof(f6627,plain,
c_in(c_Event_Oevent_OSays(v_B,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f2972]) ).
fof(f6628,plain,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2973]) ).
fof(f6629,plain,
c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evso),tc_Message_Omsg)),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2974]) ).
fof(f6630,plain,
( v_NB != v_NBa
| v_NA != v_NAa
| ! [V_U] : V_U != c_Message_Omsg_OKey(v_K) ),
inference(miniscoping,[status(thm)],[f2975]) ).
fof(f6631,plain,
! [X0] :
( v_NB != v_NBa
| v_NA != v_NAa
| X0 != c_Message_Omsg_OKey(v_K) ),
inference(cnf_transformation,[status(thm)],[f6630]) ).
fof(f6640,definition,
! [X0] :
( sQ2_spl
<=> X0 != c_Message_Omsg_OKey(v_K) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f6641,plain,
! [X0] :
( ~ sQ2_spl
| X0 != c_Message_Omsg_OKey(v_K) ),
inference(component_clause,[status(thm)],[f6640]) ).
fof(f6643,definition,
( sQ3_spl
<=> v_NA = v_NAa ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f6645,plain,
( sQ3_spl
| v_NAa != v_NA ),
inference(component_clause,[status(thm)],[f6643]) ).
fof(f6646,definition,
( sQ4_spl
<=> v_NB = v_NBa ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f6647,plain,
( ~ sQ4_spl
| v_NB = v_NBa ),
inference(component_clause,[status(thm)],[f6646]) ).
fof(f6649,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f6631,f6640,f6643,f6646]) ).
fof(f6710,definition,
( sQ6_spl
<=> c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f6712,plain,
( sQ6_spl
| ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f6710]) ).
fof(f6714,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6712,f6624]) ).
fof(f6715,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f6714]) ).
fof(f7055,definition,
( sQ11_spl
<=> c_Public_OshrK(v_sko__2VY(v_K)) = v_K ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f7056,plain,
( ~ sQ11_spl
| v_K = c_Public_OshrK(v_sko__2VY(v_K)) ),
inference(component_clause,[status(thm)],[f7055]) ).
fof(f8857,plain,
( ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
inference(resolution,[status(thm)],[f6599,f6625]) ).
fof(f8859,definition,
( sQ28_spl
<=> c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f8860,plain,
( ~ sQ28_spl
| c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f8859]) ).
fof(f8862,plain,
( ~ sQ6_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f8857,f8859,f6710]) ).
fof(f12102,plain,
! [X0] :
( ~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evso),tc_Message_Omsg)),tc_Message_Omsg)
| ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg)
| v_K = c_Public_OshrK(v_sko__2VY(v_K))
| v_NBa = X0 ),
inference(resolution,[status(thm)],[f6611,f6625]) ).
fof(f12105,definition,
! [X0] :
( sQ90_spl
<=> ( ~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evso),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg)
| v_NBa = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f12106,plain,
! [X0] :
( ~ sQ90_spl
| ~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evso),tc_Message_Omsg)),tc_Message_Omsg)
| v_NBa = X0
| c_in(c_Message_Omsg_ONonce(X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f12105]) ).
fof(f12108,plain,
( ~ sQ6_spl
| sQ11_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f12102,f12105,f7055,f6710]) ).
fof(f12138,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ11_spl
| ~ c_in(X5,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(X5,tc_Event_Oevent),tc_Event_Oevent) ),
inference(paramodulation,[status(thm)],[f7056,f6592]) ).
fof(f13843,plain,
! [X0,X1,X2,X3,X4] :
( X4 = v_NA
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OGets(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OCrypt(c_Public_OshrK(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f6601,f6627]) ).
fof(f13848,definition,
! [X0,X1,X2,X3,X4] :
( sQ144_spl
<=> ( X4 = v_NA
| ~ c_in(c_Event_Oevent_OGets(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OCrypt(c_Public_OshrK(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f13849,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ144_spl
| ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X0),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| v_NA = X0 ),
inference(component_clause,[status(thm)],[f13848]) ).
fof(f13851,definition,
( sQ145_spl
<=> c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f13852,plain,
( ~ sQ145_spl
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f13851]) ).
fof(f13854,plain,
( sQ145_spl
| sQ144_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f13843,f6710,f13848,f13851]) ).
fof(f13861,plain,
( ~ sQ145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13852,f6628]) ).
fof(f13862,plain,
~ sQ145_spl,
inference(contradiction_clause,[status(thm)],[f13861]) ).
fof(f20586,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg)
| X0 = v_B
| ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f6605,f6627]) ).
fof(f20592,definition,
! [X0,X1,X2,X3,X4] :
( sQ215_spl
<=> ( ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| X0 = v_B ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f20593,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ215_spl
| ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| X0 = v_B ),
inference(component_clause,[status(thm)],[f20592]) ).
fof(f20595,plain,
( sQ145_spl
| sQ215_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f20586,f6710,f20592,f13851]) ).
fof(f37747,plain,
( ~ sQ11_spl
| ~ c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f12138,f6625]) ).
fof(f37756,plain,
( ~ sQ11_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f37747,f6710,f7055]) ).
fof(f37849,plain,
( ~ sQ90_spl
| v_NBa = v_NB
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evso)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f12106,f6629]) ).
fof(f37851,plain,
( ~ sQ90_spl
| sQ4_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f37849,f13851,f6646,f12105]) ).
fof(f38022,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ215_spl
| ~ sQ4_spl
| ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X4),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| X0 = v_B ),
inference(backward_demodulation,[status(thm)],[f6647,f20593]) ).
fof(f38024,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ144_spl
| ~ sQ4_spl
| ~ c_in(c_Event_Oevent_OGets(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OCrypt(c_Public_OshrK(X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X0),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)
| v_NA = X0 ),
inference(backward_demodulation,[status(thm)],[f6647,f13849]) ).
fof(f38715,plain,
( ~ sQ28_spl
| ~ sQ215_spl
| ~ sQ4_spl
| v_B = v_Ba ),
inference(resolution,[status(thm)],[f38022,f8860]) ).
fof(f38772,plain,
( ~ sQ28_spl
| ~ sQ215_spl
| ~ sQ4_spl
| c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
inference(backward_demodulation,[status(thm)],[f38715,f8860]) ).
fof(f38783,plain,
( ~ sQ28_spl
| ~ sQ215_spl
| ~ sQ4_spl
| c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
inference(forward_demodulation,[status(thm)],[f38715,f38772]) ).
fof(f40083,plain,
( ~ sQ144_spl
| ~ sQ4_spl
| ~ sQ28_spl
| ~ sQ215_spl
| v_NAa = v_NA ),
inference(resolution,[status(thm)],[f38783,f38024]) ).
fof(f40085,plain,
( ~ sQ144_spl
| ~ sQ4_spl
| ~ sQ28_spl
| ~ sQ215_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f40083,f6645]) ).
fof(f40086,plain,
( ~ sQ144_spl
| ~ sQ4_spl
| ~ sQ28_spl
| ~ sQ215_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f40085]) ).
fof(f40087,plain,
( ~ sQ2_spl
| $false ),
inference(destructive_equality_resolution,[status(thm)],[f6641]) ).
fof(f40088,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f40087]) ).
fof(f40089,plain,
$false,
inference(sat_refutation,[status(thm)],[f6649,f6715,f8862,f12108,f13854,f13862,f20595,f37756,f37851,f40086,f40088]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV354-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 08:40:36 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.36/0.66 % Drodi V4.1.1
% 129.67/17.18 % Refutation found
% 129.67/17.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 129.67/17.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 38.98/18.21 % Elapsed time: 17.790911 seconds
% 38.98/18.21 % CPU time: 132.733203 seconds
% 38.98/18.21 % Total memory used: 881.966 MB
% 38.98/18.21 % Net memory used: 830.411 MB
%------------------------------------------------------------------------------