%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV803-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 : Tue Sep 29 01:19:32 PM UTC 2026
% Result : Unsatisfiable 6.72s 2.61s
% Output : Refutation 14.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 74
% Syntax : Number of formulae : 368 ( 100 unt; 52 def)
% Number of atoms : 807 ( 121 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 859 ( 420 ~; 414 |; 0 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 26 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 48 con; 0-4 aty)
% Number of variables : 491 ( 0 sgn 491 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f526,axiom,
! [X2,X3,X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,X1,X2,X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0)))))))),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(X1,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_B__trusts__NS3_0) ).
fof(f531,axiom,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ 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(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X6))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| X0 = X1
| ~ 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(X7,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X9))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_unique__session__keys_0) ).
fof(f533,axiom,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ 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(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X9))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X5),X6))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_unique__session__keys_2) ).
fof(f534,axiom,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ 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(X9),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X6),X0))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X6),X1))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_unique__session__keys_3) ).
fof(f541,axiom,
! [X2,X3,X0,X1,X4,X5] :
( 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,X3),X4))))),c_List_Oset(X5,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X5,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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,X3),X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X5)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_A__trusts__NS2_0) ).
fof(f550,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz_OSnd_0) ).
fof(f551,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X2),c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz_OFst_0) ).
fof(f552,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts_OSnd_0) ).
fof(f563,axiom,
! [X2,X3,X0,X1] :
( ~ 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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Says__imp__parts__knows__Spy_0) ).
fof(f575,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts_OBody_0) ).
fof(f579,axiom,
! [X2,X3,X0,X1] :
( ~ 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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Says__imp__analz__Spy_0) ).
fof(f581,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X0 = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3)))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X3,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cert__A__form_1) ).
fof(f582,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X3,c_Event_Obad,tc_Message_Oagent))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3))) = X0 ),
inference(reorient_equations,[],[f581]) ).
fof(f609,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| ~ hBOOL(c_in(X2,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__Spy__analz__bad_0) ).
fof(f618,axiom,
! [X0,X1] :
( ~ hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_analz__conj__parts_0) ).
fof(f619,negated_conjecture,
~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f620,negated_conjecture,
~ hBOOL(c_in(v_B,c_Event_Obad,tc_Message_Oagent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f621,negated_conjecture,
hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f624,negated_conjecture,
hBOOL(c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_Xa))))),c_List_Oset(v_evs5,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f625,negated_conjecture,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f626,negated_conjecture,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(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_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f627,negated_conjecture,
v_K = v_Ka,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f628,plain,
v_Ka = v_K,
inference(reorient_equations,[],[f627]) ).
fof(f632,negated_conjecture,
( v_B != v_Ba
| v_A != v_Aa ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_11) ).
fof(f669,plain,
hBOOL(c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_Xa))))),c_List_Oset(v_evs5,tc_Event_Oevent),tc_Event_Oevent)),
inference(definition_unfolding,[],[f624,f628]) ).
fof(f671,definition,
sF0 = c_in(v_A,c_Event_Obad,tc_Message_Oagent),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f672,plain,
c_in(v_A,c_Event_Obad,tc_Message_Oagent) = sF0,
inference(reorient_equations,[],[f671]) ).
fof(f673,plain,
~ hBOOL(sF0),
inference(definition_folding,[],[f619,f672]) ).
fof(f674,definition,
sF1 = c_in(v_B,c_Event_Obad,tc_Message_Oagent),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f675,plain,
c_in(v_B,c_Event_Obad,tc_Message_Oagent) = sF1,
inference(reorient_equations,[],[f674]) ).
fof(f676,plain,
~ hBOOL(sF1),
inference(definition_folding,[],[f620,f675]) ).
fof(f677,definition,
sF2 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f678,plain,
tc_List_Olist(tc_Event_Oevent) = sF2,
inference(reorient_equations,[],[f677]) ).
fof(f679,definition,
sF3 = c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f680,plain,
c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2) = sF3,
inference(reorient_equations,[],[f679]) ).
fof(f681,plain,
hBOOL(sF3),
inference(definition_folding,[],[f621,f680,f678]) ).
fof(f691,definition,
sF8 = c_List_Oset(v_evs5,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f692,plain,
c_List_Oset(v_evs5,tc_Event_Oevent) = sF8,
inference(reorient_equations,[],[f691]) ).
fof(f696,definition,
sF10 = hAPP(c_Public_OshrK,v_Aa),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f697,plain,
hAPP(c_Public_OshrK,v_Aa) = sF10,
inference(reorient_equations,[],[f696]) ).
fof(f698,definition,
sF11 = c_Message_Omsg_ONonce(v_NAa),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f699,plain,
c_Message_Omsg_ONonce(v_NAa) = sF11,
inference(reorient_equations,[],[f698]) ).
fof(f700,definition,
sF12 = c_Message_Omsg_OAgent(v_Ba),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f701,plain,
c_Message_Omsg_OAgent(v_Ba) = sF12,
inference(reorient_equations,[],[f700]) ).
fof(f702,definition,
sF13 = hAPP(c_Message_Omsg_OKey,v_K),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f703,plain,
hAPP(c_Message_Omsg_OKey,v_K) = sF13,
inference(reorient_equations,[],[f702]) ).
fof(f704,definition,
sF14 = c_Message_Omsg_OMPair(sF13,v_Xa),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f705,plain,
c_Message_Omsg_OMPair(sF13,v_Xa) = sF14,
inference(reorient_equations,[],[f704]) ).
fof(f706,definition,
sF15 = c_Message_Omsg_OMPair(sF12,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f707,plain,
c_Message_Omsg_OMPair(sF12,sF14) = sF15,
inference(reorient_equations,[],[f706]) ).
fof(f708,definition,
sF16 = c_Message_Omsg_OMPair(sF11,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f709,plain,
c_Message_Omsg_OMPair(sF11,sF15) = sF16,
inference(reorient_equations,[],[f708]) ).
fof(f710,definition,
sF17 = c_Message_Omsg_OCrypt(sF10,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f711,plain,
c_Message_Omsg_OCrypt(sF10,sF16) = sF17,
inference(reorient_equations,[],[f710]) ).
fof(f712,definition,
sF18 = c_Event_Oevent_OSays(v_S,v_Aa,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f713,plain,
c_Event_Oevent_OSays(v_S,v_Aa,sF17) = sF18,
inference(reorient_equations,[],[f712]) ).
fof(f714,definition,
sF19 = c_in(sF18,sF8,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f715,plain,
c_in(sF18,sF8,tc_Event_Oevent) = sF19,
inference(reorient_equations,[],[f714]) ).
fof(f716,plain,
hBOOL(sF19),
inference(definition_folding,[],[f669,f715,f692,f713,f711,f709,f707,f705,f703,f701,f699,f697]) ).
fof(f717,definition,
sF20 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f718,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5) = sF20,
inference(reorient_equations,[],[f717]) ).
fof(f719,definition,
sF21 = c_Message_Oanalz(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f720,plain,
c_Message_Oanalz(sF20) = sF21,
inference(reorient_equations,[],[f719]) ).
fof(f721,definition,
sF22 = c_in(sF13,sF21,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f722,plain,
c_in(sF13,sF21,tc_Message_Omsg) = sF22,
inference(reorient_equations,[],[f721]) ).
fof(f723,plain,
~ hBOOL(sF22),
inference(definition_folding,[],[f625,f722,f720,f718,f703]) ).
fof(f724,definition,
sF23 = hAPP(c_Public_OshrK,v_A),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f725,plain,
hAPP(c_Public_OshrK,v_A) = sF23,
inference(reorient_equations,[],[f724]) ).
fof(f726,definition,
sF24 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f727,plain,
c_Message_Omsg_ONonce(v_NA) = sF24,
inference(reorient_equations,[],[f726]) ).
fof(f728,definition,
sF25 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f729,plain,
c_Message_Omsg_OAgent(v_B) = sF25,
inference(reorient_equations,[],[f728]) ).
fof(f730,definition,
sF26 = c_Message_Omsg_OMPair(sF13,v_X),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f731,plain,
c_Message_Omsg_OMPair(sF13,v_X) = sF26,
inference(reorient_equations,[],[f730]) ).
fof(f732,definition,
sF27 = c_Message_Omsg_OMPair(sF25,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f733,plain,
c_Message_Omsg_OMPair(sF25,sF26) = sF27,
inference(reorient_equations,[],[f732]) ).
fof(f734,definition,
sF28 = c_Message_Omsg_OMPair(sF24,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f735,plain,
c_Message_Omsg_OMPair(sF24,sF27) = sF28,
inference(reorient_equations,[],[f734]) ).
fof(f736,definition,
sF29 = c_Message_Omsg_OCrypt(sF23,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f737,plain,
c_Message_Omsg_OCrypt(sF23,sF28) = sF29,
inference(reorient_equations,[],[f736]) ).
fof(f738,definition,
sF30 = c_Message_Oparts(sF20),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f739,plain,
c_Message_Oparts(sF20) = sF30,
inference(reorient_equations,[],[f738]) ).
fof(f740,definition,
sF31 = c_in(sF29,sF30,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f741,plain,
c_in(sF29,sF30,tc_Message_Omsg) = sF31,
inference(reorient_equations,[],[f740]) ).
fof(f742,plain,
hBOOL(sF31),
inference(definition_folding,[],[f626,f741,f739,f718,f737,f735,f733,f731,f703,f729,f727,f725]) ).
fof(f760,definition,
( spl37_1
<=> hBOOL(sF31) ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
fof(f761,plain,
( hBOOL(sF31)
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f773,definition,
( spl37_4
<=> v_A = v_Aa ),
introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition]) ).
fof(f775,plain,
( v_A != v_Aa
| spl37_4 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f777,definition,
( spl37_5
<=> v_B = v_Ba ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
fof(f778,plain,
( v_B = v_Ba
| ~ spl37_5 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f779,plain,
( v_B != v_Ba
| spl37_5 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f780,plain,
( ~ spl37_4
| ~ spl37_5 ),
inference(avatar_split_clause,[],[f632,f777,f773]) ).
fof(f782,plain,
spl37_1,
inference(avatar_split_clause,[],[f742,f760]) ).
fof(f817,definition,
( spl37_6
<=> hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
fof(f818,plain,
( hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ spl37_6 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f819,plain,
( ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| spl37_6 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f824,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),X1),c_Message_Oanalz(sF20),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(X1,c_Message_Oanalz(sF20),tc_Message_Omsg)) ),
inference(superposition,[],[f609,f718]) ).
fof(f825,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),X1),sF21,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(X1,c_Message_Oanalz(sF20),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f824,f720]) ).
fof(f826,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),X1),sF21,tc_Message_Omsg))
| hBOOL(c_in(X1,sF21,tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(forward_demodulation,[],[f825,f720]) ).
fof(f901,plain,
! [X2,X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,X2),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(v_B,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)) ),
inference(superposition,[],[f526,f729]) ).
fof(f917,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,X2),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(v_B,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f901,f678]) ).
fof(f933,plain,
! [X2,X0,X1] :
( hBOOL(sF1)
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,X2),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f917,f675]) ).
fof(f936,plain,
! [X2,X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,X2),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X2,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)) ),
inference(forward_subsumption_resolution,[],[f933,f676]) ).
fof(f959,plain,
! [X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(superposition,[],[f936,f692]) ).
fof(f960,plain,
! [X0,X1] :
( ~ hBOOL(sF3)
| 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f959,f680]) ).
fof(f961,plain,
! [X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(forward_subsumption_resolution,[],[f960,f681]) ).
fof(f962,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(sF20),tc_Message_Omsg))
| 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f961,f718]) ).
fof(f963,plain,
! [X0,X1] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,X1,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X0))),sF30,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f962,f739]) ).
fof(f974,plain,
! [X0] :
( 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(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,v_B,v_K,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(X0)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(X0))),sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f963,f703]) ).
fof(f1009,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ 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(sF13,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)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| X3 = X8 ),
inference(superposition,[],[f534,f703]) ).
fof(f1013,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ 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(sF13,X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| X3 = X8 ),
inference(forward_demodulation,[],[f1009,f678]) ).
fof(f1033,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| X3 = X7 ),
inference(superposition,[],[f1013,f692]) ).
fof(f1034,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(sF3)
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| X3 = X7 ),
inference(forward_demodulation,[],[f1033,f680]) ).
fof(f1035,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| X3 = X7 ),
inference(forward_subsumption_resolution,[],[f1034,f681]) ).
fof(f1044,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ 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(sF13,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)))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| X2 = X7 ),
inference(superposition,[],[f533,f703]) ).
fof(f1048,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ 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(sF13,X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| X2 = X7 ),
inference(forward_demodulation,[],[f1044,f678]) ).
fof(f1068,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| X2 = X6 ),
inference(superposition,[],[f1048,f692]) ).
fof(f1069,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(sF3)
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| X2 = X6 ),
inference(forward_demodulation,[],[f1068,f680]) ).
fof(f1070,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| X2 = X6 ),
inference(forward_subsumption_resolution,[],[f1069,f681]) ).
fof(f1081,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ 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(sF13,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)))
| X0 = X5
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(superposition,[],[f531,f703]) ).
fof(f1085,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X5,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X5),c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X7),c_Message_Omsg_OMPair(sF13,X8))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ 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(sF13,X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| X0 = X5
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2)) ),
inference(forward_demodulation,[],[f1081,f678]) ).
fof(f1105,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| X0 = X4
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2)) ),
inference(superposition,[],[f1085,f692]) ).
fof(f1106,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(sF3)
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| X0 = X4 ),
inference(forward_demodulation,[],[f1105,f680]) ).
fof(f1107,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X4,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X4),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X6),c_Message_Omsg_OMPair(sF13,X7))))),sF8,tc_Event_Oevent))
| ~ 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(sF13,X3))))),sF8,tc_Event_Oevent))
| X0 = X4 ),
inference(forward_subsumption_resolution,[],[f1106,f681]) ).
fof(f1149,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(superposition,[],[f582,f725]) ).
fof(f1160,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))
| hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_demodulation,[],[f1149,f678]) ).
fof(f1164,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(sF0)
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_demodulation,[],[f1160,f672]) ).
fof(f1166,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_subsumption_resolution,[],[f1164,f673]) ).
fof(f1172,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(sF20),tc_Message_Omsg))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(superposition,[],[f1166,f718]) ).
fof(f1173,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),sF30,tc_Message_Omsg))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_demodulation,[],[f1172,f739]) ).
fof(f1174,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(sF3)
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),sF30,tc_Message_Omsg))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_demodulation,[],[f1173,f680]) ).
fof(f1175,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),sF30,tc_Message_Omsg))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3 ),
inference(forward_subsumption_resolution,[],[f1174,f681]) ).
fof(f1186,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))) = X2 ),
inference(superposition,[],[f1175,f703]) ).
fof(f1190,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF26))),sF30,tc_Message_Omsg))
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))) ),
inference(superposition,[],[f1186,f731]) ).
fof(f1220,plain,
! [X2,X3,X0,X1,X4] :
( 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(sF13,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)))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)) ),
inference(superposition,[],[f541,f703]) ).
fof(f1227,plain,
! [X2,X3,X0,X1,X4] :
( 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(sF13,X3))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))
| ~ hBOOL(c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1220,f678]) ).
fof(f1266,plain,
! [X2,X3,X0,X1] :
( 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(v_evs5,c_NS__Shared__Mirabelle_Ons__shared,sF2))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(superposition,[],[f1227,f692]) ).
fof(f1271,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(sF3)
| 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(sF13,X3))))),sF8,tc_Event_Oevent))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1266,f680]) ).
fof(f1273,plain,
! [X2,X3,X0,X1] :
( 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(sF13,X3))))),sF8,tc_Event_Oevent))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(forward_subsumption_resolution,[],[f1271,f681]) ).
fof(f1274,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(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(sF13,X3)))),c_Message_Oparts(sF20),tc_Message_Omsg))
| 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(sF13,X3))))),sF8,tc_Event_Oevent))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(forward_demodulation,[],[f1273,f718]) ).
fof(f1275,plain,
! [X2,X3,X0,X1] :
( 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(sF13,X3))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(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(sF13,X3)))),sF30,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Event_Obad,tc_Message_Oagent)) ),
inference(forward_demodulation,[],[f1274,f739]) ).
fof(f1278,plain,
! [X2,X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
inference(superposition,[],[f1275,f725]) ).
fof(f1279,plain,
! [X2,X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(superposition,[],[f1275,f697]) ).
fof(f1285,plain,
! [X2,X0,X1] :
( hBOOL(sF0)
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f1278,f672]) ).
fof(f1286,plain,
! [X2,X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg)) ),
inference(forward_subsumption_resolution,[],[f1285,f673]) ).
fof(f1288,plain,
! [X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,X1))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,X1)))),sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f1286,f729]) ).
fof(f1536,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ 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),sF14)))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Xa = X6 ),
inference(superposition,[],[f1035,f705]) ).
fof(f1538,definition,
( spl37_14
<=> ! [X5,X4,X6,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Xa = X6 ) ),
introduced(definition,[new_symbols(definition,[spl37_14])],[avatar_definition]) ).
fof(f1539,plain,
( ! [X3,X6,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Xa = X6 )
| ~ spl37_14 ),
inference(avatar_component_clause,[],[f1538]) ).
fof(f1541,definition,
( spl37_15
<=> ! [X2,X0,X1] : ~ 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),sF14)))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_15])],[avatar_definition]) ).
fof(f1542,plain,
( ! [X2,X0,X1] : ~ 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),sF14)))),sF8,tc_Event_Oevent))
| ~ spl37_15 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1543,plain,
( spl37_14
| spl37_15 ),
inference(avatar_split_clause,[],[f1536,f1541,f1538]) ).
fof(f1548,definition,
( spl37_17
<=> ! [X2,X0,X1] : ~ 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),sF26)))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_17])],[avatar_definition]) ).
fof(f1549,plain,
( ! [X2,X0,X1] : ~ 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),sF26)))),sF8,tc_Event_Oevent))
| ~ spl37_17 ),
inference(avatar_component_clause,[],[f1548]) ).
fof(f1554,plain,
! [X0] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,X0),sF21,tc_Message_Omsg))
| hBOOL(c_in(X0,sF21,tc_Message_Omsg))
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(superposition,[],[f826,f697]) ).
fof(f1723,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Aa = X3 ),
inference(superposition,[],[f1107,f697]) ).
fof(f1732,definition,
( spl37_20
<=> ! [X5,X4,X6,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Aa = X3 ) ),
introduced(definition,[new_symbols(definition,[spl37_20])],[avatar_definition]) ).
fof(f1733,plain,
( ! [X3,X6,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_Aa = X3 )
| ~ spl37_20 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1735,definition,
( spl37_21
<=> ! [X2,X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_21])],[avatar_definition]) ).
fof(f1736,plain,
( ! [X2,X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ spl37_21 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1737,plain,
( spl37_20
| spl37_21 ),
inference(avatar_split_clause,[],[f1723,f1735,f1732]) ).
fof(f1742,definition,
( spl37_23
<=> ! [X2,X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_23])],[avatar_definition]) ).
fof(f1743,plain,
( ! [X2,X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ spl37_23 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1817,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| v_A = v_Aa )
| ~ spl37_20 ),
inference(superposition,[],[f1733,f725]) ).
fof(f1932,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ 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(sF25,c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_B = X5 ),
inference(superposition,[],[f1070,f729]) ).
fof(f1943,definition,
( spl37_25
<=> ! [X5,X4,X6,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_B = X5 ) ),
introduced(definition,[new_symbols(definition,[spl37_25])],[avatar_definition]) ).
fof(f1944,plain,
( ! [X3,X6,X4,X5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(sF13,X6))))),sF8,tc_Event_Oevent))
| v_B = X5 )
| ~ spl37_25 ),
inference(avatar_component_clause,[],[f1943]) ).
fof(f1946,definition,
( spl37_26
<=> ! [X2,X0,X1] : ~ 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(sF25,c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_26])],[avatar_definition]) ).
fof(f1947,plain,
( ! [X2,X0,X1] : ~ 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(sF25,c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ spl37_26 ),
inference(avatar_component_clause,[],[f1946]) ).
fof(f1948,plain,
( spl37_25
| spl37_26 ),
inference(avatar_split_clause,[],[f1932,f1946,f1943]) ).
fof(f1969,plain,
( ! [X2,X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| spl37_4
| ~ spl37_20 ),
inference(forward_subsumption_resolution,[],[f1817,f775]) ).
fof(f1984,plain,
( spl37_23
| spl37_4
| ~ spl37_20 ),
inference(avatar_split_clause,[],[f1969,f1732,f773,f1742]) ).
fof(f2128,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(c_in(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(sF13,X3)))),sF30,tc_Message_Omsg))
| v_B = X0
| hBOOL(c_in(X1,c_Event_Obad,tc_Message_Oagent)) )
| ~ spl37_25 ),
inference(resolution,[],[f1944,f1275]) ).
fof(f2160,definition,
( spl37_27
<=> ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_27])],[avatar_definition]) ).
fof(f2161,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg))
| ~ spl37_27 ),
inference(avatar_component_clause,[],[f2160]) ).
fof(f2267,plain,
! [X0] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF26))),sF30,tc_Message_Omsg))
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))) ),
inference(superposition,[],[f1190,f729]) ).
fof(f2277,plain,
! [X0] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27)),sF30,tc_Message_Omsg))
| v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))) ),
inference(forward_demodulation,[],[f2267,f733]) ).
fof(f2279,definition,
( spl37_37
<=> v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))) ),
introduced(definition,[new_symbols(definition,[spl37_37])],[avatar_definition]) ).
fof(f2281,plain,
( v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A)))
| ~ spl37_37 ),
inference(avatar_component_clause,[],[f2279]) ).
fof(f2283,definition,
( spl37_38
<=> ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27)),sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_38])],[avatar_definition]) ).
fof(f2284,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27)),sF30,tc_Message_Omsg))
| ~ spl37_38 ),
inference(avatar_component_clause,[],[f2283]) ).
fof(f2285,plain,
( spl37_37
| spl37_38 ),
inference(avatar_split_clause,[],[f2277,f2283,f2279]) ).
fof(f2340,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF21,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oparts(sF20),tc_Message_Omsg)) ),
inference(superposition,[],[f618,f720]) ).
fof(f2341,plain,
! [X0] :
( ~ hBOOL(c_in(X0,sF21,tc_Message_Omsg))
| hBOOL(c_in(X0,sF30,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f2340,f739]) ).
fof(f2389,plain,
( ! [X0] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,X0),sF21,tc_Message_Omsg))
| hBOOL(c_in(X0,sF21,tc_Message_Omsg)) )
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f1554,f818]) ).
fof(f2506,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A)))))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))),sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f974,f725]) ).
fof(f2539,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,v_X))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))),sF30,tc_Message_Omsg))
| ~ spl37_37 ),
inference(forward_demodulation,[],[f2506,f2281]) ).
fof(f2541,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),c_Message_Omsg_OMPair(sF25,sF26)))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))),sF30,tc_Message_Omsg))
| ~ spl37_37 ),
inference(forward_demodulation,[],[f2539,f731]) ).
fof(f2543,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF27))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(sF13,c_Message_Omsg_OAgent(v_A))),sF30,tc_Message_Omsg))
| ~ spl37_37 ),
inference(forward_demodulation,[],[f2541,f733]) ).
fof(f2545,definition,
( spl37_51
<=> hBOOL(c_in(v_X,sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_51])],[avatar_definition]) ).
fof(f2546,plain,
( hBOOL(c_in(v_X,sF30,tc_Message_Omsg))
| ~ spl37_51 ),
inference(avatar_component_clause,[],[f2545]) ).
fof(f2547,plain,
( ~ hBOOL(c_in(v_X,sF30,tc_Message_Omsg))
| spl37_51 ),
inference(avatar_component_clause,[],[f2545]) ).
fof(f2549,definition,
( spl37_52
<=> hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF27))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_52])],[avatar_definition]) ).
fof(f2551,plain,
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF27))),sF8,tc_Event_Oevent))
| ~ spl37_52 ),
inference(avatar_component_clause,[],[f2549]) ).
fof(f2553,plain,
( ~ hBOOL(c_in(v_X,sF30,tc_Message_Omsg))
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF27))),sF8,tc_Event_Oevent))
| ~ spl37_37 ),
inference(forward_demodulation,[],[f2543,f2281]) ).
fof(f2554,plain,
( spl37_52
| ~ spl37_51
| ~ spl37_37 ),
inference(avatar_split_clause,[],[f2553,f2279,f2545,f2549]) ).
fof(f2563,plain,
( ~ hBOOL(c_in(sF17,sF21,tc_Message_Omsg))
| hBOOL(c_in(sF16,sF21,tc_Message_Omsg))
| ~ spl37_6 ),
inference(superposition,[],[f2389,f711]) ).
fof(f2565,definition,
( spl37_53
<=> hBOOL(c_in(sF16,sF21,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_53])],[avatar_definition]) ).
fof(f2567,plain,
( hBOOL(c_in(sF16,sF21,tc_Message_Omsg))
| ~ spl37_53 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2569,definition,
( spl37_54
<=> hBOOL(c_in(sF17,sF21,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_54])],[avatar_definition]) ).
fof(f2570,plain,
( hBOOL(c_in(sF17,sF21,tc_Message_Omsg))
| ~ spl37_54 ),
inference(avatar_component_clause,[],[f2569]) ).
fof(f2571,plain,
( ~ hBOOL(c_in(sF17,sF21,tc_Message_Omsg))
| spl37_54 ),
inference(avatar_component_clause,[],[f2569]) ).
fof(f2572,plain,
( spl37_53
| ~ spl37_54
| ~ spl37_6 ),
inference(avatar_split_clause,[],[f2563,f817,f2569,f2565]) ).
fof(f2613,definition,
( spl37_56
<=> ! [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(X3,sF27))),sF8,tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[spl37_56])],[avatar_definition]) ).
fof(f2614,plain,
( ! [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(X3,sF27))),sF8,tc_Event_Oevent))
| ~ spl37_56 ),
inference(avatar_component_clause,[],[f2613]) ).
fof(f2619,plain,
( c_Message_Omsg_OAgent(v_B) = sF12
| ~ spl37_5 ),
inference(superposition,[],[f701,f778]) ).
fof(f2620,plain,
( sF12 = sF25
| ~ spl37_5 ),
inference(forward_demodulation,[],[f2619,f729]) ).
fof(f2780,plain,
( ! [X0] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27))),sF8,tc_Event_Oevent))
| ~ spl37_56 ),
inference(superposition,[],[f2614,f725]) ).
fof(f2802,plain,
( ! [X2,X0,X1] :
( ~ 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),sF26)))),sF8,tc_Event_Oevent))
| v_Xa = v_X )
| ~ spl37_14 ),
inference(superposition,[],[f1539,f731]) ).
fof(f2812,definition,
( spl37_62
<=> v_Xa = v_X ),
introduced(definition,[new_symbols(definition,[spl37_62])],[avatar_definition]) ).
fof(f2814,plain,
( v_Xa = v_X
| ~ spl37_62 ),
inference(avatar_component_clause,[],[f2812]) ).
fof(f3327,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent))
| hBOOL(c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(superposition,[],[f579,f692]) ).
fof(f3328,plain,
! [X2,X0,X1] :
( hBOOL(c_in(X2,c_Message_Oanalz(sF20),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f3327,f718]) ).
fof(f3331,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent))
| hBOOL(c_in(X2,sF21,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f3328,f720]) ).
fof(f3538,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent))
| hBOOL(c_in(X2,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs5)),tc_Message_Omsg)) ),
inference(superposition,[],[f563,f692]) ).
fof(f3539,plain,
! [X2,X0,X1] :
( hBOOL(c_in(X2,c_Message_Oparts(sF20),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent)) ),
inference(forward_demodulation,[],[f3538,f718]) ).
fof(f3541,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X0,X1,X2),sF8,tc_Event_Oevent))
| hBOOL(c_in(X2,sF30,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f3539,f739]) ).
fof(f3730,plain,
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,sF28),sF30,tc_Message_Omsg))
| ~ spl37_38 ),
inference(superposition,[],[f2284,f735]) ).
fof(f3731,plain,
( ~ hBOOL(c_in(sF29,sF30,tc_Message_Omsg))
| ~ spl37_38 ),
inference(forward_demodulation,[],[f3730,f737]) ).
fof(f3732,plain,
( ~ hBOOL(sF31)
| ~ spl37_38 ),
inference(forward_demodulation,[],[f3731,f741]) ).
fof(f3733,plain,
( $false
| ~ spl37_1
| ~ spl37_38 ),
inference(forward_subsumption_resolution,[],[f3732,f761]) ).
fof(f3734,plain,
( ~ spl37_1
| ~ spl37_38 ),
inference(avatar_contradiction_clause,[],[f3733]) ).
fof(f3738,plain,
( c_Message_Omsg_OMPair(sF13,v_Xa) = sF26
| ~ spl37_62 ),
inference(superposition,[],[f731,f2814]) ).
fof(f3741,plain,
( sF14 = sF26
| ~ spl37_62 ),
inference(forward_demodulation,[],[f3738,f705]) ).
fof(f3745,plain,
( sF27 = c_Message_Omsg_OMPair(sF25,sF14)
| ~ spl37_62 ),
inference(superposition,[],[f733,f3741]) ).
fof(f3835,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| v_B = X1
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) )
| ~ spl37_25 ),
inference(superposition,[],[f2128,f697]) ).
fof(f3860,plain,
! [X0] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF26)))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF26))),sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f1288,f731]) ).
fof(f3862,plain,
! [X0] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF26))),sF30,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f3860,f733]) ).
fof(f3863,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF25,sF26))),sF30,tc_Message_Omsg))
| ~ spl37_56 ),
inference(forward_subsumption_resolution,[],[f3862,f2780]) ).
fof(f3864,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF27)),sF30,tc_Message_Omsg))
| ~ spl37_56 ),
inference(forward_demodulation,[],[f3863,f733]) ).
fof(f3865,plain,
( spl37_38
| ~ spl37_56 ),
inference(avatar_split_clause,[],[f3864,f2613,f2283]) ).
fof(f3888,plain,
( c_Message_Omsg_OMPair(sF12,sF14) = sF27
| ~ spl37_5
| ~ spl37_62 ),
inference(superposition,[],[f3745,f2620]) ).
fof(f3889,plain,
( sF15 = sF27
| ~ spl37_5
| ~ spl37_62 ),
inference(forward_demodulation,[],[f3888,f707]) ).
fof(f4037,plain,
( ! [X0,X1] : ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF14)))),sF8,tc_Event_Oevent))
| ~ spl37_15 ),
inference(superposition,[],[f1542,f697]) ).
fof(f4098,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_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),c_Message_Omsg_OMPair(sF25,c_Message_Omsg_OMPair(sF13,v_X))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(v_X,sF30,tc_Message_Omsg))
| ~ spl37_37 ),
inference(superposition,[],[f974,f2281]) ).
fof(f4200,plain,
( ! [X0,X1] : ~ 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(sF25,sF26)))),sF8,tc_Event_Oevent))
| ~ spl37_17 ),
inference(superposition,[],[f1549,f729]) ).
fof(f4203,plain,
( ! [X0,X1] : ~ 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,sF27))),sF8,tc_Event_Oevent))
| ~ spl37_17 ),
inference(forward_demodulation,[],[f4200,f733]) ).
fof(f4205,plain,
( spl37_56
| ~ spl37_17 ),
inference(avatar_split_clause,[],[f4203,f1548,f2613]) ).
fof(f4507,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),sF21,tc_Message_Omsg))
| hBOOL(c_in(X0,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f551,f720]) ).
fof(f4515,plain,
( ~ hBOOL(c_in(sF14,sF21,tc_Message_Omsg))
| hBOOL(c_in(sF13,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f4507,f705]) ).
fof(f4528,plain,
( hBOOL(sF22)
| ~ hBOOL(c_in(sF14,sF21,tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f4515,f722]) ).
fof(f4540,definition,
( spl37_96
<=> hBOOL(c_in(sF15,sF21,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_96])],[avatar_definition]) ).
fof(f4541,plain,
( hBOOL(c_in(sF15,sF21,tc_Message_Omsg))
| ~ spl37_96 ),
inference(avatar_component_clause,[],[f4540]) ).
fof(f4542,plain,
( ~ hBOOL(c_in(sF15,sF21,tc_Message_Omsg))
| spl37_96 ),
inference(avatar_component_clause,[],[f4540]) ).
fof(f4559,plain,
~ hBOOL(c_in(sF14,sF21,tc_Message_Omsg)),
inference(forward_subsumption_resolution,[],[f4528,f723]) ).
fof(f4574,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),sF21,tc_Message_Omsg))
| hBOOL(c_in(X1,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f550,f720]) ).
fof(f4577,plain,
( ~ hBOOL(c_in(sF16,sF21,tc_Message_Omsg))
| hBOOL(c_in(sF15,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f4574,f709]) ).
fof(f4578,plain,
( ~ hBOOL(c_in(sF15,sF21,tc_Message_Omsg))
| hBOOL(c_in(sF14,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f4574,f707]) ).
fof(f4849,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),sF30,tc_Message_Omsg))
| hBOOL(c_in(X1,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f552,f739]) ).
fof(f4855,plain,
( ~ hBOOL(c_in(sF26,sF30,tc_Message_Omsg))
| hBOOL(c_in(v_X,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f4849,f731]) ).
fof(f4857,plain,
( ~ hBOOL(c_in(sF28,sF30,tc_Message_Omsg))
| hBOOL(c_in(sF27,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f4849,f735]) ).
fof(f4858,plain,
( ~ hBOOL(c_in(sF27,sF30,tc_Message_Omsg))
| hBOOL(c_in(sF26,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f4849,f733]) ).
fof(f4860,definition,
( spl37_100
<=> hBOOL(c_in(sF26,sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_100])],[avatar_definition]) ).
fof(f4864,definition,
( spl37_101
<=> hBOOL(c_in(sF27,sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_101])],[avatar_definition]) ).
fof(f4867,plain,
( spl37_100
| ~ spl37_101 ),
inference(avatar_split_clause,[],[f4858,f4864,f4860]) ).
fof(f4869,definition,
( spl37_102
<=> hBOOL(c_in(sF28,sF30,tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[spl37_102])],[avatar_definition]) ).
fof(f4871,plain,
( ~ hBOOL(c_in(sF28,sF30,tc_Message_Omsg))
| spl37_102 ),
inference(avatar_component_clause,[],[f4869]) ).
fof(f4872,plain,
( spl37_101
| ~ spl37_102 ),
inference(avatar_split_clause,[],[f4857,f4869,f4864]) ).
fof(f4882,plain,
( ~ hBOOL(c_in(sF26,sF30,tc_Message_Omsg))
| spl37_51 ),
inference(forward_subsumption_resolution,[],[f4855,f2547]) ).
fof(f4899,plain,
( ~ spl37_100
| spl37_51 ),
inference(avatar_split_clause,[],[f4882,f2545,f4860]) ).
fof(f4958,plain,
! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X1),sF30,tc_Message_Omsg))
| hBOOL(c_in(X1,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f575,f739]) ).
fof(f4964,plain,
( ~ hBOOL(c_in(sF29,sF30,tc_Message_Omsg))
| hBOOL(c_in(sF28,sF30,tc_Message_Omsg)) ),
inference(superposition,[],[f4958,f737]) ).
fof(f4965,plain,
( ~ hBOOL(c_in(sF29,sF30,tc_Message_Omsg))
| spl37_102 ),
inference(forward_subsumption_resolution,[],[f4964,f4871]) ).
fof(f4968,plain,
( ~ hBOOL(sF31)
| spl37_102 ),
inference(forward_demodulation,[],[f4965,f741]) ).
fof(f4970,plain,
( $false
| ~ spl37_1
| spl37_102 ),
inference(forward_subsumption_resolution,[],[f4968,f761]) ).
fof(f4971,plain,
( ~ spl37_1
| spl37_102 ),
inference(avatar_contradiction_clause,[],[f4970]) ).
fof(f4975,plain,
( ~ hBOOL(c_in(v_X,sF30,tc_Message_Omsg))
| ~ spl37_26
| ~ spl37_37 ),
inference(forward_subsumption_resolution,[],[f4098,f1947]) ).
fof(f4986,plain,
( $false
| ~ spl37_26
| ~ spl37_37
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f4975,f2546]) ).
fof(f4987,plain,
( ~ spl37_26
| ~ spl37_37
| ~ spl37_51 ),
inference(avatar_contradiction_clause,[],[f4986]) ).
fof(f5442,plain,
( ~ hBOOL(c_in(sF18,sF8,tc_Event_Oevent))
| hBOOL(c_in(sF17,sF21,tc_Message_Omsg)) ),
inference(superposition,[],[f3331,f713]) ).
fof(f5443,plain,
( ~ hBOOL(c_in(sF18,sF8,tc_Event_Oevent))
| spl37_54 ),
inference(forward_subsumption_resolution,[],[f5442,f2571]) ).
fof(f5450,plain,
( ~ hBOOL(sF19)
| spl37_54 ),
inference(forward_demodulation,[],[f5443,f715]) ).
fof(f5456,plain,
( $false
| spl37_54 ),
inference(forward_subsumption_resolution,[],[f5450,f716]) ).
fof(f5457,plain,
spl37_54,
inference(avatar_contradiction_clause,[],[f5456]) ).
fof(f5466,plain,
( ! [X2,X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2))))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg)) )
| spl37_6 ),
inference(forward_subsumption_resolution,[],[f1279,f819]) ).
fof(f5475,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| v_B = X1 )
| spl37_6
| ~ spl37_25 ),
inference(forward_subsumption_resolution,[],[f3835,f819]) ).
fof(f5495,plain,
( ! [X2,X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(forward_subsumption_resolution,[],[f5466,f1736]) ).
fof(f5597,plain,
( ! [X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,c_Message_Omsg_OMPair(sF13,X1)))),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(superposition,[],[f5495,f701]) ).
fof(f5603,plain,
( ! [X0,X1] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,c_Message_Omsg_OMPair(sF13,X1)))),sF30,tc_Message_Omsg))
| v_B = v_Ba )
| spl37_6
| ~ spl37_25 ),
inference(superposition,[],[f5475,f701]) ).
fof(f5697,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,sF14))),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(superposition,[],[f5597,f705]) ).
fof(f5698,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(forward_demodulation,[],[f5697,f707]) ).
fof(f5762,plain,
( hBOOL(c_in(sF15,sF21,tc_Message_Omsg))
| ~ spl37_53 ),
inference(forward_subsumption_resolution,[],[f4577,f2567]) ).
fof(f5763,plain,
( $false
| ~ spl37_53
| spl37_96 ),
inference(forward_subsumption_resolution,[],[f5762,f4542]) ).
fof(f5764,plain,
( ~ spl37_53
| spl37_96 ),
inference(avatar_contradiction_clause,[],[f5763]) ).
fof(f5765,plain,
( hBOOL(c_in(sF14,sF21,tc_Message_Omsg))
| ~ spl37_96 ),
inference(forward_subsumption_resolution,[],[f4578,f4541]) ).
fof(f5766,plain,
( $false
| ~ spl37_96 ),
inference(forward_subsumption_resolution,[],[f5765,f4559]) ).
fof(f5767,plain,
~ spl37_96,
inference(avatar_contradiction_clause,[],[f5766]) ).
fof(f5849,plain,
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,sF16),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(superposition,[],[f5698,f709]) ).
fof(f5850,plain,
( ~ hBOOL(c_in(sF17,sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_21 ),
inference(forward_demodulation,[],[f5849,f711]) ).
fof(f5915,plain,
( hBOOL(c_in(sF17,sF30,tc_Message_Omsg))
| ~ spl37_54 ),
inference(resolution,[],[f2570,f2341]) ).
fof(f5921,plain,
( $false
| spl37_6
| ~ spl37_21
| ~ spl37_54 ),
inference(forward_subsumption_resolution,[],[f5915,f5850]) ).
fof(f5922,plain,
( spl37_6
| ~ spl37_21
| ~ spl37_54 ),
inference(avatar_contradiction_clause,[],[f5921]) ).
fof(f5943,plain,
( ! [X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,c_Message_Omsg_OMPair(sF13,X1)))),sF30,tc_Message_Omsg))
| spl37_5
| spl37_6
| ~ spl37_25 ),
inference(forward_subsumption_resolution,[],[f5603,f779]) ).
fof(f6183,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,sF14))),sF30,tc_Message_Omsg))
| spl37_5
| spl37_6
| ~ spl37_25 ),
inference(superposition,[],[f5943,f705]) ).
fof(f6184,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg))
| spl37_5
| spl37_6
| ~ spl37_25 ),
inference(forward_demodulation,[],[f6183,f707]) ).
fof(f6194,plain,
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,sF16),sF30,tc_Message_Omsg))
| spl37_5
| spl37_6
| ~ spl37_25 ),
inference(superposition,[],[f6184,f709]) ).
fof(f6195,plain,
( ~ hBOOL(c_in(sF17,sF30,tc_Message_Omsg))
| spl37_5
| spl37_6
| ~ spl37_25 ),
inference(forward_demodulation,[],[f6194,f711]) ).
fof(f6196,plain,
( $false
| spl37_5
| spl37_6
| ~ spl37_25
| ~ spl37_54 ),
inference(forward_subsumption_resolution,[],[f6195,f5915]) ).
fof(f6197,plain,
( spl37_5
| spl37_6
| ~ spl37_25
| ~ spl37_54 ),
inference(avatar_contradiction_clause,[],[f6196]) ).
fof(f6450,plain,
( ! [X0,X1] :
( hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF14)))),sF8,tc_Event_Oevent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF14))),sF30,tc_Message_Omsg)) )
| spl37_6 ),
inference(superposition,[],[f5466,f705]) ).
fof(f6451,plain,
( ! [X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF14))),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f6450,f4037]) ).
fof(f6456,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,sF14))),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_15 ),
inference(superposition,[],[f6451,f701]) ).
fof(f6457,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_15 ),
inference(forward_demodulation,[],[f6456,f707]) ).
fof(f6461,plain,
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF10,sF16),sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_15 ),
inference(superposition,[],[f6457,f709]) ).
fof(f6462,plain,
( ~ hBOOL(c_in(sF17,sF30,tc_Message_Omsg))
| spl37_6
| ~ spl37_15 ),
inference(forward_demodulation,[],[f6461,f711]) ).
fof(f6463,plain,
( $false
| spl37_6
| ~ spl37_15
| ~ spl37_54 ),
inference(forward_subsumption_resolution,[],[f6462,f5915]) ).
fof(f6464,plain,
( spl37_6
| ~ spl37_15
| ~ spl37_54 ),
inference(avatar_contradiction_clause,[],[f6463]) ).
fof(f6466,plain,
( spl37_62
| spl37_17
| ~ spl37_14 ),
inference(avatar_split_clause,[],[f2802,f1538,f1548,f2812]) ).
fof(f6554,plain,
( ! [X2,X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(sF13,X2)))),sF30,tc_Message_Omsg))
| ~ spl37_23 ),
inference(resolution,[],[f1743,f1286]) ).
fof(f6566,plain,
( ! [X0,X1] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),sF14))),sF30,tc_Message_Omsg))
| ~ spl37_23 ),
inference(superposition,[],[f6554,f705]) ).
fof(f6571,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(sF12,sF14))),sF30,tc_Message_Omsg))
| ~ spl37_23 ),
inference(superposition,[],[f6566,f701]) ).
fof(f6572,plain,
( ! [X0] : ~ hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(X0,sF15)),sF30,tc_Message_Omsg))
| ~ spl37_23 ),
inference(forward_demodulation,[],[f6571,f707]) ).
fof(f7251,plain,
( hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF27)),sF30,tc_Message_Omsg))
| ~ spl37_52 ),
inference(resolution,[],[f3541,f2551]) ).
fof(f7259,plain,
( hBOOL(c_in(c_Message_Omsg_OCrypt(sF23,c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(v_A,v_B,v_K,v_evs5),sF15)),sF30,tc_Message_Omsg))
| ~ spl37_5
| ~ spl37_52
| ~ spl37_62 ),
inference(forward_demodulation,[],[f7251,f3889]) ).
fof(f7269,plain,
( $false
| ~ spl37_5
| ~ spl37_27
| ~ spl37_52
| ~ spl37_62 ),
inference(forward_subsumption_resolution,[],[f7259,f2161]) ).
fof(f7270,plain,
( ~ spl37_5
| ~ spl37_27
| ~ spl37_52
| ~ spl37_62 ),
inference(avatar_contradiction_clause,[],[f7269]) ).
fof(f7276,plain,
( spl37_27
| ~ spl37_23 ),
inference(avatar_split_clause,[],[f6572,f1742,f2160]) ).
cnf(s2,plain,
( ~ spl37_4
| ~ spl37_5 ),
inference(sat_conversion,[],[f780]) ).
cnf(s4,plain,
spl37_1,
inference(sat_conversion,[],[f782]) ).
cnf(s10,plain,
( spl37_14
| spl37_15 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s13,plain,
( spl37_20
| spl37_21 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s18,plain,
( spl37_25
| spl37_26 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s22,plain,
( spl37_4
| ~ spl37_20
| spl37_23 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s36,plain,
( spl37_37
| spl37_38 ),
inference(sat_conversion,[],[f2285]) ).
cnf(s44,plain,
( ~ spl37_37
| ~ spl37_51
| spl37_52 ),
inference(sat_conversion,[],[f2554]) ).
cnf(s45,plain,
( ~ spl37_6
| spl37_53
| ~ spl37_54 ),
inference(sat_conversion,[],[f2572]) ).
cnf(s74,plain,
( ~ spl37_1
| ~ spl37_38 ),
inference(sat_conversion,[],[f3734]) ).
cnf(s76,plain,
( spl37_38
| ~ spl37_56 ),
inference(sat_conversion,[],[f3865]) ).
cnf(s86,plain,
( ~ spl37_17
| spl37_56 ),
inference(sat_conversion,[],[f4205]) ).
cnf(s96,plain,
( spl37_100
| ~ spl37_101 ),
inference(sat_conversion,[],[f4867]) ).
cnf(s97,plain,
( spl37_101
| ~ spl37_102 ),
inference(sat_conversion,[],[f4872]) ).
cnf(s103,plain,
( spl37_51
| ~ spl37_100 ),
inference(sat_conversion,[],[f4899]) ).
cnf(s104,plain,
( ~ spl37_1
| spl37_102 ),
inference(sat_conversion,[],[f4971]) ).
cnf(s110,plain,
( ~ spl37_26
| ~ spl37_37
| ~ spl37_51 ),
inference(sat_conversion,[],[f4987]) ).
cnf(s119,plain,
spl37_54,
inference(sat_conversion,[],[f5457]) ).
cnf(s129,plain,
( ~ spl37_53
| spl37_96 ),
inference(sat_conversion,[],[f5764]) ).
cnf(s130,plain,
~ spl37_96,
inference(sat_conversion,[],[f5767]) ).
cnf(s139,plain,
( spl37_6
| ~ spl37_21
| ~ spl37_54 ),
inference(sat_conversion,[],[f5922]) ).
cnf(s143,plain,
( spl37_5
| spl37_6
| ~ spl37_25
| ~ spl37_54 ),
inference(sat_conversion,[],[f6197]) ).
cnf(s152,plain,
( spl37_6
| ~ spl37_15
| ~ spl37_54 ),
inference(sat_conversion,[],[f6464]) ).
cnf(s153,plain,
( ~ spl37_14
| spl37_17
| spl37_62 ),
inference(sat_conversion,[],[f6466]) ).
cnf(s162,plain,
( ~ spl37_5
| ~ spl37_27
| ~ spl37_52
| ~ spl37_62 ),
inference(sat_conversion,[],[f7270]) ).
cnf(s163,plain,
( ~ spl37_23
| spl37_27 ),
inference(sat_conversion,[],[f7276]) ).
cnf(s166,plain,
~ spl37_53,
inference(rat,[],[s129,s130]) ).
cnf(s174,plain,
~ spl37_6,
inference(rat,[],[s45,s119,s166]) ).
cnf(s175,plain,
~ spl37_15,
inference(rat,[],[s152,s119,s174]) ).
cnf(s176,plain,
~ spl37_21,
inference(rat,[],[s139,s119,s174]) ).
cnf(s181,plain,
spl37_20,
inference(rat,[],[s13,s176]) ).
cnf(s182,plain,
spl37_14,
inference(rat,[],[s10,s175]) ).
cnf(s183,plain,
spl37_102,
inference(rat,[],[s104,s4]) ).
cnf(s184,plain,
~ spl37_38,
inference(rat,[],[s74,s4]) ).
cnf(s186,plain,
spl37_101,
inference(rat,[],[s97,s183]) ).
cnf(s187,plain,
~ spl37_56,
inference(rat,[],[s76,s184]) ).
cnf(s188,plain,
spl37_37,
inference(rat,[],[s36,s184]) ).
cnf(s190,plain,
spl37_100,
inference(rat,[],[s96,s186]) ).
cnf(s191,plain,
~ spl37_17,
inference(rat,[],[s86,s187]) ).
cnf(s193,plain,
spl37_51,
inference(rat,[],[s103,s190]) ).
cnf(s194,plain,
spl37_62,
inference(rat,[],[s153,s182,s191]) ).
cnf(s198,plain,
spl37_52,
inference(rat,[],[s44,s188,s193]) ).
cnf(s199,plain,
~ spl37_26,
inference(rat,[],[s110,s188,s193]) ).
cnf(s202,plain,
spl37_25,
inference(rat,[],[s18,s199]) ).
cnf(s203,plain,
spl37_5,
inference(rat,[],[s143,s119,s174,s202]) ).
cnf(s204,plain,
~ spl37_27,
inference(rat,[],[s162,s194,s198,s203]) ).
cnf(s209,plain,
~ spl37_23,
inference(rat,[],[s163,s204]) ).
cnf(s215,plain,
spl37_4,
inference(rat,[],[s22,s181,s209]) ).
cnf(s219,plain,
$false,
inference(rat,[],[s2,s203,s215]) ).
fof(f7278,plain,
$false,
inference(avatar_sat_refutation,[],[s219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV803-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n017.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 12:30:51 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.72/2.61 % (3511238)Input is clausal, will run a generic CNF schedule.
% 6.72/2.61 % (3511331)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3157871757:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.72/2.61 % (3511333)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=46921278:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.72/2.61 % (3511341)dis-21_1_sil=8000:lcm=predicate:random_seed=3382596537:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.72/2.61 % (3511335)lrs+10_1_sil=8000:sp=occurrence:random_seed=3152802816:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.72/2.61 % (3511340)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1841510004:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.72/2.61 % (3511336)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=633058958:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.72/2.61 % (3511329)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2910035533:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.72/2.61 % (3511341)Instruction limit reached!
% 6.72/2.61 % (3511341)------------------------------
% 6.72/2.61 % (3511341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511341)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511341)Termination reason: Instruction limit
% 6.72/2.61 % (3511341)Termination phase: Saturation
% 6.72/2.61 % (3511341)Time elapsed: 0.060 s
% 6.72/2.61 % (3511341)Peak memory usage: 89 MB
% 6.72/2.61 % (3511341)Instructions burned: 119 (million)
% 6.72/2.61 % (3511335)Instruction limit reached!
% 6.72/2.61 % (3511335)------------------------------
% 6.72/2.61 % (3511335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511335)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511335)Termination reason: Instruction limit
% 6.72/2.61 % (3511335)Termination phase: Saturation
% 6.72/2.61 % (3511335)Time elapsed: 0.071 s
% 6.72/2.61 % (3511335)Peak memory usage: 89 MB
% 6.72/2.61 % (3511335)Instructions burned: 107 (million)
% 6.72/2.61 % (3511336)Instruction limit reached!
% 6.72/2.61 % (3511336)------------------------------
% 6.72/2.61 % (3511336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511336)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511336)Termination reason: Instruction limit
% 6.72/2.61 % (3511336)Termination phase: Saturation
% 6.72/2.61 % (3511336)Time elapsed: 0.075 s
% 6.72/2.61 % (3511336)Peak memory usage: 90 MB
% 6.72/2.61 % (3511336)Instructions burned: 115 (million)
% 6.72/2.61 % (3511340)Instruction limit reached!
% 6.72/2.61 % (3511340)------------------------------
% 6.72/2.61 % (3511340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511340)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511340)Termination reason: Instruction limit
% 6.72/2.61 % (3511340)Termination phase: Saturation
% 6.72/2.61 % (3511340)Time elapsed: 0.114 s
% 6.72/2.61 % (3511340)Peak memory usage: 90 MB
% 6.72/2.61 % (3511340)Instructions burned: 180 (million)
% 6.72/2.61 % (3511387)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2704030576:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.72/2.61 % (3511388)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4088125266:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.72/2.61 % (3511389)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1747721991:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.72/2.61 % (3511390)lrs+10_64_to=lpo:sil=8000:random_seed=1658655215:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.72/2.61 % (3511387)Instruction limit reached!
% 6.72/2.61 % (3511387)------------------------------
% 6.72/2.61 % (3511387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511387)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511387)Termination reason: Instruction limit
% 6.72/2.61 % (3511387)Termination phase: Saturation
% 6.72/2.61 % (3511387)Time elapsed: 0.089 s
% 6.72/2.61 % (3511387)Peak memory usage: 90 MB
% 6.72/2.61 % (3511387)Instructions burned: 143 (million)
% 6.72/2.61 % (3511388)Instruction limit reached!
% 6.72/2.61 % (3511388)------------------------------
% 6.72/2.61 % (3511388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511388)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511388)Termination reason: Instruction limit
% 6.72/2.61 % (3511388)Termination phase: Saturation
% 6.72/2.61 % (3511388)Time elapsed: 0.103 s
% 6.72/2.61 % (3511388)Peak memory usage: 91 MB
% 6.72/2.61 % (3511388)Instructions burned: 191 (million)
% 6.72/2.61 % (3511389)Instruction limit reached!
% 6.72/2.61 % (3511389)------------------------------
% 6.72/2.61 % (3511389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511389)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511389)Termination reason: Instruction limit
% 6.72/2.61 % (3511389)Termination phase: Saturation
% 6.72/2.61 % (3511389)Time elapsed: 0.126 s
% 6.72/2.61 % (3511389)Peak memory usage: 91 MB
% 6.72/2.61 % (3511389)Instructions burned: 219 (million)
% 6.72/2.61 % (3511390)Instruction limit reached!
% 6.72/2.61 % (3511390)------------------------------
% 6.72/2.61 % (3511390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511390)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511390)Termination reason: Instruction limit
% 6.72/2.61 % (3511390)Termination phase: Saturation
% 6.72/2.61 % (3511390)Time elapsed: 0.079 s
% 6.72/2.61 % (3511390)Peak memory usage: 90 MB
% 6.72/2.61 % (3511390)Instructions burned: 126 (million)
% 6.72/2.61 % (3511395)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3354041937:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.72/2.61 % (3511396)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=429876425:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.72/2.61 % (3511398)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=762599951:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 6.72/2.61 % (3511397)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=360699658:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 6.72/2.61 % (3511398)Instruction limit reached!
% 6.72/2.61 % (3511398)------------------------------
% 6.72/2.61 % (3511398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511398)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511398)Termination reason: Instruction limit
% 6.72/2.61 % (3511398)Termination phase: Saturation
% 6.72/2.61 % (3511398)Time elapsed: 0.059 s
% 6.72/2.61 % (3511398)Peak memory usage: 89 MB
% 6.72/2.61 % (3511398)Instructions burned: 106 (million)
% 6.72/2.61 % (3511395)Instruction limit reached!
% 6.72/2.61 % (3511395)------------------------------
% 6.72/2.61 % (3511395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511395)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511395)Termination reason: Instruction limit
% 6.72/2.61 % (3511395)Termination phase: Saturation
% 6.72/2.61 % (3511395)Time elapsed: 0.129 s
% 6.72/2.61 % (3511395)Peak memory usage: 90 MB
% 6.72/2.61 % (3511395)Instructions burned: 194 (million)
% 6.72/2.61 % (3511396)Instruction limit reached!
% 6.72/2.61 % (3511396)------------------------------
% 6.72/2.61 % (3511396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511396)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511396)Termination reason: Instruction limit
% 6.72/2.61 % (3511396)Termination phase: Saturation
% 6.72/2.61 % (3511396)Time elapsed: 0.103 s
% 6.72/2.61 % (3511396)Peak memory usage: 91 MB
% 6.72/2.61 % (3511396)Instructions burned: 158 (million)
% 6.72/2.61 % (3511404)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=806948915:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 6.72/2.61 % (3511403)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2702728422:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.72/2.61 % (3511405)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3291001911:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 6.72/2.61 % (3511403)Instruction limit reached!
% 6.72/2.61 % (3511403)------------------------------
% 6.72/2.61 % (3511403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511403)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511403)Termination reason: Instruction limit
% 6.72/2.61 % (3511403)Termination phase: Saturation
% 6.72/2.61 % (3511403)Time elapsed: 0.069 s
% 6.72/2.61 % (3511403)Peak memory usage: 90 MB
% 6.72/2.61 % (3511403)Instructions burned: 108 (million)
% 6.72/2.61 % (3511404)Instruction limit reached!
% 6.72/2.61 % (3511404)------------------------------
% 6.72/2.61 % (3511404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511404)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511404)Termination reason: Instruction limit
% 6.72/2.61 % (3511404)Termination phase: Saturation
% 6.72/2.61 % (3511404)Time elapsed: 0.222 s
% 6.72/2.61 % (3511404)Peak memory usage: 90 MB
% 6.72/2.61 % (3511404)Instructions burned: 243 (million)
% 6.72/2.61 % (3511417)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2844395888:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 6.72/2.61 % (3511417)Instruction limit reached!
% 6.72/2.61 % (3511417)------------------------------
% 6.72/2.61 % (3511417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511417)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511417)Termination reason: Instruction limit
% 6.72/2.61 % (3511417)Termination phase: Saturation
% 6.72/2.61 % (3511417)Time elapsed: 0.112 s
% 6.72/2.61 % (3511417)Peak memory usage: 89 MB
% 6.72/2.61 % (3511417)Instructions burned: 135 (million)
% 6.72/2.61 % (3511424)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=791201614:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 6.72/2.61 % (3511433)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2719908456:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 6.72/2.61 % (3511329)First to succeed.
% 6.72/2.61 % (3511329)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3511238"
% 6.72/2.61 % (3511433)Instruction limit reached!
% 6.72/2.61 % (3511433)------------------------------
% 6.72/2.61 % (3511433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/2.61 % (3511433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/2.61 % (3511433)CaDiCaL version: 2.1.3
% 6.72/2.61 % (3511433)Termination reason: Instruction limit
% 6.72/2.61 % (3511433)Termination phase: Saturation
% 6.72/2.61 % (3511433)Time elapsed: 0.168 s
% 6.72/2.61 % (3511433)Peak memory usage: 91 MB
% 6.72/2.61 % (3511433)Instructions burned: 192 (million)
% 6.72/2.61 % (3511329)Refutation found. Thanks to Tanya!
% 6.72/2.61 % SZS status Unsatisfiable for theBenchmark
% 6.72/2.61 % SZS output start Proof for theBenchmark
% See solution above
% 14.08/2.84 % (3511329)------------------------------
% 14.08/2.84 % (3511329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/2.84 % (3511329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.08/2.84 % (3511329)CaDiCaL version: 2.1.3
% 14.08/2.84 % (3511329)Termination reason: Refutation
% 14.08/2.84 % (3511329)Time elapsed: 1.513 s
% 14.08/2.84 % (3511329)Peak memory usage: 146 MB
% 14.08/2.84 % (3511329)Instructions burned: 2977 (million)
% 14.08/2.84 % (3511329)------------------------------
% 14.08/2.84 % (3511329)------------------------------
% 14.08/2.84 % (3511238)Success in time 1.941 s
% 14.08/2.84 % Vampire exiting
%------------------------------------------------------------------------------