%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV731-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:49:25 PM UTC 2026
% Result : Unsatisfiable 141.98s 18.58s
% Output : CNFRefutation 124.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 74
% Syntax : Number of formulae : 254 ( 109 unt; 36 def)
% Number of atoms : 415 ( 38 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 282 ( 121 ~; 125 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 47 ( 45 usr; 37 prp; 0-4 aty)
% Number of functors : 41 ( 41 usr; 21 con; 0-4 aty)
% Number of variables : 167 ( 167 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [T_a] : c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
c_Event_OinitState(c_Message_Oagent_OSpy) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [T_a,V_c,V_A,V_B] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A))
| hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [V_f,V_A,T_b,T_a,V_B] : c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(V_f,V_A,T_b,T_a),c_Set_Oimage(V_f,V_B,T_b,T_a),tc_fun(T_a,tc_bool)) = c_Set_Oimage(V_f,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_b,tc_bool)),T_b,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,axiom,
! [V_H] : c_lessequals(V_H,c_Message_Oparts(V_H),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [V_xs,T_a] : c_Finite__Set_Ofinite(c_List_Oset(V_xs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,axiom,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f386,axiom,
! [V_X,V_B,V_K,V_A,V_evs,V_K_H,V_N] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X)))))),c_List_Oset(V_evs,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f421,axiom,
! [V_X,V_H] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),V_X),V_H))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),V_X),c_Message_Oanalz(V_H))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f515,axiom,
! [V_N] : c_Message_Oparts(c_Set_Oimage(c_Message_Omsg_OKey,V_N,tc_nat,tc_Message_Omsg)) = c_Set_Oimage(c_Message_Omsg_OKey,V_N,tc_nat,tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f526,axiom,
! [V_X] : hBOOL(hAPP(hAPP(c_in(tc_nat),hAPP(c_Public_OshrK,V_X)),c_Message_OsymKeys)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f529,axiom,
hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),c_List_Olist_ONil(tc_Event_Oevent)),c_NS__Shared__Mirabelle_Ons__shared)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f530,axiom,
c_Fun_Oinj__on(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f532,axiom,
! [V_K,V_evs,V_A,V_K_H,V_N,V_B,V_X] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X)))))),c_List_Oset(V_evs,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared))
| ~ hBOOL(hAPP(hAPP(c_in(tc_nat),V_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f553,axiom,
! [V_A,V_NA,V_B,V_K,V_X,V_evs] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs))))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),V_A),c_Event_Obad))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared))
| hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),c_Message_Omsg_OMPair(V_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X)))))),c_List_Oset(V_evs,tc_Event_Oevent))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f565,axiom,
! [V_X,V_H] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),V_X),V_H))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),V_X),c_Message_Oparts(V_H))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f566,axiom,
hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OSpy),c_Event_Obad)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f584,axiom,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f585,axiom,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f602,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f603,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f604,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f605,negated_conjecture,
( hBOOL(hAPP(hAPP(c_in(tc_nat),v_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat)))
| v_X != c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f607,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f610,axiom,
! [T_2,T_1] :
( ~ class_Orderings_Opreorder(T_1)
| class_Orderings_Opreorder(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f612,axiom,
! [T_2,T_1] :
( ~ class_Orderings_Oorder(T_1)
| class_Orderings_Oorder(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f616,axiom,
class_Lattices_Oupper__semilattice(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f617,axiom,
class_Orderings_Opreorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f620,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f622,axiom,
class_HOL_Oord(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f624,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f627,axiom,
class_Orderings_Opreorder(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f628,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f629,axiom,
class_Orderings_Oorder(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f632,axiom,
class_HOL_Oord(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f640,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) = c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f688,plain,
! [X0,X1] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f698,plain,
! [X0] : c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f765,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f835,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A))
| ! [V_B] : hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)))) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f836,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| hBOOL(hAPP(hAPP(c_in(X0),X1),c_Lattices_Oupper__semilattice__class_Osup(X2,X3,tc_fun(X0,tc_bool)))) ),
inference(cnf_transformation,[status(thm)],[f835]) ).
fof(f839,plain,
! [X0,X1] : ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f860,plain,
! [X0,X1,X2,X3,X4] : c_Set_Oimage(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(X0,X1,X3,X4),c_Set_Oimage(X0,X2,X3,X4),tc_fun(X4,tc_bool)),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f868,plain,
! [X0] : c_lessequals(X0,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f917,plain,
! [X0,X1] : c_Finite__Set_Ofinite(c_List_Oset(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f969,plain,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f1188,plain,
! [V_X,V_B,V_K,V_A,V_evs] :
( ! [V_K_H,V_N] : ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X)))))),c_List_Oset(V_evs,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
inference(miniscoping,[status(thm)],[f386]) ).
fof(f1189,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,X2,c_Message_Omsg_OCrypt(X5,c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),X3)))))),c_List_Oset(X4,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),X4),c_NS__Shared__Mirabelle_Ons__shared))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),c_Message_Omsg_OAgent(X2))) = X3 ),
inference(cnf_transformation,[status(thm)],[f1188]) ).
fof(f1239,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),X0),X1))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),X0),c_Message_Oanalz(X1))) ),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f1366,plain,
! [X0] : c_Message_Oparts(c_Set_Oimage(c_Message_Omsg_OKey,X0,tc_nat,tc_Message_Omsg)) = c_Set_Oimage(c_Message_Omsg_OKey,X0,tc_nat,tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f515]) ).
fof(f1379,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(tc_nat),hAPP(c_Public_OshrK,X0)),c_Message_OsymKeys)),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f1384,plain,
hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),c_List_Olist_ONil(tc_Event_Oevent)),c_NS__Shared__Mirabelle_Ons__shared)),
inference(cnf_transformation,[status(thm)],[f529]) ).
fof(f1385,plain,
c_Fun_Oinj__on(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),
inference(cnf_transformation,[status(thm)],[f530]) ).
fof(f1387,plain,
! [V_K,V_evs] :
( ! [V_A,V_K_H,V_N,V_B,V_X] : ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OCrypt(V_K_H,c_Message_Omsg_OMPair(V_N,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),V_X)))))),c_List_Oset(V_evs,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared))
| ~ hBOOL(hAPP(hAPP(c_in(tc_nat),V_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat))) ),
inference(miniscoping,[status(thm)],[f532]) ).
fof(f1388,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),X6),c_NS__Shared__Mirabelle_Ons__shared))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(X2,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X0),X5)))))),c_List_Oset(X6,tc_Event_Oevent)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_nat),X0),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat))) ),
inference(cnf_transformation,[status(thm)],[f1387]) ).
fof(f1417,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),X5),c_NS__Shared__Mirabelle_Ons__shared))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),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))))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),X0),c_Event_Obad))
| hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),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))) ),
inference(cnf_transformation,[status(thm)],[f553]) ).
fof(f1434,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),X0),c_Message_Oparts(X1)))
| ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f1435,plain,
hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OSpy),c_Event_Obad)),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f1457,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(miniscoping,[status(thm)],[f584]) ).
fof(f1458,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1457]) ).
fof(f1459,plain,
! [V_S,V_x] :
( ! [T_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f585]) ).
fof(f1460,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X2,X1))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f1459]) ).
fof(f1485,plain,
hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)))),
inference(cnf_transformation,[status(thm)],[f602]) ).
fof(f1486,plain,
~ hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)),
inference(cnf_transformation,[status(thm)],[f603]) ).
fof(f1487,plain,
hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)),
inference(cnf_transformation,[status(thm)],[f604]) ).
fof(f1488,plain,
( hBOOL(hAPP(hAPP(c_in(tc_nat),v_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat)))
| v_X != c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))) ),
inference(cnf_transformation,[status(thm)],[f605]) ).
fof(f1491,plain,
! [T_1] :
( ~ class_Lattices_Olattice(T_1)
| ! [T_2] : class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f607]) ).
fof(f1492,plain,
! [X0,X1] :
( ~ class_Lattices_Olattice(X1)
| class_Lattices_Oupper__semilattice(tc_fun(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1491]) ).
fof(f1497,plain,
! [T_1] :
( ~ class_Orderings_Opreorder(T_1)
| ! [T_2] : class_Orderings_Opreorder(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f610]) ).
fof(f1498,plain,
! [X0,X1] :
( class_Orderings_Opreorder(tc_fun(X1,X0))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1497]) ).
fof(f1501,plain,
! [T_1] :
( ~ class_Orderings_Oorder(T_1)
| ! [T_2] : class_Orderings_Oorder(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f612]) ).
fof(f1502,plain,
! [X0,X1] :
( class_Orderings_Oorder(tc_fun(X1,X0))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1501]) ).
fof(f1509,plain,
class_Lattices_Oupper__semilattice(tc_nat),
inference(cnf_transformation,[status(thm)],[f616]) ).
fof(f1510,plain,
class_Orderings_Opreorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f617]) ).
fof(f1513,plain,
class_Orderings_Oorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f1515,plain,
class_HOL_Oord(tc_nat),
inference(cnf_transformation,[status(thm)],[f622]) ).
fof(f1517,plain,
class_Lattices_Oupper__semilattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f1520,plain,
class_Orderings_Opreorder(tc_bool),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f1521,plain,
class_Lattices_Olattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f628]) ).
fof(f1522,plain,
class_Orderings_Oorder(tc_bool),
inference(cnf_transformation,[status(thm)],[f629]) ).
fof(f1525,plain,
class_HOL_Oord(tc_bool),
inference(cnf_transformation,[status(thm)],[f632]) ).
fof(f1529,definition,
( sQ0_spl
<=> v_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1532,definition,
( sQ1_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_nat),v_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1535,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1488,f1529,f1532]) ).
fof(f1548,definition,
( sQ3_spl
<=> class_Orderings_Oorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1550,plain,
( sQ3_spl
| ~ class_Orderings_Oorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f1548]) ).
fof(f1593,plain,
( ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))
| hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad))
| hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))),c_List_Oset(v_evs,tc_Event_Oevent))) ),
inference(resolution,[status(thm)],[f1417,f1485]) ).
fof(f1594,definition,
( sQ5_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))),c_List_Oset(v_evs,tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1595,plain,
( ~ sQ5_spl
| hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))),c_List_Oset(v_evs,tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f1594]) ).
fof(f1597,definition,
( sQ6_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1598,plain,
( ~ sQ6_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)) ),
inference(component_clause,[status(thm)],[f1597]) ).
fof(f1600,definition,
( sQ7_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1602,plain,
( sQ7_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)) ),
inference(component_clause,[status(thm)],[f1600]) ).
fof(f1603,plain,
( ~ sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1593,f1594,f1597,f1600]) ).
fof(f1604,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1602,f1487]) ).
fof(f1605,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1604]) ).
fof(f1656,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1598,f1486]) ).
fof(f1657,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1656]) ).
fof(f1662,definition,
( sQ10_spl
<=> class_Lattices_Oupper__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1664,plain,
( sQ10_spl
| ~ class_Lattices_Oupper__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f1662]) ).
fof(f1981,plain,
! [X0] : hBOOL(hAPP(c_Message_OsymKeys,hAPP(c_Public_OshrK,X0))),
inference(resolution,[status(thm)],[f1460,f1379]) ).
fof(f1983,plain,
hBOOL(hAPP(c_Event_Obad,c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f1460,f1435]) ).
fof(f1997,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,c_List_Olist_ONil(tc_Event_Oevent))),
inference(resolution,[status(thm)],[f1460,f1384]) ).
fof(f1998,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs)),
inference(resolution,[status(thm)],[f1460,f1487]) ).
fof(f2018,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(X0),c_Message_Oagent_OSpy),c_Event_Obad)),
inference(resolution,[status(thm)],[f1983,f1458]) ).
fof(f2019,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(X0),v_evs),c_NS__Shared__Mirabelle_Ons__shared)),
inference(resolution,[status(thm)],[f1998,f1458]) ).
fof(f2038,definition,
( sQ23_spl
<=> class_Lattices_Oupper__semilattice(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f2040,plain,
( sQ23_spl
| ~ class_Lattices_Oupper__semilattice(tc_nat) ),
inference(component_clause,[status(thm)],[f2038]) ).
fof(f2048,definition,
( sQ26_spl
<=> class_Orderings_Oorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f2050,plain,
( sQ26_spl
| ~ class_Orderings_Oorder(tc_nat) ),
inference(component_clause,[status(thm)],[f2048]) ).
fof(f2052,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2040,f1509]) ).
fof(f2053,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f2052]) ).
fof(f2064,definition,
( sQ28_spl
<=> class_Orderings_Oorder(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f2066,plain,
( sQ28_spl
| ~ class_Orderings_Oorder(tc_bool) ),
inference(component_clause,[status(thm)],[f2064]) ).
fof(f2068,definition,
( sQ29_spl
<=> class_Lattices_Oupper__semilattice(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f2070,plain,
( sQ29_spl
| ~ class_Lattices_Oupper__semilattice(tc_bool) ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2075,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2070,f1517]) ).
fof(f2076,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f2075]) ).
fof(f2203,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(X0),c_List_Olist_ONil(tc_Event_Oevent)),c_NS__Shared__Mirabelle_Ons__shared)),
inference(resolution,[status(thm)],[f1997,f1458]) ).
fof(f2204,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_in(X0),hAPP(c_Public_OshrK,X1)),c_Message_OsymKeys)),
inference(resolution,[status(thm)],[f1981,f1458]) ).
fof(f2267,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(forward_demodulation,[status(thm)],[f860,f765]) ).
fof(f2268,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(forward_demodulation,[status(thm)],[f860,f2267]) ).
fof(f2269,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(forward_demodulation,[status(thm)],[f860,f2268]) ).
fof(f2270,plain,
c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),c_Set_Oimage(c_Message_OinvKey,c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(forward_demodulation,[status(thm)],[f860,f2269]) ).
fof(f2271,plain,
c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_nat),c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg) = c_Event_OinitState(c_Message_Oagent_OSpy),
inference(forward_demodulation,[status(thm)],[f860,f2270]) ).
fof(f2276,plain,
c_Message_Oparts(c_Event_OinitState(c_Message_Oagent_OSpy)) = c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_OinvKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Event_Obad,tc_Message_Oagent,tc_nat),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_nat),c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OEncryption),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),c_Set_Oimage(c_Public_OpublicKey(c_Public_Okeymode_OSignature),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),
inference(paramodulation,[status(thm)],[f2271,f1366]) ).
fof(f2289,plain,
c_Event_OinitState(c_Message_Oagent_OSpy) = c_Message_Oparts(c_Event_OinitState(c_Message_Oagent_OSpy)),
inference(forward_demodulation,[status(thm)],[f2271,f2276]) ).
fof(f2307,plain,
c_lessequals(c_Event_OinitState(c_Message_Oagent_OSpy),c_Event_OinitState(c_Message_Oagent_OSpy),tc_fun(tc_Message_Omsg,tc_bool)),
inference(paramodulation,[status(thm)],[f2289,f868]) ).
fof(f2351,definition,
! [X0,X1] :
( sQ40_spl
<=> ~ c_Finite__Set_Ofinite(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2352,plain,
! [X0,X1] :
( ~ sQ40_spl
| ~ c_Finite__Set_Ofinite(X0,X1) ),
inference(component_clause,[status(thm)],[f2351]) ).
fof(f2430,plain,
( ~ sQ40_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f917,f2352]) ).
fof(f2432,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f2430]) ).
fof(f2571,definition,
( sQ49_spl
<=> c_lessequals(c_Event_OinitState(c_Message_Oagent_OSpy),c_Event_OinitState(c_Message_Oagent_OSpy),tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f2573,plain,
( sQ49_spl
| ~ c_lessequals(c_Event_OinitState(c_Message_Oagent_OSpy),c_Event_OinitState(c_Message_Oagent_OSpy),tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f2571]) ).
fof(f2616,plain,
! [X0] : class_Orderings_Oorder(tc_fun(X0,tc_bool)),
inference(resolution,[status(thm)],[f1502,f1522]) ).
fof(f2621,plain,
( sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1550,f2616]) ).
fof(f2624,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2621]) ).
fof(f2626,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2573,f2307]) ).
fof(f2627,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f2626]) ).
fof(f2647,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),X0,tc_fun(tc_Message_Omsg,tc_bool)))),
inference(resolution,[status(thm)],[f836,f1485]) ).
fof(f2675,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),X0,tc_fun(tc_Message_Omsg,tc_bool))))),
inference(resolution,[status(thm)],[f2647,f1434]) ).
fof(f2875,plain,
! [X0] : class_Lattices_Oupper__semilattice(tc_fun(X0,tc_bool)),
inference(resolution,[status(thm)],[f1492,f1521]) ).
fof(f2920,plain,
( sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1664,f2875]) ).
fof(f2923,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f2920]) ).
fof(f3575,plain,
! [X0] : class_Orderings_Opreorder(tc_fun(X0,tc_bool)),
inference(resolution,[status(thm)],[f1498,f1520]) ).
fof(f3739,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2066,f1522]) ).
fof(f3740,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f3739]) ).
fof(f3885,definition,
( sQ82_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),c_List_Olist_ONil(tc_Event_Oevent)),c_NS__Shared__Mirabelle_Ons__shared)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3887,plain,
( sQ82_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),c_List_Olist_ONil(tc_Event_Oevent)),c_NS__Shared__Mirabelle_Ons__shared)) ),
inference(component_clause,[status(thm)],[f3885]) ).
fof(f3901,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3887,f2203]) ).
fof(f3902,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f3901]) ).
fof(f4015,definition,
( sQ85_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f4016,plain,
( ~ sQ85_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))) ),
inference(component_clause,[status(thm)],[f4015]) ).
fof(f4022,definition,
( sQ87_spl
<=> c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4024,plain,
( sQ87_spl
| c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f4022]) ).
fof(f4030,definition,
( sQ89_spl
<=> c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f4032,plain,
( sQ89_spl
| ~ c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f4030]) ).
fof(f4045,plain,
( sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4032,f688]) ).
fof(f4046,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f4045]) ).
fof(f4047,plain,
( sQ87_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4024]) ).
fof(f4048,plain,
sQ87_spl,
inference(contradiction_clause,[status(thm)],[f4047]) ).
fof(f4049,plain,
( ~ sQ85_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))) ),
inference(forward_demodulation,[status(thm)],[f640,f4016]) ).
fof(f4050,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4049,f839]) ).
fof(f4051,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f4050]) ).
fof(f4203,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2050,f1513]) ).
fof(f4204,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f4203]) ).
fof(f4710,definition,
! [X0] :
( sQ107_spl
<=> c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f4711,plain,
! [X0] :
( ~ sQ107_spl
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) ),
inference(component_clause,[status(thm)],[f4710]) ).
fof(f4718,plain,
( ~ sQ107_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4711]) ).
fof(f4719,plain,
~ sQ107_spl,
inference(contradiction_clause,[status(thm)],[f4718]) ).
fof(f4872,definition,
( sQ115_spl
<=> class_HOL_Oord(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f4874,plain,
( sQ115_spl
| ~ class_HOL_Oord(tc_bool) ),
inference(component_clause,[status(thm)],[f4872]) ).
fof(f4879,definition,
( sQ117_spl
<=> class_HOL_Oord(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f4881,plain,
( sQ117_spl
| ~ class_HOL_Oord(tc_nat) ),
inference(component_clause,[status(thm)],[f4879]) ).
fof(f4931,plain,
( sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4881,f1515]) ).
fof(f4932,plain,
sQ117_spl,
inference(contradiction_clause,[status(thm)],[f4931]) ).
fof(f4933,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4874,f1525]) ).
fof(f4934,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f4933]) ).
fof(f5073,definition,
( sQ137_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),v_evs),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f5075,plain,
( sQ137_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),v_evs),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))) ),
inference(component_clause,[status(thm)],[f5073]) ).
fof(f5217,definition,
( sQ145_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Oagent_OSpy),c_Message_Oanalz(c_Event_Obad))) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f5219,plain,
( sQ145_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Oagent_OSpy),c_Message_Oanalz(c_Event_Obad))) ),
inference(component_clause,[status(thm)],[f5217]) ).
fof(f7957,definition,
( sQ242_spl
<=> c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f7959,plain,
( sQ242_spl
| ~ c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7957]) ).
fof(f8012,definition,
! [X0,X1,X2] :
( sQ243_spl
<=> ~ c_Fun_Oinj__on(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f8013,plain,
! [X0,X1,X2] :
( ~ sQ243_spl
| ~ c_Fun_Oinj__on(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2) ),
inference(component_clause,[status(thm)],[f8012]) ).
fof(f8397,plain,
( ~ sQ243_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1385,f8013]) ).
fof(f8398,plain,
~ sQ243_spl,
inference(contradiction_clause,[status(thm)],[f8397]) ).
fof(f9055,plain,
( sQ242_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7959,f698]) ).
fof(f9056,plain,
sQ242_spl,
inference(contradiction_clause,[status(thm)],[f9055]) ).
fof(f9104,definition,
( sQ278_spl
<=> class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f9106,plain,
( sQ278_spl
| ~ class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f9104]) ).
fof(f9140,definition,
( sQ287_spl
<=> class_Orderings_Opreorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f9142,plain,
( sQ287_spl
| ~ class_Orderings_Opreorder(tc_nat) ),
inference(component_clause,[status(thm)],[f9140]) ).
fof(f9148,definition,
( sQ289_spl
<=> class_Orderings_Opreorder(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f9150,plain,
( sQ289_spl
| ~ class_Orderings_Opreorder(tc_bool) ),
inference(component_clause,[status(thm)],[f9148]) ).
fof(f9215,plain,
( sQ287_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9142,f1510]) ).
fof(f9216,plain,
sQ287_spl,
inference(contradiction_clause,[status(thm)],[f9215]) ).
fof(f9217,plain,
( sQ289_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9150,f1520]) ).
fof(f9218,plain,
sQ289_spl,
inference(contradiction_clause,[status(thm)],[f9217]) ).
fof(f9219,plain,
( sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9106,f3575]) ).
fof(f9220,plain,
sQ278_spl,
inference(contradiction_clause,[status(thm)],[f9219]) ).
fof(f11018,definition,
( sQ385_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))) ),
introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition]) ).
fof(f11019,plain,
( ~ sQ385_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))) ),
inference(component_clause,[status(thm)],[f11018]) ).
fof(f11038,plain,
( ~ sQ385_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))) ),
inference(forward_demodulation,[status(thm)],[f640,f11019]) ).
fof(f11039,plain,
( ~ sQ385_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11038,f839]) ).
fof(f11040,plain,
~ sQ385_spl,
inference(contradiction_clause,[status(thm)],[f11039]) ).
fof(f11057,definition,
( sQ389_spl
<=> c_Orderings_Otop__class_Otop(tc_bool) = c_Orderings_Otop__class_Otop(tc_bool) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f11059,plain,
( sQ389_spl
| c_Orderings_Otop__class_Otop(tc_bool) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(component_clause,[status(thm)],[f11057]) ).
fof(f11064,plain,
( sQ389_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11059]) ).
fof(f11065,plain,
sQ389_spl,
inference(contradiction_clause,[status(thm)],[f11064]) ).
fof(f11860,definition,
! [X0] :
( sQ443_spl
<=> c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) != c_Message_Oparts(X0) ),
introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition]) ).
fof(f11861,plain,
! [X0] :
( ~ sQ443_spl
| c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) != c_Message_Oparts(X0) ),
inference(component_clause,[status(thm)],[f11860]) ).
fof(f11870,definition,
! [X0] :
( sQ445_spl
<=> c_Message_Oparts(X0) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f11871,plain,
! [X0] :
( ~ sQ445_spl
| c_Message_Oparts(X0) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f11870]) ).
fof(f12349,plain,
( ~ sQ443_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f640,f11861]) ).
fof(f12359,plain,
~ sQ443_spl,
inference(contradiction_clause,[status(thm)],[f12349]) ).
fof(f12452,definition,
( sQ466_spl
<=> c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))) = c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))) ),
introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition]) ).
fof(f12454,plain,
( sQ466_spl
| c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))) != c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))) ),
inference(component_clause,[status(thm)],[f12452]) ).
fof(f12487,plain,
( sQ466_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f12454]) ).
fof(f12488,plain,
sQ466_spl,
inference(contradiction_clause,[status(thm)],[f12487]) ).
fof(f12525,plain,
( ~ sQ5_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))) = v_X ),
inference(resolution,[status(thm)],[f1189,f1595]) ).
fof(f12526,plain,
( ~ sQ5_spl
| ~ sQ7_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f12525,f1529,f1600,f1594]) ).
fof(f12641,plain,
hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Oagent_OSpy),c_Message_Oanalz(c_Event_Obad))),
inference(resolution,[status(thm)],[f1239,f2018]) ).
fof(f12645,plain,
hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),v_evs),c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared))),
inference(resolution,[status(thm)],[f1239,f2019]) ).
fof(f12685,plain,
( sQ145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12641,f5219]) ).
fof(f12686,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f12685]) ).
fof(f12697,plain,
( sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12645,f5075]) ).
fof(f12698,plain,
sQ137_spl,
inference(contradiction_clause,[status(thm)],[f12697]) ).
fof(f12728,plain,
( ~ sQ445_spl
| hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))) ),
inference(paramodulation,[status(thm)],[f11871,f2675]) ).
fof(f12907,plain,
( ~ sQ445_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12728,f839]) ).
fof(f12908,plain,
~ sQ445_spl,
inference(contradiction_clause,[status(thm)],[f12907]) ).
fof(f12978,definition,
( sQ469_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_nat),hAPP(c_Public_OshrK,v_B)),c_Message_OsymKeys)) ),
introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition]) ).
fof(f12980,plain,
( sQ469_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_nat),hAPP(c_Public_OshrK,v_B)),c_Message_OsymKeys)) ),
inference(component_clause,[status(thm)],[f12978]) ).
fof(f12992,plain,
( sQ469_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12980,f2204]) ).
fof(f12993,plain,
sQ469_spl,
inference(contradiction_clause,[status(thm)],[f12992]) ).
fof(f13523,definition,
( sQ488_spl
<=> v_X = v_X ),
introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition]) ).
fof(f13525,plain,
( sQ488_spl
| v_X != v_X ),
inference(component_clause,[status(thm)],[f13523]) ).
fof(f13527,plain,
( sQ488_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13525]) ).
fof(f13528,plain,
sQ488_spl,
inference(contradiction_clause,[status(thm)],[f13527]) ).
fof(f14056,definition,
( sQ525_spl
<=> v_K = v_K ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f14058,plain,
( sQ525_spl
| v_K != v_K ),
inference(component_clause,[status(thm)],[f14056]) ).
fof(f14669,definition,
( sQ578_spl
<=> hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f14671,plain,
( sQ578_spl
| ~ hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f14669]) ).
fof(f14673,plain,
( sQ578_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14671,f969]) ).
fof(f14674,plain,
sQ578_spl,
inference(contradiction_clause,[status(thm)],[f14673]) ).
fof(f14763,plain,
( sQ525_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f14058]) ).
fof(f14764,plain,
sQ525_spl,
inference(contradiction_clause,[status(thm)],[f14763]) ).
fof(f16581,plain,
( ~ sQ5_spl
| ~ hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))
| ~ hBOOL(hAPP(hAPP(c_in(tc_nat),v_K),c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat))) ),
inference(resolution,[status(thm)],[f1388,f1595]) ).
fof(f16582,plain,
( ~ sQ5_spl
| ~ sQ7_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f16581,f1532,f1600,f1594]) ).
fof(f16583,plain,
$false,
inference(sat_refutation,[status(thm)],[f1535,f1603,f1605,f1657,f2053,f2076,f2432,f2624,f2627,f2923,f3740,f3902,f4046,f4048,f4051,f4204,f4719,f4932,f4934,f8398,f9056,f9216,f9218,f9220,f11040,f11065,f12359,f12488,f12526,f12686,f12698,f12908,f12993,f13528,f14674,f14764,f16582]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV731-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n020.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 09:23:03 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.23/0.52 % Drodi V4.1.1
% 141.98/18.58 % Refutation found
% 141.98/18.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 141.98/18.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.97/20.29 % Elapsed time: 19.818608 seconds
% 10.97/20.29 % CPU time: 148.329359 seconds
% 10.97/20.29 % Total memory used: 945.201 MB
% 10.97/20.29 % Net memory used: 873.924 MB
%------------------------------------------------------------------------------