%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV801-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 : n001.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:34 PM UTC 2026
% Result : Unsatisfiable 37.93s 5.43s
% Output : CNFRefutation 37.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 100
% Syntax : Number of formulae : 435 ( 214 unt; 59 def)
% Number of atoms : 662 ( 58 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 404 ( 177 ~; 168 |; 0 &)
% ( 59 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 67 ( 65 usr; 60 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 22 con; 0-3 aty)
% Number of variables : 199 ( 199 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [V_K] : c_Message_OinvKey(c_Message_OinvKey(V_K)) = V_K,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [V_xs,T_a] : c_List_Odistinct(c_List_Oremdups(V_xs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [V_X,V_H] : c_lessequals(c_Set_Oinsert(V_X,c_Message_Osynth(V_H),tc_Message_Omsg),c_Message_Osynth(c_Set_Oinsert(V_X,V_H,tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,axiom,
! [V_A,V_H] : c_in(c_Message_Omsg_OAgent(V_A),c_Message_Osynth(V_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f232,axiom,
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(f236,axiom,
! [V_K] :
( ~ c_in(V_K,c_Message_OsymKeys,tc_nat)
| c_in(c_Message_OinvKey(V_K),c_Message_OsymKeys,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,axiom,
! [V_K] :
( ~ c_in(V_K,c_Message_OsymKeys,tc_nat)
| c_Message_OinvKey(V_K) = V_K ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f240,axiom,
! [V_x,V_xa,T_a,V_zs] : c_List_Oappend(c_List_Olist_OCons(V_x,V_xa,T_a),V_zs,T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(V_xa,V_zs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,axiom,
! [V_x,V_B,T_a,V_A] :
( ~ c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))
| c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f263,axiom,
! [V_H] : c_Message_Osynth(c_Message_Osynth(V_H)) = c_Message_Osynth(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,axiom,
! [V_a,V_A,T_a] :
( ~ c_in(V_a,V_A,T_a)
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [V_x,V_xs,T_a] :
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f388,axiom,
! [V_K,V_H,V_X] :
( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)
| c_in(c_Message_OinvKey(V_K),c_Message_OkeysFor(V_H),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f431,axiom,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f444,axiom,
! [V_K,V_evs] :
( c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Event_Oused(V_evs),tc_Message_Omsg)
| ~ c_in(V_K,c_Message_OsymKeys,tc_nat)
| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(V_K,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs))),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f453,axiom,
! [V_X] : c_in(hAPP(c_Public_OshrK,V_X),c_Message_OsymKeys,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f457,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f471,axiom,
! [V_X,V_H] :
( ~ c_in(V_X,V_H,tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f472,axiom,
! [V_X,V_H] :
( ~ c_in(V_X,V_H,tc_Message_Omsg)
| c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f475,axiom,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f481,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f505,axiom,
! [V_msg1,V_msg2,V_nat_H,V_msg_H] : c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f513,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| c_in(V_x,V_S,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f514,axiom,
! [V_S,V_x,T_a] :
( ~ c_in(V_x,V_S,T_a)
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f539,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f540,negated_conjecture,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f541,negated_conjecture,
c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f542,negated_conjecture,
~ c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f543,negated_conjecture,
c_in(v_KAB,c_Message_OsymKeys,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f544,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_ONonce(v_NAa)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f545,negated_conjecture,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f546,negated_conjecture,
v_A = v_Aa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f548,negated_conjecture,
v_B = v_Ba,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f549,negated_conjecture,
v_K = v_KAB,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f551,negated_conjecture,
c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f552,negated_conjecture,
~ c_in(c_Event_Oevent_OSays(v_Aa,v_Ba,c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f567,axiom,
class_HOL_Oord(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f575,axiom,
class_HOL_Oord(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f581,plain,
! [X0,X1,X2] : c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f590,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f593,plain,
! [X0] : c_Message_OinvKey(c_Message_OinvKey(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f604,plain,
! [X0,X1] : c_List_Odistinct(c_List_Oremdups(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f656,plain,
c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f676,plain,
! [X0,X1] : c_lessequals(c_Set_Oinsert(X0,c_Message_Osynth(X1),tc_Message_Omsg),c_Message_Osynth(c_Set_Oinsert(X0,X1,tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f876,plain,
! [X0,X1] : c_in(c_Message_Omsg_OAgent(X0),c_Message_Osynth(X1),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f907,plain,
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)],[f232]) ).
fof(f911,plain,
! [X0] :
( ~ c_in(X0,c_Message_OsymKeys,tc_nat)
| c_in(c_Message_OinvKey(X0),c_Message_OsymKeys,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f912,plain,
! [X0] :
( ~ c_in(X0,c_Message_OsymKeys,tc_nat)
| c_Message_OinvKey(X0) = X0 ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f917,plain,
! [X0,X1,X2,X3] : c_List_Oappend(c_List_Olist_OCons(X0,X1,X2),X3,X2) = c_List_Olist_OCons(X0,c_List_Oappend(X1,X3,X2),X2),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f926,plain,
! [V_x,V_B,T_a] :
( ! [V_A] : ~ c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))
| c_in(V_x,V_B,T_a) ),
inference(miniscoping,[status(thm)],[f247]) ).
fof(f927,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(c_Set_Oinsert(X0,X3,X2),X1,tc_fun(X2,tc_bool))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f926]) ).
fof(f951,plain,
! [X0] : c_Message_Osynth(c_Message_Osynth(X0)) = c_Message_Osynth(X0),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f1017,plain,
! [X0,X1,X2] :
( ~ c_in(X0,X1,X2)
| c_Set_Oinsert(X0,X1,X2) = X1 ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f1058,plain,
! [X0,X1,X2] :
( ~ c_List_Odistinct(c_List_Olist_OCons(X0,X1,X2),X2)
| ~ c_in(X0,c_List_Oset(X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f1126,plain,
! [V_K,V_H] :
( ! [V_X] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)
| c_in(c_Message_OinvKey(V_K),c_Message_OkeysFor(V_H),tc_nat) ),
inference(miniscoping,[status(thm)],[f388]) ).
fof(f1127,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OCrypt(X0,X2),X1,tc_Message_Omsg)
| c_in(c_Message_OinvKey(X0),c_Message_OkeysFor(X1),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1126]) ).
fof(f1196,plain,
! [X0,X1,X2] : X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f1217,plain,
! [X0,X1] :
( c_in(hAPP(c_Message_Omsg_OKey,X0),c_Event_Oused(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_OsymKeys,tc_nat)
| ~ c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(X0,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1))),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f444]) ).
fof(f1232,plain,
! [X0] : c_in(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,tc_nat),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f1237,plain,
! [X0] : c_Message_Oanalz(c_Message_Oanalz(X0)) = c_Message_Oanalz(X0),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f1260,plain,
! [X0,X1] :
( ~ c_in(X0,X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f471]) ).
fof(f1261,plain,
! [X0,X1] :
( ~ c_in(X0,X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f472]) ).
fof(f1266,plain,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f1273,plain,
! [X0] : c_Message_Oanalz(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f1311,plain,
! [X0,X1,X2,X3] : c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OCrypt(X2,X3),
inference(cnf_transformation,[status(thm)],[f505]) ).
fof(f1321,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : c_in(V_x,V_S,T_a) ),
inference(miniscoping,[status(thm)],[f513]) ).
fof(f1322,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X1,X0))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1321]) ).
fof(f1323,plain,
! [V_S,V_x] :
( ! [T_a] : ~ c_in(V_x,V_S,T_a)
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f514]) ).
fof(f1324,plain,
! [X0,X1,X2] :
( ~ c_in(X1,X0,X2)
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1323]) ).
fof(f1356,plain,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(thm)],[f539]) ).
fof(f1357,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(thm)],[f540]) ).
fof(f1358,plain,
c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f1359,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f542]) ).
fof(f1360,plain,
c_in(v_KAB,c_Message_OsymKeys,tc_nat),
inference(cnf_transformation,[status(thm)],[f543]) ).
fof(f1361,plain,
c_in(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_ONonce(v_NAa)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f544]) ).
fof(f1362,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f1363,plain,
v_A = v_Aa,
inference(cnf_transformation,[status(thm)],[f546]) ).
fof(f1365,plain,
v_B = v_Ba,
inference(cnf_transformation,[status(thm)],[f548]) ).
fof(f1366,plain,
v_K = v_KAB,
inference(cnf_transformation,[status(thm)],[f549]) ).
fof(f1368,plain,
c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f1369,plain,
~ c_in(c_Event_Oevent_OSays(v_Aa,v_Ba,c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f1392,plain,
class_HOL_Oord(tc_nat),
inference(cnf_transformation,[status(thm)],[f567]) ).
fof(f1400,plain,
class_HOL_Oord(tc_bool),
inference(cnf_transformation,[status(thm)],[f575]) ).
fof(f1404,definition,
( sQ0_spl
<=> c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1405,plain,
( ~ sQ0_spl
| c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f1404]) ).
fof(f1407,definition,
( sQ1_spl
<=> c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1409,plain,
( sQ1_spl
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f1407]) ).
fof(f1431,plain,
c_in(v_K,c_Message_OsymKeys,tc_nat),
inference(forward_demodulation,[status(thm)],[f1366,f1360]) ).
fof(f1432,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f1366,f1359]) ).
fof(f1440,plain,
c_in(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_ONonce(v_NAa)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[status(thm)],[f1363,f1361]) ).
fof(f1441,plain,
c_in(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[status(thm)],[f1365,f1440]) ).
fof(f1456,plain,
c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg),
inference(forward_demodulation,[status(thm)],[f1366,f1368]) ).
fof(f1465,plain,
~ c_in(c_Event_Oevent_OSays(v_A,v_Ba,c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[status(thm)],[f1363,f1369]) ).
fof(f1466,plain,
~ c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[status(thm)],[f1365,f1465]) ).
fof(f1467,plain,
~ c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_demodulation,[status(thm)],[f1366,f1466]) ).
fof(f2126,plain,
c_in(c_Message_OinvKey(v_K),c_Message_OsymKeys,tc_nat),
inference(resolution,[status(thm)],[f911,f1431]) ).
fof(f2243,plain,
c_Message_OinvKey(c_Message_OinvKey(v_K)) = c_Message_OinvKey(v_K),
inference(resolution,[status(thm)],[f912,f2126]) ).
fof(f2245,plain,
v_K = c_Message_OinvKey(v_K),
inference(forward_demodulation,[status(thm)],[f593,f2243]) ).
fof(f2256,definition,
( sQ70_spl
<=> c_in(v_K,c_Message_OsymKeys,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f2258,plain,
( sQ70_spl
| ~ c_in(v_K,c_Message_OsymKeys,tc_nat) ),
inference(component_clause,[status(thm)],[f2256]) ).
fof(f3738,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2258,f1431]) ).
fof(f3739,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f3738]) ).
fof(f3906,definition,
( sQ188_spl
<=> c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f3908,plain,
( sQ188_spl
| ~ c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f3906]) ).
fof(f3910,plain,
( sQ188_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3908,f1358]) ).
fof(f3911,plain,
sQ188_spl,
inference(contradiction_clause,[status(thm)],[f3910]) ).
fof(f4078,definition,
( sQ213_spl
<=> c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f4079,plain,
( ~ sQ213_spl
| c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f4078]) ).
fof(f4083,plain,
( ~ sQ213_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4079,f1432]) ).
fof(f4084,plain,
~ sQ213_spl,
inference(contradiction_clause,[status(thm)],[f4083]) ).
fof(f5876,plain,
c_Set_Oinsert(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent) = c_Event_Obad,
inference(resolution,[status(thm)],[f1017,f1266]) ).
fof(f5887,plain,
! [X0] : c_Set_Oinsert(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,tc_nat) = c_Message_OsymKeys,
inference(resolution,[status(thm)],[f1017,f1232]) ).
fof(f5896,plain,
c_Set_Oinsert(v_K,c_Message_OsymKeys,tc_nat) = c_Message_OsymKeys,
inference(resolution,[status(thm)],[f1017,f1431]) ).
fof(f5897,plain,
c_Set_Oinsert(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) = c_NS__Shared__Mirabelle_Ons__shared,
inference(resolution,[status(thm)],[f1017,f1358]) ).
fof(f5912,plain,
hBOOL(hAPP(c_Event_Obad,c_Message_Oagent_OSpy)),
inference(paramodulation,[status(thm)],[f5876,f590]) ).
fof(f6077,plain,
hBOOL(hAPP(c_Message_OsymKeys,v_K)),
inference(paramodulation,[status(thm)],[f5896,f590]) ).
fof(f6145,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs2)),
inference(paramodulation,[status(thm)],[f5897,f590]) ).
fof(f6176,plain,
! [X0] : c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,X0),
inference(resolution,[status(thm)],[f1322,f6145]) ).
fof(f6177,plain,
! [X0] : c_in(v_K,c_Message_OsymKeys,X0),
inference(resolution,[status(thm)],[f1322,f6077]) ).
fof(f6178,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Event_Obad,X0),
inference(resolution,[status(thm)],[f1322,f5912]) ).
fof(f6188,plain,
! [X0,X1,X2,X3] : c_in(X0,c_Set_Oinsert(X0,X1,X2),X3),
inference(resolution,[status(thm)],[f1322,f590]) ).
fof(f6191,plain,
c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6176,f1261]) ).
fof(f6192,plain,
c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6176,f1260]) ).
fof(f6193,plain,
! [X0] : c_Set_Oinsert(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,X0) = c_NS__Shared__Mirabelle_Ons__shared,
inference(resolution,[status(thm)],[f6176,f1017]) ).
fof(f6224,plain,
c_in(v_K,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6177,f1261]) ).
fof(f6225,plain,
c_in(v_K,c_Message_Oparts(c_Message_OsymKeys),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6177,f1260]) ).
fof(f6226,plain,
! [X0] : c_Set_Oinsert(v_K,c_Message_OsymKeys,X0) = c_Message_OsymKeys,
inference(resolution,[status(thm)],[f6177,f1017]) ).
fof(f6278,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6178,f1261]) ).
fof(f6279,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Oparts(c_Event_Obad),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6178,f1260]) ).
fof(f6280,plain,
! [X0] : c_Set_Oinsert(c_Message_Oagent_OSpy,c_Event_Obad,X0) = c_Event_Obad,
inference(resolution,[status(thm)],[f6178,f1017]) ).
fof(f6305,definition,
( sQ308_spl
<=> c_in(v_evs2,c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f6307,plain,
( sQ308_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6305]) ).
fof(f6316,plain,
! [X0,X1,X2] : c_in(X0,c_Message_Oanalz(c_Set_Oinsert(X0,X1,X2)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6188,f1261]) ).
fof(f6329,plain,
! [X0,X1] : c_in(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,X1),
inference(paramodulation,[status(thm)],[f5887,f6188]) ).
fof(f6360,definition,
( sQ310_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f6362,plain,
( sQ310_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6360]) ).
fof(f6388,definition,
( sQ312_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Event_Obad),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f6390,plain,
( sQ312_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Event_Obad),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6388]) ).
fof(f6500,plain,
! [X0,X1] : c_Set_Oinsert(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,X1) = c_Message_OsymKeys,
inference(resolution,[status(thm)],[f6329,f1017]) ).
fof(f6539,definition,
( sQ316_spl
<=> c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f6540,plain,
( ~ sQ316_spl
| c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
inference(component_clause,[status(thm)],[f6539]) ).
fof(f6568,definition,
( sQ318_spl
<=> c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f6569,plain,
( ~ sQ318_spl
| c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f6568]) ).
fof(f6577,plain,
( ~ sQ318_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6569,f1362]) ).
fof(f6578,plain,
~ sQ318_spl,
inference(contradiction_clause,[status(thm)],[f6577]) ).
fof(f6581,plain,
hBOOL(hAPP(c_Message_Oparts(c_Event_Obad),c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f1324,f6279]) ).
fof(f6582,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Event_Obad),c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f1324,f6278]) ).
fof(f6589,plain,
! [X0,X1] : hBOOL(hAPP(c_Message_Osynth(X0),c_Message_Omsg_OAgent(X1))),
inference(resolution,[status(thm)],[f1324,f876]) ).
fof(f6602,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,c_List_Olist_ONil(tc_Event_Oevent))),
inference(resolution,[status(thm)],[f1324,f907]) ).
fof(f6605,plain,
hBOOL(hAPP(c_Message_Oparts(c_Message_OsymKeys),v_K)),
inference(resolution,[status(thm)],[f1324,f6225]) ).
fof(f6606,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Message_OsymKeys),v_K)),
inference(resolution,[status(thm)],[f1324,f6224]) ).
fof(f6608,plain,
hBOOL(hAPP(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),v_evs2)),
inference(resolution,[status(thm)],[f1324,f6192]) ).
fof(f6609,plain,
hBOOL(hAPP(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),v_evs2)),
inference(resolution,[status(thm)],[f1324,f6191]) ).
fof(f6616,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Message_Oparts(c_Event_Obad),X0),
inference(resolution,[status(thm)],[f6581,f1322]) ).
fof(f6620,plain,
! [X0] : c_in(v_K,c_Message_Oparts(c_Message_OsymKeys),X0),
inference(resolution,[status(thm)],[f6605,f1322]) ).
fof(f6634,plain,
! [X0] : c_Set_Oinsert(c_Message_Oagent_OSpy,c_Message_Oparts(c_Event_Obad),X0) = c_Message_Oparts(c_Event_Obad),
inference(resolution,[status(thm)],[f6616,f1017]) ).
fof(f6644,plain,
! [X0] : c_Set_Oinsert(v_K,c_Message_Oparts(c_Message_OsymKeys),X0) = c_Message_Oparts(c_Message_OsymKeys),
inference(resolution,[status(thm)],[f6620,f1017]) ).
fof(f6684,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),X0),
inference(resolution,[status(thm)],[f6582,f1322]) ).
fof(f6693,plain,
! [X0] : c_Set_Oinsert(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),X0) = c_Message_Oanalz(c_Event_Obad),
inference(resolution,[status(thm)],[f6684,f1017]) ).
fof(f6697,plain,
! [X0,X1,X2] : c_in(c_Message_Omsg_OAgent(X0),c_Message_Osynth(X1),X2),
inference(resolution,[status(thm)],[f6589,f1322]) ).
fof(f6868,plain,
! [X0] : c_in(v_K,c_Message_Oanalz(c_Message_OsymKeys),X0),
inference(resolution,[status(thm)],[f6606,f1322]) ).
fof(f6882,plain,
! [X0] : c_Set_Oinsert(v_K,c_Message_Oanalz(c_Message_OsymKeys),X0) = c_Message_Oanalz(c_Message_OsymKeys),
inference(resolution,[status(thm)],[f6868,f1017]) ).
fof(f6886,plain,
! [X0] : c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,X0),
inference(resolution,[status(thm)],[f6602,f1322]) ).
fof(f6945,plain,
c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg),
inference(resolution,[status(thm)],[f6886,f1261]) ).
fof(f6948,plain,
! [X0] : c_Set_Oinsert(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,X0) = c_NS__Shared__Mirabelle_Ons__shared,
inference(resolution,[status(thm)],[f6886,f1017]) ).
fof(f6951,plain,
! [X0] : c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),X0),
inference(resolution,[status(thm)],[f6608,f1322]) ).
fof(f6962,plain,
! [X0] : c_Set_Oinsert(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),X0) = c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),
inference(resolution,[status(thm)],[f6951,f1017]) ).
fof(f6979,plain,
! [X0] : c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),X0),
inference(resolution,[status(thm)],[f6609,f1322]) ).
fof(f6988,plain,
! [X0] : c_Set_Oinsert(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),X0) = c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),
inference(resolution,[status(thm)],[f6979,f1017]) ).
fof(f7197,definition,
( sQ359_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f7199,plain,
( sQ359_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7197]) ).
fof(f7351,definition,
( sQ373_spl
<=> c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f7353,plain,
( sQ373_spl
| ~ c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7351]) ).
fof(f7364,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_Message_Oanalz(c_Set_Oinsert(X0,X1,X2)),X0)),
inference(resolution,[status(thm)],[f6316,f1324]) ).
fof(f7671,definition,
( sQ407_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f7673,plain,
( sQ407_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7671]) ).
fof(f7800,definition,
! [X1] :
( sQ410_spl
<=> ~ c_in(hAPP(c_Public_OshrK,X1),c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f7801,plain,
! [X0] :
( ~ sQ410_spl
| ~ c_in(hAPP(c_Public_OshrK,X0),c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7800]) ).
fof(f8037,definition,
( sQ412_spl
<=> c_in(v_evs2,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition]) ).
fof(f8039,plain,
( sQ412_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8037]) ).
fof(f8397,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1405,f1467]) ).
fof(f8398,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f8397]) ).
fof(f8399,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1409,f1456]) ).
fof(f8400,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f8399]) ).
fof(f8472,definition,
( sQ418_spl
<=> c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f8474,plain,
( sQ418_spl
| ~ c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8472]) ).
fof(f8479,definition,
( sQ420_spl
<=> c_in(v_evs2,c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f8481,plain,
( sQ420_spl
| ~ c_in(v_evs2,c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8479]) ).
fof(f8483,definition,
( sQ421_spl
<=> c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f8485,plain,
( sQ421_spl
| ~ c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8483]) ).
fof(f8490,definition,
( sQ423_spl
<=> c_in(v_K,c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition]) ).
fof(f8492,plain,
( sQ423_spl
| ~ c_in(v_K,c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8490]) ).
fof(f8497,definition,
( sQ425_spl
<=> c_in(v_K,c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition]) ).
fof(f8499,plain,
( sQ425_spl
| ~ c_in(v_K,c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8497]) ).
fof(f8504,definition,
( sQ427_spl
<=> c_in(v_K,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f8506,plain,
( sQ427_spl
| ~ c_in(v_K,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8504]) ).
fof(f8511,definition,
( sQ429_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f8513,plain,
( sQ429_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8511]) ).
fof(f8527,definition,
( sQ431_spl
<=> c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oanalz(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition]) ).
fof(f8529,plain,
( sQ431_spl
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oanalz(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8527]) ).
fof(f8543,definition,
! [X1] :
( sQ432_spl
<=> ~ c_in(hAPP(c_Public_OshrK,X1),c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f8544,plain,
! [X0] :
( ~ sQ432_spl
| ~ c_in(hAPP(c_Public_OshrK,X0),c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f8543]) ).
fof(f8550,plain,
( sQ431_spl
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f8529]) ).
fof(f8551,plain,
( sQ431_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8550,f1456]) ).
fof(f8552,plain,
sQ431_spl,
inference(contradiction_clause,[status(thm)],[f8551]) ).
fof(f8553,plain,
( sQ429_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8513,f6684]) ).
fof(f8554,plain,
sQ429_spl,
inference(contradiction_clause,[status(thm)],[f8553]) ).
fof(f8555,plain,
( sQ427_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8506,f6868]) ).
fof(f8556,plain,
sQ427_spl,
inference(contradiction_clause,[status(thm)],[f8555]) ).
fof(f8557,plain,
( sQ425_spl
| ~ c_in(v_K,c_Message_Oparts(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f8499]) ).
fof(f8558,plain,
( sQ425_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8557,f6620]) ).
fof(f8559,plain,
sQ425_spl,
inference(contradiction_clause,[status(thm)],[f8558]) ).
fof(f8560,plain,
( sQ423_spl
| ~ c_in(v_K,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f8492]) ).
fof(f8561,plain,
( sQ423_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8560,f6868]) ).
fof(f8562,plain,
sQ423_spl,
inference(contradiction_clause,[status(thm)],[f8561]) ).
fof(f8563,plain,
( sQ421_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8485,f6979]) ).
fof(f8564,plain,
sQ421_spl,
inference(contradiction_clause,[status(thm)],[f8563]) ).
fof(f8565,plain,
( sQ420_spl
| ~ c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f8481]) ).
fof(f8566,plain,
( sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8565,f6951]) ).
fof(f8567,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f8566]) ).
fof(f8568,plain,
( sQ418_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8474,f6945]) ).
fof(f8569,plain,
sQ418_spl,
inference(contradiction_clause,[status(thm)],[f8568]) ).
fof(f9226,definition,
( sQ434_spl
<=> c_in(v_evs2,c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f9228,plain,
( sQ434_spl
| ~ c_in(v_evs2,c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f9226]) ).
fof(f9236,definition,
( sQ436_spl
<=> c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f9238,plain,
( sQ436_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f9236]) ).
fof(f9247,plain,
( sQ434_spl
| ~ c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f9228]) ).
fof(f9248,plain,
( sQ434_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9247,f6979]) ).
fof(f9249,plain,
sQ434_spl,
inference(contradiction_clause,[status(thm)],[f9248]) ).
fof(f9376,plain,
! [X0,X1,X2,X3] : c_in(X0,c_Message_Oanalz(c_Set_Oinsert(X0,X1,X2)),X3),
inference(resolution,[status(thm)],[f7364,f1322]) ).
fof(f9463,plain,
! [X0,X1] : c_in(hAPP(c_Public_OshrK,X0),c_Message_Oanalz(c_Message_OsymKeys),X1),
inference(paramodulation,[status(thm)],[f6500,f9376]) ).
fof(f11350,plain,
! [X0,X1,X2,X3] : c_List_Olist_ONil(X0) != c_List_Oappend(c_List_Olist_OCons(X1,X2,X0),X3,X0),
inference(paramodulation,[status(thm)],[f917,f581]) ).
fof(f11801,definition,
( sQ506_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f11803,plain,
( sQ506_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f11801]) ).
fof(f11811,definition,
( sQ508_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition]) ).
fof(f11813,plain,
( sQ508_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f11811]) ).
fof(f11824,plain,
( sQ506_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oparts(c_Event_Obad),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f11803]) ).
fof(f11825,plain,
( sQ506_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11824,f6616]) ).
fof(f11826,plain,
sQ506_spl,
inference(contradiction_clause,[status(thm)],[f11825]) ).
fof(f12056,definition,
( sQ520_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f12058,plain,
( sQ520_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f12056]) ).
fof(f12066,definition,
( sQ522_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ522_spl])],[split_symbol_definition]) ).
fof(f12068,plain,
( sQ522_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f12066]) ).
fof(f12079,plain,
( sQ520_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Event_Obad),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f12058]) ).
fof(f12080,plain,
( sQ520_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12079,f6684]) ).
fof(f12081,plain,
sQ520_spl,
inference(contradiction_clause,[status(thm)],[f12080]) ).
fof(f12183,definition,
( sQ523_spl
<=> c_Orderings_Otop__class_Otop(tc_bool) = c_Orderings_Otop__class_Otop(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f12185,plain,
( sQ523_spl
| c_Orderings_Otop__class_Otop(tc_bool) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(component_clause,[status(thm)],[f12183]) ).
fof(f12189,plain,
( sQ523_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f12185]) ).
fof(f12190,plain,
sQ523_spl,
inference(contradiction_clause,[status(thm)],[f12189]) ).
fof(f12195,plain,
! [X0,X1] : c_in(X0,c_Message_Osynth(c_Set_Oinsert(X0,X1,tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f927,f676]) ).
fof(f12285,definition,
! [X0] :
( sQ525_spl
<=> X0 = v_evs2 ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f12286,plain,
! [X0] :
( ~ sQ525_spl
| X0 = v_evs2 ),
inference(component_clause,[status(thm)],[f12285]) ).
fof(f12404,plain,
( ~ sQ525_spl
| $false ),
inference(resolution,[status(thm)],[f12286,f1196]) ).
fof(f12453,plain,
~ sQ525_spl,
inference(contradiction_clause,[status(thm)],[f12404]) ).
fof(f12620,definition,
! [X0] :
( sQ536_spl
<=> X0 = v_K ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f12621,plain,
! [X0] :
( ~ sQ536_spl
| X0 = v_K ),
inference(component_clause,[status(thm)],[f12620]) ).
fof(f12630,plain,
( ~ sQ536_spl
| $false ),
inference(resolution,[status(thm)],[f12621,f1196]) ).
fof(f12666,plain,
~ sQ536_spl,
inference(contradiction_clause,[status(thm)],[f12630]) ).
fof(f14931,definition,
( sQ613_spl
<=> class_HOL_Oord(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f14933,plain,
( sQ613_spl
| ~ class_HOL_Oord(tc_bool) ),
inference(component_clause,[status(thm)],[f14931]) ).
fof(f15082,definition,
( sQ651_spl
<=> class_HOL_Oord(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f15084,plain,
( sQ651_spl
| ~ class_HOL_Oord(tc_nat) ),
inference(component_clause,[status(thm)],[f15082]) ).
fof(f15093,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14933,f1400]) ).
fof(f15094,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f15093]) ).
fof(f15095,plain,
( sQ651_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15084,f1392]) ).
fof(f15096,plain,
sQ651_spl,
inference(contradiction_clause,[status(thm)],[f15095]) ).
fof(f15192,plain,
( ~ sQ432_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8544,f9463]) ).
fof(f15193,plain,
~ sQ432_spl,
inference(contradiction_clause,[status(thm)],[f15192]) ).
fof(f17133,definition,
! [X1] :
( sQ705_spl
<=> c_List_Olist_ONil(tc_Event_Oevent) = X1 ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f17134,plain,
! [X0] :
( ~ sQ705_spl
| c_List_Olist_ONil(tc_Event_Oevent) = X0 ),
inference(component_clause,[status(thm)],[f17133]) ).
fof(f17137,plain,
( ~ sQ705_spl
| $false ),
inference(resolution,[status(thm)],[f17134,f11350]) ).
fof(f17182,plain,
~ sQ705_spl,
inference(contradiction_clause,[status(thm)],[f17137]) ).
fof(f17572,plain,
c_in(c_List_Olist_ONil(tc_Event_Oevent),c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6948,f12195]) ).
fof(f17573,plain,
c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6988,f12195]) ).
fof(f17574,plain,
c_in(v_evs2,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6962,f12195]) ).
fof(f17575,plain,
c_in(v_evs2,c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6193,f12195]) ).
fof(f17576,plain,
c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6882,f12195]) ).
fof(f17577,plain,
c_in(v_K,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6644,f12195]) ).
fof(f17578,plain,
c_in(v_K,c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6226,f12195]) ).
fof(f17579,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6693,f12195]) ).
fof(f17580,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6634,f12195]) ).
fof(f17581,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Event_Obad),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6280,f12195]) ).
fof(f17609,plain,
! [X0] : c_in(hAPP(c_Public_OshrK,X0),c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f6500,f12195]) ).
fof(f17621,plain,
( sQ373_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17572,f7353]) ).
fof(f17622,plain,
sQ373_spl,
inference(contradiction_clause,[status(thm)],[f17621]) ).
fof(f17623,plain,
( sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17573,f9238]) ).
fof(f17624,plain,
sQ436_spl,
inference(contradiction_clause,[status(thm)],[f17623]) ).
fof(f17625,plain,
( sQ412_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17574,f8039]) ).
fof(f17626,plain,
sQ412_spl,
inference(contradiction_clause,[status(thm)],[f17625]) ).
fof(f17627,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17575,f6307]) ).
fof(f17628,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f17627]) ).
fof(f17629,plain,
( sQ407_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17576,f7673]) ).
fof(f17630,plain,
sQ407_spl,
inference(contradiction_clause,[status(thm)],[f17629]) ).
fof(f17631,plain,
( sQ359_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17577,f7199]) ).
fof(f17632,plain,
sQ359_spl,
inference(contradiction_clause,[status(thm)],[f17631]) ).
fof(f17633,plain,
( sQ310_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17578,f6362]) ).
fof(f17634,plain,
sQ310_spl,
inference(contradiction_clause,[status(thm)],[f17633]) ).
fof(f17635,plain,
( sQ522_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17579,f12068]) ).
fof(f17636,plain,
sQ522_spl,
inference(contradiction_clause,[status(thm)],[f17635]) ).
fof(f17637,plain,
( sQ508_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17580,f11813]) ).
fof(f17638,plain,
sQ508_spl,
inference(contradiction_clause,[status(thm)],[f17637]) ).
fof(f17639,plain,
( sQ312_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17581,f6390]) ).
fof(f17640,plain,
sQ312_spl,
inference(contradiction_clause,[status(thm)],[f17639]) ).
fof(f17642,plain,
( ~ sQ410_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17609,f7801]) ).
fof(f17643,plain,
~ sQ410_spl,
inference(contradiction_clause,[status(thm)],[f17642]) ).
fof(f17646,plain,
c_in(v_evs2,c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f17575,f1261]) ).
fof(f17655,plain,
hBOOL(hAPP(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),v_evs2)),
inference(resolution,[status(thm)],[f17575,f1324]) ).
fof(f17832,plain,
c_in(v_K,c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f17578,f1261]) ).
fof(f17841,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_OsymKeys),v_K)),
inference(resolution,[status(thm)],[f17578,f1324]) ).
fof(f17877,plain,
c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),tc_Message_Omsg),
inference(resolution,[status(thm)],[f17581,f1261]) ).
fof(f17886,plain,
hBOOL(hAPP(c_Message_Osynth(c_Event_Obad),c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f17581,f1324]) ).
fof(f18165,plain,
! [X0] : c_in(v_evs2,c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),X0),
inference(resolution,[status(thm)],[f17655,f1322]) ).
fof(f18308,definition,
( sQ718_spl
<=> c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition]) ).
fof(f18310,plain,
( sQ718_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18308]) ).
fof(f18315,definition,
( sQ720_spl
<=> c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition]) ).
fof(f18317,plain,
( sQ720_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18315]) ).
fof(f18323,definition,
( sQ722_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f18325,plain,
( sQ722_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18323]) ).
fof(f18330,definition,
( sQ724_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition]) ).
fof(f18332,plain,
( sQ724_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18330]) ).
fof(f18341,definition,
( sQ727_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Event_Obad))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition]) ).
fof(f18343,plain,
( sQ727_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Message_Oanalz(c_Event_Obad))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18341]) ).
fof(f18348,definition,
( sQ729_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Event_Obad))),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ729_spl])],[split_symbol_definition]) ).
fof(f18350,plain,
( sQ729_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Message_Oparts(c_Event_Obad))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f18348]) ).
fof(f18493,plain,
( sQ729_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oparts(c_Event_Obad)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f18350]) ).
fof(f18494,plain,
( sQ727_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f18343]) ).
fof(f18495,plain,
( sQ724_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f18332]) ).
fof(f18496,plain,
( sQ722_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f18325]) ).
fof(f18497,plain,
( sQ720_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1273,f18317]) ).
fof(f18498,plain,
( sQ718_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f1237,f18310]) ).
fof(f18605,plain,
! [X0] : c_in(v_K,c_Message_Osynth(c_Message_OsymKeys),X0),
inference(resolution,[status(thm)],[f17841,f1322]) ).
fof(f18806,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Event_Obad),X0),
inference(resolution,[status(thm)],[f17886,f1322]) ).
fof(f19060,definition,
( sQ759_spl
<=> c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)) = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) ),
introduced(definition,[new_symbols(definition,[sQ759_spl])],[split_symbol_definition]) ).
fof(f19061,plain,
( ~ sQ759_spl
| c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)) = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) ),
inference(component_clause,[status(thm)],[f19060]) ).
fof(f19067,definition,
( sQ761_spl
<=> c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa))) = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) ),
introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition]) ).
fof(f19068,plain,
( ~ sQ761_spl
| c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa))) = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) ),
inference(component_clause,[status(thm)],[f19067]) ).
fof(f19072,plain,
( ~ sQ761_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19068,f1311]) ).
fof(f19073,plain,
~ sQ761_spl,
inference(contradiction_clause,[status(thm)],[f19072]) ).
fof(f19074,plain,
( ~ sQ759_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19061,f1311]) ).
fof(f19075,plain,
~ sQ759_spl,
inference(contradiction_clause,[status(thm)],[f19074]) ).
fof(f19864,plain,
hBOOL(hAPP(c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f17579,f1324]) ).
fof(f19901,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),v_evs2)),
inference(resolution,[status(thm)],[f17646,f1324]) ).
fof(f20464,plain,
~ c_List_Odistinct(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),v_evs2,tc_Event_Oevent),tc_Event_Oevent),
inference(resolution,[status(thm)],[f1058,f1441]) ).
fof(f20498,definition,
( sQ804_spl
<=> c_List_Odistinct(c_List_Oremdups(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),v_evs2,tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ804_spl])],[split_symbol_definition]) ).
fof(f20500,plain,
( sQ804_spl
| ~ c_List_Odistinct(c_List_Oremdups(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))),v_evs2,tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f20498]) ).
fof(f20502,plain,
( sQ804_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20500,f604]) ).
fof(f20503,plain,
sQ804_spl,
inference(contradiction_clause,[status(thm)],[f20502]) ).
fof(f20733,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys)),v_K)),
inference(resolution,[status(thm)],[f17832,f1324]) ).
fof(f20773,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f17877,f1324]) ).
fof(f20982,plain,
( sQ724_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18495,f17577]) ).
fof(f20983,plain,
sQ724_spl,
inference(contradiction_clause,[status(thm)],[f20982]) ).
fof(f20985,plain,
( sQ729_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18493,f17580]) ).
fof(f20986,plain,
sQ729_spl,
inference(contradiction_clause,[status(thm)],[f20985]) ).
fof(f20988,plain,
( sQ727_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18494,f17579]) ).
fof(f20989,plain,
sQ727_spl,
inference(contradiction_clause,[status(thm)],[f20988]) ).
fof(f21093,plain,
( sQ722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18496,f17576]) ).
fof(f21094,plain,
sQ722_spl,
inference(contradiction_clause,[status(thm)],[f21093]) ).
fof(f21096,plain,
( sQ720_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18497,f17574]) ).
fof(f21097,plain,
sQ720_spl,
inference(contradiction_clause,[status(thm)],[f21096]) ).
fof(f21099,plain,
( sQ718_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18498,f17573]) ).
fof(f21100,plain,
sQ718_spl,
inference(contradiction_clause,[status(thm)],[f21099]) ).
fof(f21683,definition,
( sQ827_spl
<=> c_List_Odistinct(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),v_evs2,tc_Event_Oevent),tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ827_spl])],[split_symbol_definition]) ).
fof(f21684,plain,
( ~ sQ827_spl
| c_List_Odistinct(c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),v_evs2,tc_Event_Oevent),tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f21683]) ).
fof(f21690,definition,
( sQ829_spl
<=> c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),v_evs2,tc_Event_Oevent) = c_List_Olist_ONil(tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f21691,plain,
( ~ sQ829_spl
| c_List_Olist_OCons(c_Event_Oevent_OSays(v_A_H,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_ONonce(v_NAa)))),v_evs2,tc_Event_Oevent) = c_List_Olist_ONil(tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f21690]) ).
fof(f21694,plain,
( ~ sQ829_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21691,f581]) ).
fof(f21695,plain,
~ sQ829_spl,
inference(contradiction_clause,[status(thm)],[f21694]) ).
fof(f21696,plain,
( ~ sQ827_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21684,f20464]) ).
fof(f21697,plain,
~ sQ827_spl,
inference(contradiction_clause,[status(thm)],[f21696]) ).
fof(f21881,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),X0),
inference(resolution,[status(thm)],[f19864,f1322]) ).
fof(f21939,plain,
! [X0] : c_in(v_evs2,c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),X0),
inference(resolution,[status(thm)],[f19901,f1322]) ).
fof(f22751,plain,
! [X0] : c_in(v_K,c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys)),X0),
inference(resolution,[status(thm)],[f20733,f1322]) ).
fof(f22902,definition,
( sQ852_spl
<=> c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ852_spl])],[split_symbol_definition]) ).
fof(f22904,plain,
( sQ852_spl
| ~ c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f22902]) ).
fof(f22906,plain,
( sQ852_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22904,f656]) ).
fof(f22907,plain,
sQ852_spl,
inference(contradiction_clause,[status(thm)],[f22906]) ).
fof(f22933,plain,
! [X0] : c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),X0),
inference(resolution,[status(thm)],[f20773,f1322]) ).
fof(f23838,definition,
( sQ889_spl
<=> c_in(v_evs2,c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ889_spl])],[split_symbol_definition]) ).
fof(f23840,plain,
( sQ889_spl
| ~ c_in(v_evs2,c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f23838]) ).
fof(f23845,definition,
( sQ891_spl
<=> c_in(v_evs2,c_Message_Osynth(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ891_spl])],[split_symbol_definition]) ).
fof(f23847,plain,
( sQ891_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f23845]) ).
fof(f23854,plain,
( sQ891_spl
| ~ c_in(v_evs2,c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f951,f23847]) ).
fof(f23855,plain,
( sQ891_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23854,f18165]) ).
fof(f23856,plain,
sQ891_spl,
inference(contradiction_clause,[status(thm)],[f23855]) ).
fof(f23857,plain,
( sQ889_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23840,f21939]) ).
fof(f23858,plain,
sQ889_spl,
inference(contradiction_clause,[status(thm)],[f23857]) ).
fof(f24817,plain,
c_in(c_Message_OinvKey(v_K),c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat),
inference(resolution,[status(thm)],[f1127,f1456]) ).
fof(f24837,plain,
c_in(v_K,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat),
inference(forward_demodulation,[status(thm)],[f2245,f24817]) ).
fof(f25107,definition,
( sQ938_spl
<=> c_in(v_K,c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ938_spl])],[split_symbol_definition]) ).
fof(f25109,plain,
( sQ938_spl
| ~ c_in(v_K,c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f25107]) ).
fof(f25114,definition,
( sQ940_spl
<=> c_in(v_K,c_Message_Osynth(c_Message_Osynth(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ940_spl])],[split_symbol_definition]) ).
fof(f25116,plain,
( sQ940_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_Osynth(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f25114]) ).
fof(f25123,plain,
( sQ940_spl
| ~ c_in(v_K,c_Message_Osynth(c_Message_OsymKeys),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f951,f25116]) ).
fof(f25124,plain,
( sQ940_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25123,f18605]) ).
fof(f25125,plain,
sQ940_spl,
inference(contradiction_clause,[status(thm)],[f25124]) ).
fof(f25126,plain,
( sQ938_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25109,f22751]) ).
fof(f25127,plain,
sQ938_spl,
inference(contradiction_clause,[status(thm)],[f25126]) ).
fof(f25223,definition,
( sQ947_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition]) ).
fof(f25225,plain,
( sQ947_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f25223]) ).
fof(f25230,definition,
( sQ949_spl
<=> c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Osynth(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ949_spl])],[split_symbol_definition]) ).
fof(f25232,plain,
( sQ949_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Message_Osynth(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f25230]) ).
fof(f25239,plain,
( sQ949_spl
| ~ c_in(c_Message_Oagent_OSpy,c_Message_Osynth(c_Event_Obad),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f951,f25232]) ).
fof(f25240,plain,
( sQ949_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25239,f18806]) ).
fof(f25241,plain,
sQ949_spl,
inference(contradiction_clause,[status(thm)],[f25240]) ).
fof(f25242,plain,
( sQ947_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25225,f22933]) ).
fof(f25243,plain,
sQ947_spl,
inference(contradiction_clause,[status(thm)],[f25242]) ).
fof(f25765,definition,
( sQ951_spl
<=> c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
introduced(definition,[new_symbols(definition,[sQ951_spl])],[split_symbol_definition]) ).
fof(f25766,plain,
( ~ sQ951_spl
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(component_clause,[status(thm)],[f25765]) ).
fof(f25781,plain,
( ~ sQ951_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25766,f1356]) ).
fof(f25782,plain,
~ sQ951_spl,
inference(contradiction_clause,[status(thm)],[f25781]) ).
fof(f27656,definition,
! [X0] :
( sQ1000_spl
<=> ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ1000_spl])],[split_symbol_definition]) ).
fof(f27657,plain,
! [X0] :
( ~ sQ1000_spl
| ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f27656]) ).
fof(f27662,plain,
( ~ sQ1000_spl
| $false ),
inference(resolution,[status(thm)],[f27657,f6697]) ).
fof(f27664,plain,
~ sQ1000_spl,
inference(contradiction_clause,[status(thm)],[f27662]) ).
fof(f27980,definition,
! [X0] :
( sQ1003_spl
<=> ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ1003_spl])],[split_symbol_definition]) ).
fof(f27981,plain,
! [X0] :
( ~ sQ1003_spl
| ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f27980]) ).
fof(f28040,definition,
( sQ1012_spl
<=> c_in(hAPP(c_Public_OshrK,v_B),c_Message_OsymKeys,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ1012_spl])],[split_symbol_definition]) ).
fof(f28042,plain,
( sQ1012_spl
| ~ c_in(hAPP(c_Public_OshrK,v_B),c_Message_OsymKeys,tc_nat) ),
inference(component_clause,[status(thm)],[f28040]) ).
fof(f28044,plain,
( sQ1012_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28042,f6329]) ).
fof(f28045,plain,
sQ1012_spl,
inference(contradiction_clause,[status(thm)],[f28044]) ).
fof(f28075,plain,
( ~ sQ1003_spl
| $false ),
inference(resolution,[status(thm)],[f27981,f6697]) ).
fof(f28077,plain,
~ sQ1003_spl,
inference(contradiction_clause,[status(thm)],[f28075]) ).
fof(f28421,definition,
! [X0] :
( sQ1016_spl
<=> ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ1016_spl])],[split_symbol_definition]) ).
fof(f28422,plain,
! [X0] :
( ~ sQ1016_spl
| ~ c_in(X0,c_Message_Osynth(c_Message_Oanalz(c_Event_Obad)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f28421]) ).
fof(f28557,plain,
( ~ sQ1016_spl
| $false ),
inference(resolution,[status(thm)],[f28422,f21881]) ).
fof(f28559,plain,
~ sQ1016_spl,
inference(contradiction_clause,[status(thm)],[f28557]) ).
fof(f29348,plain,
( ~ sQ316_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6540,f1357]) ).
fof(f29349,plain,
~ sQ316_spl,
inference(contradiction_clause,[status(thm)],[f29348]) ).
fof(f29350,plain,
( c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg)
| ~ c_in(v_K,c_Message_OsymKeys,tc_nat)
| ~ c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f1217,f24837]) ).
fof(f29361,plain,
( sQ213_spl
| ~ sQ70_spl
| ~ sQ188_spl ),
inference(split_clause,[status(thm)],[f29350,f3906,f2256,f4078]) ).
fof(f29367,plain,
$false,
inference(sat_refutation,[status(thm)],[f3739,f3911,f4084,f6578,f8398,f8400,f8552,f8554,f8556,f8559,f8562,f8564,f8567,f8569,f9249,f11826,f12081,f12190,f12453,f12666,f15094,f15096,f15193,f17182,f17622,f17624,f17626,f17628,f17630,f17632,f17634,f17636,f17638,f17640,f17643,f19073,f19075,f20503,f20983,f20986,f20989,f21094,f21097,f21100,f21695,f21697,f22907,f23856,f23858,f25125,f25127,f25241,f25243,f25782,f27664,f28045,f28077,f28559,f29349,f29361]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV801-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.54 % Computer : n001.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.55 % WCLimit : 300
% 0.10/0.55 % DateTime : Mon Sep 21 09:31:30 UTC 2026
% 0.10/0.55 % CPUTime :
% 0.14/0.59 % Drodi V4.1.1
% 37.93/5.43 % Refutation found
% 37.93/5.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 37.93/5.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.60/5.66 % Elapsed time: 5.091969 seconds
% 2.60/5.66 % CPU time: 38.801294 seconds
% 2.60/5.66 % Total memory used: 530.528 MB
% 2.60/5.66 % Net memory used: 502.323 MB
%------------------------------------------------------------------------------