%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV764-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:49:30 PM UTC 2026
% Result : Unsatisfiable 104.04s 18.66s
% Output : CNFRefutation 104.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 48
% Syntax : Number of formulae : 195 ( 81 unt; 20 def)
% Number of atoms : 354 ( 30 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 294 ( 135 ~; 139 |; 0 &)
% ( 20 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 21 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 22 con; 0-4 aty)
% Number of variables : 214 ( 214 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,axiom,
! [V_X,V_H] :
( ~ hBOOL(c_in(V_X,V_H,tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f288,axiom,
hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,axiom,
! [V_X,V_evs,V_A] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),V_X),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg))
| ~ hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f471,axiom,
! [V_A,V_B,V_K,V_evs] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg))
| hBOOL(c_in(V_B,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(V_A,V_B,V_K,V_evs),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A)))))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f487,axiom,
! [V_X] : hBOOL(c_in(hAPP(c_Public_OshrK,V_X),c_Message_OsymKeys,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f491,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f493,axiom,
! [V_X,V_H,V_Y] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f505,axiom,
! [V_X,V_H] :
( ~ hBOOL(c_in(V_X,V_H,tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f506,axiom,
! [V_X,V_H] :
( ~ hBOOL(c_in(V_X,V_H,tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f507,axiom,
! [V_X,V_evs,V_A,V_B] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f514,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f522,axiom,
! [V_X,V_evs,V_A,V_B] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f524,axiom,
! [V_A,V_A_H,V_evs,V_NA_H,V_B_H,V_K,V_X_H,V_NA,V_B,V_X] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A_H),c_Message_Omsg_OMPair(V_NA_H,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X_H))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_A = V_A_H ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f526,axiom,
! [V_B,V_B_H,V_evs,V_A_H,V_NA_H,V_K,V_X_H,V_A,V_NA,V_X] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A_H),c_Message_Omsg_OMPair(V_NA_H,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X_H))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_B = V_B_H ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f540,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(c_in(V_x,V_S,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f541,axiom,
! [V_S,V_x,T_a] :
( ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f552,axiom,
! [V_X,V_B,V_K,V_A,V_evs,V_K_H,V_N] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f562,negated_conjecture,
hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f564,negated_conjecture,
hBOOL(c_in(v_Ka,c_Message_OsymKeys,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f565,negated_conjecture,
hBOOL(c_in(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f566,negated_conjecture,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f567,negated_conjecture,
hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f568,negated_conjecture,
v_K = v_Ka,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f570,negated_conjecture,
! [V_x] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_x,v_B,v_X),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f579,axiom,
! [T_2,T_1] :
( ~ class_Orderings_Oorder(T_1)
| class_Orderings_Oorder(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f587,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f595,axiom,
class_Orderings_Oorder(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f672,plain,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f865,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X0,X1,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f1011,plain,
hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f1135,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),X1),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f1278,plain,
! [X0,X1,X2,X3] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X2,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X2,X0,X1,X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X2)))))))),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X2))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f1307,plain,
! [X0] : hBOOL(c_in(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,tc_nat)),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f1312,plain,
! [X0] : c_Message_Oanalz(X0) = c_Message_Oanalz(c_Message_Oanalz(X0)),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f1315,plain,
! [V_X,V_H] :
( ! [V_Y] : ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f493]) ).
fof(f1316,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X0,c_Message_Oanalz(X2),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1315]) ).
fof(f1335,plain,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f505]) ).
fof(f1336,plain,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f506]) ).
fof(f1337,plain,
! [V_X,V_evs] :
( ! [V_A,V_B] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f507]) ).
fof(f1338,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1337]) ).
fof(f1347,plain,
! [X0] : c_Message_Oparts(X0) = c_Message_Oanalz(c_Message_Oparts(X0)),
inference(cnf_transformation,[status(thm)],[f514]) ).
fof(f1358,plain,
! [V_X,V_evs] :
( ! [V_A,V_B] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f522]) ).
fof(f1359,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1358]) ).
fof(f1361,plain,
! [V_A,V_evs,V_K] :
( ! [V_NA,V_B,V_X] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ! [V_A_H] :
( ! [V_NA_H,V_B_H,V_X_H] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A_H),c_Message_Omsg_OMPair(V_NA_H,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X_H))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_A = V_A_H ) ),
inference(miniscoping,[status(thm)],[f524]) ).
fof(f1362,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( X1 = X6
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X6,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X6),c_Message_Omsg_OMPair(X7,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X4),X9))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X4),X5))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(cnf_transformation,[status(thm)],[f1361]) ).
fof(f1365,plain,
! [V_B,V_evs,V_K] :
( ! [V_A,V_NA,V_X] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ! [V_B_H] :
( ! [V_A_H,V_NA_H,V_X_H] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A_H),c_Message_Omsg_OMPair(V_NA_H,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X_H))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_B = V_B_H ) ),
inference(miniscoping,[status(thm)],[f526]) ).
fof(f1366,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X7,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X7),c_Message_Omsg_OMPair(X8,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X4),X9))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent))
| X6 = X3
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X4),X5))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(cnf_transformation,[status(thm)],[f1365]) ).
fof(f1383,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : hBOOL(c_in(V_x,V_S,T_a)) ),
inference(miniscoping,[status(thm)],[f540]) ).
fof(f1384,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X1,X0))
| hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f1383]) ).
fof(f1385,plain,
! [V_S,V_x] :
( ! [T_a] : ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f541]) ).
fof(f1386,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X1,X0))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f1385]) ).
fof(f1402,plain,
! [V_X,V_B,V_K,V_A,V_evs] :
( ! [V_K_H,V_N] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
inference(miniscoping,[status(thm)],[f552]) ).
fof(f1403,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X2,c_Message_Omsg_OCrypt(X5,c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X2))) = X3 ),
inference(cnf_transformation,[status(thm)],[f1402]) ).
fof(f1413,plain,
hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f562]) ).
fof(f1415,plain,
hBOOL(c_in(v_Ka,c_Message_OsymKeys,tc_nat)),
inference(cnf_transformation,[status(thm)],[f564]) ).
fof(f1416,plain,
hBOOL(c_in(c_Event_Oevent_OSays(v_A_H,v_Ba,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f1417,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f1418,plain,
hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f567]) ).
fof(f1419,plain,
v_Ka = v_K,
inference(cnf_transformation,[status(thm)],[f568]) ).
fof(f1421,plain,
! [X0] : ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,v_B,v_X),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f570]) ).
fof(f1436,plain,
! [T_1] :
( ~ class_Orderings_Oorder(T_1)
| ! [T_2] : class_Orderings_Oorder(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f579]) ).
fof(f1437,plain,
! [X0,X1] :
( class_Orderings_Oorder(tc_fun(X1,X0))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1436]) ).
fof(f1448,plain,
class_Orderings_Oorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f1456,plain,
class_Orderings_Oorder(tc_bool),
inference(cnf_transformation,[status(thm)],[f595]) ).
fof(f1492,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1416,f1359]) ).
fof(f1500,plain,
hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)),
inference(forward_demodulation,[status(thm)],[f1419,f1418]) ).
fof(f1506,definition,
( sQ8_spl
<=> hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1508,plain,
( sQ8_spl
| ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f1506]) ).
fof(f1510,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1508,f1413]) ).
fof(f1511,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1510]) ).
fof(f1522,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(forward_demodulation,[status(thm)],[f1419,f1417]) ).
fof(f1548,definition,
( sQ10_spl
<=> hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1549,plain,
( ~ sQ10_spl
| hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f1548]) ).
fof(f1737,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| X0 = v_A ),
inference(resolution,[status(thm)],[f1362,f1500]) ).
fof(f1738,definition,
! [X0,X1,X2,X3] :
( sQ24_spl
<=> ( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| X0 = v_A ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1739,plain,
! [X0,X1,X2,X3] :
( ~ sQ24_spl
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_A = X0 ),
inference(component_clause,[status(thm)],[f1738]) ).
fof(f1741,plain,
( ~ sQ8_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1737,f1738,f1506]) ).
fof(f1897,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1338,f1416]) ).
fof(f1916,plain,
! [X0] : class_Orderings_Oorder(tc_fun(X0,tc_bool)),
inference(resolution,[status(thm)],[f1437,f1456]) ).
fof(f1960,plain,
! [X0] : hBOOL(hAPP(c_Message_OsymKeys,hAPP(c_Public_OshrK,X0))),
inference(resolution,[status(thm)],[f1386,f1307]) ).
fof(f1974,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs4)),
inference(resolution,[status(thm)],[f1386,f1413]) ).
fof(f1975,plain,
hBOOL(hAPP(c_Message_OsymKeys,v_Ka)),
inference(resolution,[status(thm)],[f1386,f1415]) ).
fof(f1981,plain,
! [X0] : hBOOL(c_in(v_Ka,c_Message_OsymKeys,X0)),
inference(resolution,[status(thm)],[f1975,f1384]) ).
fof(f1983,plain,
! [X0] : hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,X0)),
inference(resolution,[status(thm)],[f1974,f1384]) ).
fof(f2016,plain,
hBOOL(c_in(v_Ka,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1981,f1336]) ).
fof(f2017,plain,
hBOOL(c_in(v_Ka,c_Message_Oparts(c_Message_OsymKeys),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1981,f1335]) ).
fof(f2020,plain,
hBOOL(c_in(v_evs4,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1983,f1336]) ).
fof(f2021,plain,
hBOOL(c_in(v_evs4,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1983,f1335]) ).
fof(f2182,definition,
( sQ60_spl
<=> hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2184,plain,
( sQ60_spl
| ~ hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f2182]) ).
fof(f2260,plain,
( ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_Ka,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f1897,f1278]) ).
fof(f2267,definition,
( sQ72_spl
<=> hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_Ka,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f2268,plain,
( ~ sQ72_spl
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_Aa,v_Ba,v_Ka,v_evs4),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)))))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f2267]) ).
fof(f2270,definition,
( sQ73_spl
<=> hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2273,plain,
( ~ sQ8_spl
| sQ73_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f2260,f2267,f2270,f1506]) ).
fof(f2357,plain,
hBOOL(hAPP(c_Message_Oparts(c_Message_OsymKeys),v_Ka)),
inference(resolution,[status(thm)],[f2017,f1386]) ).
fof(f2414,plain,
! [X0] : hBOOL(c_in(v_Ka,c_Message_Oparts(c_Message_OsymKeys),X0)),
inference(resolution,[status(thm)],[f2357,f1384]) ).
fof(f2446,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Message_OsymKeys),v_Ka)),
inference(resolution,[status(thm)],[f2016,f1386]) ).
fof(f2462,plain,
! [X0] : hBOOL(c_in(v_Ka,c_Message_Oanalz(c_Message_OsymKeys),X0)),
inference(resolution,[status(thm)],[f2446,f1384]) ).
fof(f2519,plain,
! [X0,X1] : hBOOL(c_in(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,X1)),
inference(resolution,[status(thm)],[f1960,f1384]) ).
fof(f2633,plain,
hBOOL(hAPP(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),v_evs4)),
inference(resolution,[status(thm)],[f2020,f1386]) ).
fof(f2650,plain,
! [X0] : hBOOL(c_in(v_evs4,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),X0)),
inference(resolution,[status(thm)],[f2633,f1384]) ).
fof(f2723,plain,
hBOOL(hAPP(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),v_evs4)),
inference(resolution,[status(thm)],[f2021,f1386]) ).
fof(f2729,plain,
! [X0] : hBOOL(c_in(v_evs4,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),X0)),
inference(resolution,[status(thm)],[f2723,f1384]) ).
fof(f2743,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_B = X0 ),
inference(resolution,[status(thm)],[f1366,f1500]) ).
fof(f2744,definition,
! [X0,X1,X2,X3] :
( sQ92_spl
<=> ( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| v_B = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2745,plain,
! [X0,X1,X2,X3] :
( ~ sQ92_spl
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),X3))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent))
| X0 = v_B ),
inference(component_clause,[status(thm)],[f2744]) ).
fof(f2747,plain,
( ~ sQ8_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f2743,f2744,f1506]) ).
fof(f3442,plain,
( v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A)))
| ~ hBOOL(c_in(v_evs4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(resolution,[status(thm)],[f1403,f1500]) ).
fof(f3443,definition,
( sQ128_spl
<=> v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3444,plain,
( ~ sQ128_spl
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))) = v_X ),
inference(component_clause,[status(thm)],[f3443]) ).
fof(f3446,plain,
( sQ128_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f3442,f1506,f3443]) ).
fof(f3840,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,c_List_Olist_ONil(tc_Event_Oevent))),
inference(resolution,[status(thm)],[f1011,f1386]) ).
fof(f3844,plain,
! [X0] : hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,X0)),
inference(resolution,[status(thm)],[f3840,f1384]) ).
fof(f4910,plain,
hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f865,f2729]) ).
fof(f4911,plain,
hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f865,f2650]) ).
fof(f4916,plain,
hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f865,f2462]) ).
fof(f4917,plain,
hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f865,f2414]) ).
fof(f5596,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),v_Ka)),
inference(resolution,[status(thm)],[f4916,f1386]) ).
fof(f5617,plain,
! [X0] : hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),X0)),
inference(resolution,[status(thm)],[f5596,f1384]) ).
fof(f6505,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),v_evs4)),
inference(resolution,[status(thm)],[f4911,f1386]) ).
fof(f6636,plain,
! [X0] : hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),X0)),
inference(resolution,[status(thm)],[f6505,f1384]) ).
fof(f7274,plain,
( hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolution,[status(thm)],[f1135,f1492]) ).
fof(f7281,plain,
( sQ10_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f7274,f2270,f1548]) ).
fof(f8679,definition,
( sQ434_spl
<=> c_Orderings_Otop__class_Otop(tc_bool) = c_Orderings_Otop__class_Otop(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f8681,plain,
( sQ434_spl
| c_Orderings_Otop__class_Otop(tc_bool) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(component_clause,[status(thm)],[f8679]) ).
fof(f9091,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),v_evs4)),
inference(resolution,[status(thm)],[f4910,f1386]) ).
fof(f9099,plain,
! [X0] : hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),X0)),
inference(resolution,[status(thm)],[f9091,f1384]) ).
fof(f9214,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),v_Ka)),
inference(resolution,[status(thm)],[f4917,f1386]) ).
fof(f9219,plain,
! [X0] : hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),X0)),
inference(resolution,[status(thm)],[f9214,f1384]) ).
fof(f9416,plain,
( ~ sQ10_spl
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1549,f1316]) ).
fof(f9433,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9416,f1522]) ).
fof(f9434,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f9433]) ).
fof(f9938,definition,
! [X0] :
( sQ485_spl
<=> ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ485_spl])],[split_symbol_definition]) ).
fof(f9939,plain,
! [X0] :
( ~ sQ485_spl
| ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f9938]) ).
fof(f10099,plain,
( ~ sQ485_spl
| $false ),
inference(resolution,[status(thm)],[f9939,f3844]) ).
fof(f10101,plain,
~ sQ485_spl,
inference(contradiction_clause,[status(thm)],[f10099]) ).
fof(f10530,definition,
( sQ529_spl
<=> hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ529_spl])],[split_symbol_definition]) ).
fof(f10531,plain,
( ~ sQ529_spl
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f10530]) ).
fof(f10572,definition,
( sQ532_spl
<=> hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ532_spl])],[split_symbol_definition]) ).
fof(f10574,plain,
( sQ532_spl
| ~ hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f10572]) ).
fof(f10612,plain,
( sQ532_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10574,f672]) ).
fof(f10613,plain,
sQ532_spl,
inference(contradiction_clause,[status(thm)],[f10612]) ).
fof(f10894,plain,
( sQ434_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8681]) ).
fof(f10895,plain,
sQ434_spl,
inference(contradiction_clause,[status(thm)],[f10894]) ).
fof(f10998,definition,
( sQ570_spl
<=> class_Orderings_Oorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f11000,plain,
( sQ570_spl
| ~ class_Orderings_Oorder(tc_nat) ),
inference(component_clause,[status(thm)],[f10998]) ).
fof(f11005,definition,
( sQ572_spl
<=> class_Orderings_Oorder(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition]) ).
fof(f11007,plain,
( sQ572_spl
| ~ class_Orderings_Oorder(tc_bool) ),
inference(component_clause,[status(thm)],[f11005]) ).
fof(f11012,definition,
( sQ574_spl
<=> class_Orderings_Oorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f11014,plain,
( sQ574_spl
| ~ class_Orderings_Oorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f11012]) ).
fof(f11157,plain,
( sQ570_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11000,f1448]) ).
fof(f11158,plain,
sQ570_spl,
inference(contradiction_clause,[status(thm)],[f11157]) ).
fof(f11159,plain,
( sQ574_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11014,f1916]) ).
fof(f11160,plain,
sQ574_spl,
inference(contradiction_clause,[status(thm)],[f11159]) ).
fof(f11161,plain,
( sQ572_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11007,f1456]) ).
fof(f11162,plain,
sQ572_spl,
inference(contradiction_clause,[status(thm)],[f11161]) ).
fof(f11230,plain,
( ~ sQ92_spl
| ~ sQ72_spl
| v_Ba = v_B ),
inference(resolution,[status(thm)],[f2268,f2745]) ).
fof(f11232,plain,
( ~ sQ24_spl
| ~ sQ72_spl
| v_Aa = v_A ),
inference(resolution,[status(thm)],[f2268,f1739]) ).
fof(f11300,plain,
( ~ sQ128_spl
| ~ sQ92_spl
| ~ sQ72_spl
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))) = v_X ),
inference(backward_demodulation,[status(thm)],[f11230,f3444]) ).
fof(f11308,plain,
! [X0] :
( ~ sQ92_spl
| ~ sQ72_spl
| ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,v_Ba,v_X),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(backward_demodulation,[status(thm)],[f11230,f1421]) ).
fof(f11701,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2184,f3844]) ).
fof(f11702,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f11701]) ).
fof(f12187,definition,
( sQ636_spl
<=> hBOOL(c_in(hAPP(c_Public_OshrK,v_Aa),c_Message_OsymKeys,tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition]) ).
fof(f12189,plain,
( sQ636_spl
| ~ hBOOL(c_in(hAPP(c_Public_OshrK,v_Aa),c_Message_OsymKeys,tc_nat)) ),
inference(component_clause,[status(thm)],[f12187]) ).
fof(f12200,plain,
( sQ636_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12189,f2519]) ).
fof(f12201,plain,
sQ636_spl,
inference(contradiction_clause,[status(thm)],[f12200]) ).
fof(f12342,definition,
( sQ645_spl
<=> hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition]) ).
fof(f12344,plain,
( sQ645_spl
| ~ hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f12342]) ).
fof(f12373,definition,
( sQ649_spl
<=> hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f12375,plain,
( sQ649_spl
| ~ hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f12373]) ).
fof(f12389,definition,
( sQ652_spl
<=> hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition]) ).
fof(f12391,plain,
( sQ652_spl
| ~ hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f12389]) ).
fof(f12396,definition,
( sQ654_spl
<=> hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f12398,plain,
( sQ654_spl
| ~ hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f12396]) ).
fof(f12418,plain,
( sQ652_spl
| ~ hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f1347,f12391]) ).
fof(f12419,plain,
( sQ652_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12418,f9219]) ).
fof(f12420,plain,
sQ652_spl,
inference(contradiction_clause,[status(thm)],[f12419]) ).
fof(f12424,plain,
( sQ654_spl
| ~ hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f1347,f12398]) ).
fof(f12425,plain,
( sQ654_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12424,f9099]) ).
fof(f12426,plain,
sQ654_spl,
inference(contradiction_clause,[status(thm)],[f12425]) ).
fof(f12427,plain,
( sQ645_spl
| ~ hBOOL(c_in(v_Ka,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f1312,f12344]) ).
fof(f12428,plain,
( sQ645_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12427,f5617]) ).
fof(f12429,plain,
sQ645_spl,
inference(contradiction_clause,[status(thm)],[f12428]) ).
fof(f12436,plain,
( sQ649_spl
| ~ hBOOL(c_in(v_evs4,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f1312,f12375]) ).
fof(f12437,plain,
( sQ649_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12436,f6636]) ).
fof(f12438,plain,
sQ649_spl,
inference(contradiction_clause,[status(thm)],[f12437]) ).
fof(f12465,plain,
( ~ sQ529_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10531,f1522]) ).
fof(f12466,plain,
~ sQ529_spl,
inference(contradiction_clause,[status(thm)],[f12465]) ).
fof(f12617,plain,
( ~ sQ128_spl
| ~ sQ92_spl
| ~ sQ72_spl
| ~ sQ24_spl
| hBOOL(c_in(c_Event_Oevent_OSays(v_A_H,v_Ba,v_X),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(backward_demodulation,[status(thm)],[f12618,f1416]) ).
fof(f12618,plain,
( ~ sQ128_spl
| ~ sQ92_spl
| ~ sQ72_spl
| ~ sQ24_spl
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa))) ),
inference(forward_demodulation,[status(thm)],[f11232,f11300]) ).
fof(f12653,plain,
( ~ sQ128_spl
| ~ sQ92_spl
| ~ sQ72_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12617,f11308]) ).
fof(f12654,plain,
( ~ sQ128_spl
| ~ sQ92_spl
| ~ sQ72_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f12653]) ).
fof(f12655,plain,
$false,
inference(sat_refutation,[status(thm)],[f1511,f1741,f2273,f2747,f3446,f7281,f9434,f10101,f10613,f10895,f11158,f11160,f11162,f11702,f12201,f12420,f12426,f12429,f12438,f12466,f12654]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV764-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.39 % Computer : n016.cluster.edu
% 0.14/5.39 % Model : x86_64 x86_64
% 0.14/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.39 % Memory : 8046.5625MB
% 0.14/5.39 % OS : Linux 6.8.0-71-generic
% 0.14/5.39 % CPULimit : 300
% 0.14/5.39 % WCLimit : 300
% 0.14/5.39 % DateTime : Mon Sep 21 09:28:43 UTC 2026
% 0.17/5.40 % CPUTime :
% 0.17/5.44 % Drodi V4.1.1
% 104.04/18.66 % Refutation found
% 104.04/18.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 104.04/18.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.82/18.86 % Elapsed time: 13.449469 seconds
% 12.82/18.86 % CPU time: 105.333966 seconds
% 12.82/18.86 % Total memory used: 877.634 MB
% 12.82/18.86 % Net memory used: 849.146 MB
%------------------------------------------------------------------------------