%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV731-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:53:04 PM UTC 2026
% Result : Unsatisfiable 20.12s 13.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV731-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/10.32 % Computer : n012.cluster.edu
% 0.03/10.32 % Model : x86_64 x86_64
% 0.03/10.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/10.32 % Memory : 8046.5625MB
% 0.03/10.32 % OS : Linux 6.8.0-71-generic
% 0.03/10.32 % CPULimit : 300
% 0.03/10.32 % WCLimit : 300
% 0.03/10.32 % DateTime : Mon Sep 21 09:22:03 UTC 2026
% 0.03/10.32 % CPUTime :
% 0.03/10.35 % Drodi V4.1.1
% 20.12/13.08 % Refutation found
% 20.12/13.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 20.12/13.08 % SZS output start CNFRefutation for theBenchmark
% 20.12/13.08 fof(f5,axiom,(
% 20.12/13.08 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)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f8,axiom,(
% 20.12/13.08 c_Message_Oanalz(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f18,axiom,(
% 20.12/13.08 (![V_A,V_B,V_C,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f22,axiom,(
% 20.12/13.08 (![V_A,V_B,V_C,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f23,axiom,(
% 20.12/13.08 (![V_f,T_a,T_b]: (c_Fun_Oinj__on(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a,T_b) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f37,axiom,(
% 20.12/13.08 (![V_A,V_B,T_a,V_x]: (( c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))| ~ c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f41,axiom,(
% 20.12/13.08 (![V_a,V_B,T_a,V_C]: (c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(V_a,V_B,T_a),V_C,tc_fun(T_a,tc_bool)) = c_Set_Oinsert(V_a,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),T_a) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f51,axiom,(
% 20.12/13.08 (![T_a]: (c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f55,axiom,(
% 20.12/13.08 (![V_B,V_x,V_A,T_a]: (( hBOOL(hAPP(V_B,V_x))| hBOOL(hAPP(V_A,V_x))| ~ hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f56,axiom,(
% 20.12/13.08 (![V_A,V_B,T_a,V_x]: (( hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x))| ~ hBOOL(hAPP(V_B,V_x)) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f71,axiom,(
% 20.12/13.08 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f101,axiom,(
% 20.12/13.08 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)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f123,axiom,(
% 20.12/13.08 (![V_A,V_B,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_B,V_A,tc_fun(T_a,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f143,axiom,(
% 20.12/13.08 (![T_a,V_x]: (~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f154,axiom,(
% 20.12/13.08 (![V_f,V_A,V_B,T_b,T_a]: (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) = 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)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f164,axiom,(
% 20.12/13.08 (![V_H]: (c_lessequals(V_H,c_Message_Oparts(V_H),tc_fun(tc_Message_Omsg,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f165,axiom,(
% 20.12/13.08 (![V_G,V_H]: (( c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_fun(tc_Message_Omsg,tc_bool))| ~ c_lessequals(V_G,V_H,tc_fun(tc_Message_Omsg,tc_bool)) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f172,axiom,(
% 20.12/13.08 (![V_A,T_a]: (c_lessequals(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f174,axiom,(
% 20.12/13.08 (![V_A,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f234,axiom,(
% 20.12/13.08 hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f311,axiom,(
% 20.12/13.08 (![V_E]: (c_Message_OkeysFor(c_Set_Oimage(c_Message_Omsg_OKey,V_E,tc_nat,tc_Message_Omsg)) = c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f386,axiom,(
% 20.12/13.08 (![V_X,V_B,V_K,V_A,V_evs,V_K_H,V_N]: (( 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)))| ~ 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(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))) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f530,axiom,(
% 20.12/13.08 c_Fun_Oinj__on(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f531,axiom,(
% 20.12/13.08 ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OServer),c_Event_Obad)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f532,axiom,(
% 20.12/13.08 (![V_K,V_evs,V_A,V_K_H,V_N,V_B,V_X]: (( ~ 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)))| ~ 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(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))) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f538,axiom,(
% 20.12/13.08 (![V_K,V_X,V_A]: (~ hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(V_K,V_X)),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg))) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f553,axiom,(
% 20.12/13.08 (![V_A,V_NA,V_B,V_K,V_X,V_evs]: (( 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)))| ~ 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_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)))) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f602,negated_conjecture,(
% 20.12/13.08 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)))) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f603,negated_conjecture,(
% 20.12/13.08 ~ hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f604,negated_conjecture,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f605,negated_conjecture,(
% 20.12/13.08 ( 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)))| 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))) ) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f607,axiom,(
% 20.12/13.08 (![T_2,T_1]: (( class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1))| ~ class_Lattices_Olattice(T_1) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f610,axiom,(
% 20.12/13.08 (![T_2,T_1]: (( class_Orderings_Opreorder(tc_fun(T_2,T_1))| ~ class_Orderings_Opreorder(T_1) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f612,axiom,(
% 20.12/13.08 (![T_2,T_1]: (( class_Orderings_Oorder(tc_fun(T_2,T_1))| ~ class_Orderings_Oorder(T_1) ) ))),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f617,axiom,(
% 20.12/13.08 class_Orderings_Opreorder(tc_nat) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f622,axiom,(
% 20.12/13.08 class_HOL_Oord(tc_nat) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f627,axiom,(
% 20.12/13.08 class_Orderings_Opreorder(tc_bool) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f628,axiom,(
% 20.12/13.08 class_Lattices_Olattice(tc_bool) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f629,axiom,(
% 20.12/13.08 class_Orderings_Oorder(tc_bool) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f632,axiom,(
% 20.12/13.08 class_HOL_Oord(tc_bool) ),
% 20.12/13.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.12/13.08 fof(f640,plain,(
% 20.12/13.08 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))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f5])).
% 20.12/13.08 fof(f643,plain,(
% 20.12/13.08 c_Message_Oanalz(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))=c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f8])).
% 20.12/13.08 fof(f654,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X3,tc_bool)),X2,tc_fun(X3,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f18])).
% 20.12/13.08 fof(f660,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(X1,c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f22])).
% 20.12/13.08 fof(f661,plain,(
% 20.12/13.08 ![X0,X1,X2]: (c_Fun_Oinj__on(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,X2))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f23])).
% 20.12/13.08 fof(f679,plain,(
% 20.12/13.08 ![V_A,V_B,T_a]: (c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))|(![V_x]: ~c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f37])).
% 20.12/13.08 fof(f680,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (c_lessequals(X0,X1,tc_fun(X2,tc_bool))|~c_lessequals(c_Set_Oinsert(X3,X0,X2),X1,tc_fun(X2,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f679])).
% 20.12/13.08 fof(f685,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool))=c_Set_Oinsert(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_bool)),X2))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f41])).
% 20.12/13.08 fof(f698,plain,(
% 20.12/13.08 ![X0]: (c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f51])).
% 20.12/13.08 fof(f704,plain,(
% 20.12/13.08 ![V_B,V_x,V_A]: ((hBOOL(hAPP(V_B,V_x))|hBOOL(hAPP(V_A,V_x)))|(![T_a]: ~hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x))))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f55])).
% 20.12/13.08 fof(f705,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|hBOOL(hAPP(X2,X1))|~hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X0,tc_fun(X3,tc_bool)),X1)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f704])).
% 20.12/13.08 fof(f706,plain,(
% 20.12/13.08 ![V_B,V_x]: ((![V_A,T_a]: hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)))|~hBOOL(hAPP(V_B,V_x)))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f56])).
% 20.12/13.08 fof(f707,plain,(
% 20.12/13.08 ![X0,X1,X2,X3]: (hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3))|~hBOOL(hAPP(X1,X3)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f706])).
% 20.12/13.08 fof(f728,plain,(
% 20.12/13.08 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f71])).
% 20.12/13.08 fof(f765,plain,(
% 20.12/13.08 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))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f101])).
% 20.12/13.08 fof(f803,plain,(
% 20.12/13.08 ![X0,X1,X2]: (c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(X1,X0,tc_fun(X2,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f123])).
% 20.12/13.08 fof(f839,plain,(
% 20.12/13.08 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f143])).
% 20.12/13.08 fof(f853,plain,(
% 20.12/13.08 ![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)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f154])).
% 20.12/13.08 fof(f868,plain,(
% 20.12/13.08 ![X0]: (c_lessequals(X0,c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f164])).
% 20.12/13.08 fof(f869,plain,(
% 20.12/13.08 ![X0,X1]: (c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_fun(tc_Message_Omsg,tc_bool))|~c_lessequals(X0,X1,tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f165])).
% 20.12/13.08 fof(f879,plain,(
% 20.12/13.08 ![X0,X1]: (c_lessequals(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f172])).
% 20.12/13.08 fof(f881,plain,(
% 20.12/13.08 ![X0,X1]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f174])).
% 20.12/13.08 fof(f969,plain,(
% 20.12/13.08 hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f234])).
% 20.12/13.08 fof(f1069,plain,(
% 20.12/13.08 ![X0]: (c_Message_OkeysFor(c_Set_Oimage(c_Message_Omsg_OKey,X0,tc_nat,tc_Message_Omsg))=c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f311])).
% 20.12/13.08 fof(f1188,plain,(
% 20.12/13.08 ![V_X,V_B,V_K,V_A,V_evs]: ((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)))|~hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared)))|(![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)))))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f386])).
% 20.12/13.08 fof(f1189,plain,(
% 20.12/13.08 ![X0,X1,X2,X3,X4,X5,X6]: (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(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),X4),c_NS__Shared__Mirabelle_Ons__shared))|~hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,X3,c_Message_Omsg_OCrypt(X5,c_Message_Omsg_OMPair(X6,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))))),c_List_Oset(X4,tc_Event_Oevent))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f1188])).
% 20.12/13.08 fof(f1385,plain,(
% 20.12/13.08 c_Fun_Oinj__on(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f530])).
% 20.12/13.08 fof(f1386,plain,(
% 20.12/13.08 ~hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OServer),c_Event_Obad))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f531])).
% 20.12/13.08 fof(f1387,plain,(
% 20.12/13.08 ![V_K,V_evs]: ((~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)))|~hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),V_evs),c_NS__Shared__Mirabelle_Ons__shared)))|(![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)))))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f532])).
% 20.12/13.08 fof(f1388,plain,(
% 20.12/13.08 ![X0,X1,X2,X3,X4,X5,X6]: (~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)))|~hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),X1),c_NS__Shared__Mirabelle_Ons__shared))|~hBOOL(hAPP(hAPP(c_in(tc_Event_Oevent),c_Event_Oevent_OSays(c_Message_Oagent_OServer,X2,c_Message_Omsg_OCrypt(X3,c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X5),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X0),X6)))))),c_List_Oset(X1,tc_Event_Oevent))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f1387])).
% 20.12/13.08 fof(f1396,plain,(
% 20.12/13.08 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OCrypt(X0,X1)),c_Set_Oimage(c_Message_Omsg_OKey,X2,tc_nat,tc_Message_Omsg))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f538])).
% 20.12/13.08 fof(f1417,plain,(
% 20.12/13.08 ![X0,X1,X2,X3,X4,X5]: (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)))|~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_Oagent),X0),c_Event_Obad))|~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)))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f553])).
% 20.12/13.08 fof(f1485,plain,(
% 20.12/13.08 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))))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f602])).
% 20.12/13.08 fof(f1486,plain,(
% 20.12/13.08 ~hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f603])).
% 20.12/13.08 fof(f1487,plain,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f604])).
% 20.12/13.08 fof(f1488,plain,(
% 20.12/13.08 ~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)))|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)))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f605])).
% 20.12/13.08 fof(f1491,plain,(
% 20.12/13.08 ![T_1]: ((![T_2]: class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)))|~class_Lattices_Olattice(T_1))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f607])).
% 20.12/13.08 fof(f1492,plain,(
% 20.12/13.08 ![X0,X1]: (class_Lattices_Oupper__semilattice(tc_fun(X0,X1))|~class_Lattices_Olattice(X1))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f1491])).
% 20.12/13.08 fof(f1497,plain,(
% 20.12/13.08 ![T_1]: ((![T_2]: class_Orderings_Opreorder(tc_fun(T_2,T_1)))|~class_Orderings_Opreorder(T_1))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f610])).
% 20.12/13.08 fof(f1498,plain,(
% 20.12/13.08 ![X0,X1]: (class_Orderings_Opreorder(tc_fun(X0,X1))|~class_Orderings_Opreorder(X1))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f1497])).
% 20.12/13.08 fof(f1501,plain,(
% 20.12/13.08 ![T_1]: ((![T_2]: class_Orderings_Oorder(tc_fun(T_2,T_1)))|~class_Orderings_Oorder(T_1))),
% 20.12/13.08 inference(miniscoping,[status(thm)],[f612])).
% 20.12/13.08 fof(f1502,plain,(
% 20.12/13.08 ![X0,X1]: (class_Orderings_Oorder(tc_fun(X0,X1))|~class_Orderings_Oorder(X1))),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f1501])).
% 20.12/13.08 fof(f1510,plain,(
% 20.12/13.08 class_Orderings_Opreorder(tc_nat)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f617])).
% 20.12/13.08 fof(f1515,plain,(
% 20.12/13.08 class_HOL_Oord(tc_nat)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f622])).
% 20.12/13.08 fof(f1520,plain,(
% 20.12/13.08 class_Orderings_Opreorder(tc_bool)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f627])).
% 20.12/13.08 fof(f1521,plain,(
% 20.12/13.08 class_Lattices_Olattice(tc_bool)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f628])).
% 20.12/13.08 fof(f1522,plain,(
% 20.12/13.08 class_Orderings_Oorder(tc_bool)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f629])).
% 20.12/13.08 fof(f1525,plain,(
% 20.12/13.08 class_HOL_Oord(tc_bool)),
% 20.12/13.08 inference(cnf_transformation,[status(thm)],[f632])).
% 20.12/13.08 fof(f1529,definition,(
% 20.12/13.08 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))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f1532,definition,(
% 20.12/13.08 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))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f1535,plain,(
% 20.12/13.08 ~sQ0_spl|sQ1_spl),
% 20.12/13.08 inference(split_clause,[status(thm)],[f1488,f1529,f1532])).
% 20.12/13.08 fof(f1659,plain,(
% 20.12/13.08 ![X0]: (c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))),tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f879,f869])).
% 20.12/13.08 fof(f1952,plain,(
% 20.12/13.08 ![X0,X1]: (c_lessequals(X0,c_Message_Oparts(c_Set_Oinsert(X1,X0,tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f680,f868])).
% 20.12/13.08 fof(f2011,plain,(
% 20.12/13.08 ![X0,X1,X2]: (c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))=c_Set_Oinsert(X1,c_Lattices_Oupper__semilattice__class_Osup(X2,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X0))),
% 20.12/13.08 inference(paramodulation,[status(thm)],[f881,f685])).
% 20.12/13.08 fof(f2027,plain,(
% 20.12/13.08 ![X0,X1]: (c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))=c_Set_Oinsert(X1,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X0))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f881,f2011])).
% 20.12/13.08 fof(f2136,definition,(
% 20.12/13.08 ![X1,X2]: (sQ3_spl <=> (~c_Finite__Set_Ofinite(X1,X2)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f2137,plain,(
% 20.12/13.08 ![X0,X1]: (~c_Finite__Set_Ofinite(X0,X1)|~sQ3_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f2136])).
% 20.12/13.08 fof(f2411,plain,(
% 20.12/13.08 ![X0,X1]: (hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),tc_fun(X1,tc_bool)),c_NS__Shared__Mirabelle_Ons__shared)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f707,f1487])).
% 20.12/13.08 fof(f2588,plain,(
% 20.12/13.08 ![X0]: (hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))|hBOOL(hAPP(X0,c_NS__Shared__Mirabelle_Ons__shared)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f2411,f705])).
% 20.12/13.08 fof(f2596,definition,(
% 20.12/13.08 sQ4_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f2599,definition,(
% 20.12/13.08 ![X0]: (sQ5_spl <=> (hBOOL(hAPP(X0,c_NS__Shared__Mirabelle_Ons__shared))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f2600,plain,(
% 20.12/13.08 ![X0]: (hBOOL(hAPP(X0,c_NS__Shared__Mirabelle_Ons__shared))|~sQ5_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f2599])).
% 20.12/13.08 fof(f2602,plain,(
% 20.12/13.08 sQ4_spl|sQ5_spl),
% 20.12/13.08 inference(split_clause,[status(thm)],[f2588,f2596,f2599])).
% 20.12/13.08 fof(f3465,plain,(
% 20.12/13.08 ![X0]: (class_Lattices_Oupper__semilattice(tc_fun(X0,tc_bool)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f1492,f1521])).
% 20.12/13.08 fof(f3725,plain,(
% 20.12/13.08 ![X0]: (class_Orderings_Opreorder(tc_fun(X0,tc_bool)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f1498,f1520])).
% 20.12/13.08 fof(f4351,plain,(
% 20.12/13.08 ![X0]: (class_Orderings_Oorder(tc_fun(X0,tc_bool)))),
% 20.12/13.08 inference(resolution,[status(thm)],[f1502,f1522])).
% 20.12/13.08 fof(f4777,plain,(
% 20.12/13.08 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_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_Lattices_Oupper__semilattice__class_Osup(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),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)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f654,f765])).
% 20.12/13.08 fof(f4778,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=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_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f654,f4777])).
% 20.12/13.08 fof(f4779,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=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_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_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f654,f4778])).
% 20.12/13.08 fof(f4780,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=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_Lattices_Oupper__semilattice__class_Osup(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),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_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),c_Lattices_Oupper__semilattice__class_Osup(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),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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f660,f4779])).
% 20.12/13.08 fof(f4781,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),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_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_OSignature),c_Event_Obad,tc_Message_Oagent,tc_nat),tc_nat,tc_nat),tc_nat,tc_Message_Omsg),c_Lattices_Oupper__semilattice__class_Osup(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),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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f660,f4780])).
% 20.12/13.08 fof(f4782,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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_OSignature),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_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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f660,f4781])).
% 20.12/13.08 fof(f4783,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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_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_OSignature),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_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)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f660,f4782])).
% 20.12/13.08 fof(f4784,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f853,f4783])).
% 20.12/13.08 fof(f4785,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f853,f4784])).
% 20.12/13.08 fof(f4786,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Lattices_Oupper__semilattice__class_Osup(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),c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool))),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f853,f4785])).
% 20.12/13.08 fof(f4787,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg)),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f853,f4786])).
% 20.12/13.08 fof(f4840,definition,(
% 20.12/13.08 sQ101_spl <=> (c_lessequals(c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))),c_Message_Oparts(c_Set_Oinsert(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_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f4842,plain,(
% 20.12/13.08 ~c_lessequals(c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))),c_Message_Oparts(c_Set_Oinsert(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_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool))|sQ101_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f4840])).
% 20.12/13.08 fof(f4928,plain,(
% 20.12/13.08 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)))|~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))),
% 20.12/13.08 inference(resolution,[status(thm)],[f1417,f1485])).
% 20.12/13.08 fof(f4930,definition,(
% 20.12/13.08 sQ106_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))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f4931,plain,(
% 20.12/13.08 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)))|~sQ106_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f4930])).
% 20.12/13.08 fof(f4933,definition,(
% 20.12/13.08 sQ107_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f4934,plain,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),v_A),c_Event_Obad))|~sQ107_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f4933])).
% 20.12/13.08 fof(f4936,plain,(
% 20.12/13.08 sQ106_spl|~sQ4_spl|sQ107_spl),
% 20.12/13.08 inference(split_clause,[status(thm)],[f4928,f4930,f2596,f4933])).
% 20.12/13.08 fof(f4937,plain,(
% 20.12/13.08 $false|~sQ107_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f4934,f1486])).
% 20.12/13.08 fof(f4938,plain,(
% 20.12/13.08 ~sQ107_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f4937])).
% 20.12/13.08 fof(f4942,plain,(
% 20.12/13.08 $false|~sQ5_spl),
% 20.12/13.08 inference(resolution,[status(thm)],[f2600,f728])).
% 20.12/13.08 fof(f4956,plain,(
% 20.12/13.08 ~sQ5_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f4942])).
% 20.12/13.08 fof(f5936,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),c_Lattices_Oupper__semilattice__class_Osup(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),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_Lattices_Oupper__semilattice__class_Osup(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),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_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg)),
% 20.12/13.08 inference(backward_demodulation,[status(thm)],[f803,f4787])).
% 20.12/13.08 fof(f6074,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg)),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f660,f5936])).
% 20.12/13.08 fof(f6075,plain,(
% 20.12/13.08 c_Event_OinitState(c_Message_Oagent_OSpy)=c_Set_Oimage(c_Message_Omsg_OKey,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Public_OshrK,c_Event_Obad,tc_Message_Oagent,tc_nat),c_Lattices_Oupper__semilattice__class_Osup(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),c_Lattices_Oupper__semilattice__class_Osup(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),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),tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_bool)),tc_nat,tc_Message_Omsg)),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f853,f6074])).
% 20.12/13.08 fof(f6192,definition,(
% 20.12/13.08 sQ161_spl <=> (c_Event_OinitState(c_Message_Oagent_OSpy)=c_Event_OinitState(c_Message_Oagent_OSpy))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f6194,plain,(
% 20.12/13.08 ~c_Event_OinitState(c_Message_Oagent_OSpy)=c_Event_OinitState(c_Message_Oagent_OSpy)|sQ161_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f6192])).
% 20.12/13.08 fof(f6225,definition,(
% 20.12/13.08 sQ169_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)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f6227,plain,(
% 20.12/13.08 ~c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))|sQ169_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f6225])).
% 20.12/13.08 fof(f6232,plain,(
% 20.12/13.08 $false|sQ161_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f6194])).
% 20.12/13.08 fof(f6233,plain,(
% 20.12/13.08 sQ161_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f6232])).
% 20.12/13.08 fof(f6234,plain,(
% 20.12/13.08 $false|sQ169_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f6227])).
% 20.12/13.08 fof(f6235,plain,(
% 20.12/13.08 sQ169_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f6234])).
% 20.12/13.08 fof(f6318,definition,(
% 20.12/13.08 sQ172_spl <=> (c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),c_Message_Oparts(c_Set_Oinsert(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)),tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f6320,plain,(
% 20.12/13.08 ~c_lessequals(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),c_Message_Oparts(c_Set_Oinsert(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)),tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool))|sQ172_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f6318])).
% 20.12/13.08 fof(f6814,definition,(
% 20.12/13.08 sQ186_spl <=> (class_HOL_Oord(tc_bool))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f6816,plain,(
% 20.12/13.08 ~class_HOL_Oord(tc_bool)|sQ186_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f6814])).
% 20.12/13.08 fof(f6933,definition,(
% 20.12/13.08 sQ216_spl <=> (class_HOL_Oord(tc_nat))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f6935,plain,(
% 20.12/13.08 ~class_HOL_Oord(tc_nat)|sQ216_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f6933])).
% 20.12/13.08 fof(f6944,plain,(
% 20.12/13.08 $false|sQ186_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f6816,f1525])).
% 20.12/13.08 fof(f6945,plain,(
% 20.12/13.08 sQ186_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f6944])).
% 20.12/13.08 fof(f6946,plain,(
% 20.12/13.08 $false|sQ216_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f6935,f1515])).
% 20.12/13.08 fof(f6947,plain,(
% 20.12/13.08 sQ216_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f6946])).
% 20.12/13.08 fof(f7282,definition,(
% 20.12/13.08 sQ238_spl <=> (c_Event_OinitState(c_Message_Oagent_OServer)=c_Event_OinitState(c_Message_Oagent_OServer))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f7284,plain,(
% 20.12/13.08 ~c_Event_OinitState(c_Message_Oagent_OServer)=c_Event_OinitState(c_Message_Oagent_OServer)|sQ238_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f7282])).
% 20.12/13.08 fof(f7316,plain,(
% 20.12/13.08 $false|sQ238_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f7284])).
% 20.12/13.08 fof(f7317,plain,(
% 20.12/13.08 sQ238_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f7316])).
% 20.12/13.08 fof(f7990,definition,(
% 20.12/13.08 ![X0]: (sQ296_spl <=> (~c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f7991,plain,(
% 20.12/13.08 ![X0]: (~c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))|~sQ296_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f7990])).
% 20.12/13.08 fof(f8006,plain,(
% 20.12/13.08 $false|~sQ296_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f7991])).
% 20.12/13.08 fof(f8007,plain,(
% 20.12/13.08 ~sQ296_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f8006])).
% 20.12/13.08 fof(f10447,definition,(
% 20.12/13.08 sQ550_spl <=> (class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f10449,plain,(
% 20.12/13.08 ~class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool))|sQ550_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f10447])).
% 20.12/13.08 fof(f10454,definition,(
% 20.12/13.08 sQ552_spl <=> (class_Orderings_Opreorder(tc_bool))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f10456,plain,(
% 20.12/13.08 ~class_Orderings_Opreorder(tc_bool)|sQ552_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f10454])).
% 20.12/13.08 fof(f10485,definition,(
% 20.12/13.08 sQ560_spl <=> (class_Orderings_Opreorder(tc_nat))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f10487,plain,(
% 20.12/13.08 ~class_Orderings_Opreorder(tc_nat)|sQ560_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f10485])).
% 20.12/13.08 fof(f10658,plain,(
% 20.12/13.08 $false|sQ550_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f10449,f3725])).
% 20.12/13.08 fof(f10659,plain,(
% 20.12/13.08 sQ550_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f10658])).
% 20.12/13.08 fof(f10660,plain,(
% 20.12/13.08 $false|sQ552_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f10456,f1520])).
% 20.12/13.08 fof(f10661,plain,(
% 20.12/13.08 sQ552_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f10660])).
% 20.12/13.08 fof(f10662,plain,(
% 20.12/13.08 $false|sQ560_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f10487,f1510])).
% 20.12/13.08 fof(f10663,plain,(
% 20.12/13.08 sQ560_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f10662])).
% 20.12/13.08 fof(f11450,definition,(
% 20.12/13.08 ![X2,X3,X4]: (sQ623_spl <=> (~c_Fun_Oinj__on(X2,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)),X3,X4)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f11451,plain,(
% 20.12/13.08 ![X0,X1,X2]: (~c_Fun_Oinj__on(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2)|~sQ623_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f11450])).
% 20.12/13.08 fof(f13224,definition,(
% 20.12/13.08 sQ678_spl <=> (c_Orderings_Otop__class_Otop(tc_bool)=c_Orderings_Otop__class_Otop(tc_bool))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f13226,plain,(
% 20.12/13.08 ~c_Orderings_Otop__class_Otop(tc_bool)=c_Orderings_Otop__class_Otop(tc_bool)|sQ678_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f13224])).
% 20.12/13.08 fof(f14754,plain,(
% 20.12/13.08 $false|sQ172_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f6320,f1952])).
% 20.12/13.08 fof(f14755,plain,(
% 20.12/13.08 sQ172_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f14754])).
% 20.12/13.08 fof(f16109,plain,(
% 20.12/13.08 $false|sQ678_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f13226])).
% 20.12/13.08 fof(f16110,plain,(
% 20.12/13.08 sQ678_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f16109])).
% 20.12/13.08 fof(f18977,plain,(
% 20.12/13.08 c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy))=c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool))),
% 20.12/13.08 inference(paramodulation,[status(thm)],[f6075,f1069])).
% 20.12/13.08 fof(f19058,plain,(
% 20.12/13.08 c_Finite__Set_Ofinite(c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat)),
% 20.12/13.08 inference(paramodulation,[status(thm)],[f18977,f698])).
% 20.12/13.08 fof(f19062,plain,(
% 20.12/13.08 ![X0,X1]: (c_Fun_Oinj__on(X0,c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat,X1))),
% 20.12/13.08 inference(paramodulation,[status(thm)],[f18977,f661])).
% 20.12/13.08 fof(f20189,definition,(
% 20.12/13.08 sQ1016_spl <=> (class_Orderings_Opreorder(tc_fun(tc_nat,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1016_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f20191,plain,(
% 20.12/13.08 ~class_Orderings_Opreorder(tc_fun(tc_nat,tc_bool))|sQ1016_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f20189])).
% 20.12/13.08 fof(f20196,definition,(
% 20.12/13.08 sQ1018_spl <=> (class_Orderings_Oorder(tc_fun(tc_nat,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f20198,plain,(
% 20.12/13.08 ~class_Orderings_Oorder(tc_fun(tc_nat,tc_bool))|sQ1018_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f20196])).
% 20.12/13.08 fof(f20203,definition,(
% 20.12/13.08 sQ1020_spl <=> (class_Lattices_Oupper__semilattice(tc_fun(tc_nat,tc_bool)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1020_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f20205,plain,(
% 20.12/13.08 ~class_Lattices_Oupper__semilattice(tc_fun(tc_nat,tc_bool))|sQ1020_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f20203])).
% 20.12/13.08 fof(f20227,plain,(
% 20.12/13.08 $false|sQ1020_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f20205,f3465])).
% 20.12/13.08 fof(f20228,plain,(
% 20.12/13.08 sQ1020_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f20227])).
% 20.12/13.08 fof(f20229,plain,(
% 20.12/13.08 $false|sQ1018_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f20198,f4351])).
% 20.12/13.08 fof(f20230,plain,(
% 20.12/13.08 sQ1018_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f20229])).
% 20.12/13.08 fof(f20231,plain,(
% 20.12/13.08 $false|sQ1016_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f20191,f3725])).
% 20.12/13.08 fof(f20232,plain,(
% 20.12/13.08 sQ1016_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f20231])).
% 20.12/13.08 fof(f20238,definition,(
% 20.12/13.08 ![X0,X1]: (sQ1026_spl <=> (~c_Fun_Oinj__on(X0,c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat,X1)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f20239,plain,(
% 20.12/13.08 ![X0,X1]: (~c_Fun_Oinj__on(X0,c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat,X1)|~sQ1026_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f20238])).
% 20.12/13.08 fof(f20340,plain,(
% 20.12/13.08 $false|~sQ1026_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f20239,f19062])).
% 20.12/13.08 fof(f20341,plain,(
% 20.12/13.08 ~sQ1026_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f20340])).
% 20.12/13.08 fof(f20442,plain,(
% 20.12/13.08 $false|~sQ3_spl),
% 20.12/13.08 inference(backward_subsumption_resolution,[status(thm)],[f19058,f2137])).
% 20.12/13.08 fof(f20472,plain,(
% 20.12/13.08 ~sQ3_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f20442])).
% 20.12/13.08 fof(f21610,definition,(
% 20.12/13.08 sQ1105_spl <=> (hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1105_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f21612,plain,(
% 20.12/13.08 ~hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)))|sQ1105_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f21610])).
% 20.12/13.08 fof(f21800,plain,(
% 20.12/13.08 $false|sQ1105_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f21612,f969])).
% 20.12/13.08 fof(f21801,plain,(
% 20.12/13.08 sQ1105_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f21800])).
% 20.12/13.08 fof(f24681,plain,(
% 20.12/13.08 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)))|~hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))|~sQ106_spl),
% 20.12/13.08 inference(resolution,[status(thm)],[f1189,f4931])).
% 20.12/13.08 fof(f24683,plain,(
% 20.12/13.08 sQ0_spl|~sQ4_spl|~sQ106_spl),
% 20.12/13.08 inference(split_clause,[status(thm)],[f24681,f1529,f2596,f4930])).
% 20.12/13.08 fof(f24932,definition,(
% 20.12/13.08 sQ1220_spl <=> (v_X=v_X)),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1220_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f24934,plain,(
% 20.12/13.08 ~v_X=v_X|sQ1220_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f24932])).
% 20.12/13.08 fof(f24939,plain,(
% 20.12/13.08 $false|sQ1220_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f24934])).
% 20.12/13.08 fof(f24940,plain,(
% 20.12/13.08 sQ1220_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f24939])).
% 20.12/13.08 fof(f26014,definition,(
% 20.12/13.08 sQ1255_spl <=> (hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),c_Public_OshrK,tc_Message_Oagent,tc_nat),v_K)=hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),c_Public_OshrK,tc_Message_Oagent,tc_nat),v_K))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1255_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f26016,plain,(
% 20.12/13.08 ~hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),c_Public_OshrK,tc_Message_Oagent,tc_nat),v_K)=hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),c_Public_OshrK,tc_Message_Oagent,tc_nat),v_K)|sQ1255_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f26014])).
% 20.12/13.08 fof(f26018,plain,(
% 20.12/13.08 $false|sQ1255_spl),
% 20.12/13.08 inference(trivial_equality_resolution,[status(thm)],[f26016])).
% 20.12/13.08 fof(f26019,plain,(
% 20.12/13.08 sQ1255_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f26018])).
% 20.12/13.08 fof(f30075,definition,(
% 20.12/13.08 sQ1433_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OServer),c_Event_Obad)))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1433_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f30076,plain,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_Message_Oagent),c_Message_Oagent_OServer),c_Event_Obad))|~sQ1433_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f30075])).
% 20.12/13.08 fof(f30107,plain,(
% 20.12/13.08 $false|~sQ1433_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f30076,f1386])).
% 20.12/13.08 fof(f30108,plain,(
% 20.12/13.08 ~sQ1433_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f30107])).
% 20.12/13.08 fof(f30256,definition,(
% 20.12/13.08 sQ1446_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Message_Oanalz(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1446_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f30257,plain,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Message_Oanalz(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))))|~sQ1446_spl),
% 20.12/13.08 inference(component_clause,[status(thm)],[f30256])).
% 20.12/13.08 fof(f30276,plain,(
% 20.12/13.08 ~c_lessequals(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))),tc_fun(tc_Message_Omsg,tc_bool))|sQ101_spl),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f2027,f4842])).
% 20.12/13.08 fof(f30277,plain,(
% 20.12/13.08 $false|sQ101_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f30276,f1659])).
% 20.12/13.08 fof(f30278,plain,(
% 20.12/13.08 sQ101_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f30277])).
% 20.12/13.08 fof(f30280,plain,(
% 20.12/13.08 hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))|~sQ1446_spl),
% 20.12/13.08 inference(forward_demodulation,[status(thm)],[f643,f30257])).
% 20.12/13.08 fof(f30281,plain,(
% 20.12/13.08 $false|~sQ1446_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f30280,f839])).
% 20.12/13.08 fof(f30282,plain,(
% 20.12/13.08 ~sQ1446_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f30281])).
% 20.12/13.08 fof(f31140,definition,(
% 20.12/13.08 ![X1]: (sQ1461_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_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oinsert(X1,c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat),tc_nat,tc_Message_Omsg)))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1461_spl])],[split_symbol_definition])).
% 20.12/13.08 fof(f31141,plain,(
% 20.12/13.08 ![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_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oinsert(X0,c_Message_OkeysFor(c_Event_OinitState(c_Message_Oagent_OSpy)),tc_nat),tc_nat,tc_Message_Omsg)))|~sQ1461_spl)),
% 20.12/13.08 inference(component_clause,[status(thm)],[f31140])).
% 20.12/13.08 fof(f31148,plain,(
% 20.12/13.08 $false|~sQ1461_spl),
% 20.12/13.08 inference(forward_subsumption_resolution,[status(thm)],[f31141,f1396])).
% 20.12/13.08 fof(f31149,plain,(
% 20.12/13.08 ~sQ1461_spl),
% 20.12/13.08 inference(contradiction_clause,[status(thm)],[f31148])).
% 20.12/13.08 fof(f32325,definition,(
% 20.12/13.08 sQ1523_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))))),
% 20.12/13.08 introduced(definition,[new_symbols(definition,[sQ1523_spl])],[split_symbol_definition])).
% 20.83/13.13 fof(f32326,plain,(
% 20.83/13.13 hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))))|~sQ1523_spl),
% 20.83/13.13 inference(component_clause,[status(thm)],[f32325])).
% 20.83/13.13 fof(f32335,plain,(
% 20.83/13.13 hBOOL(hAPP(hAPP(c_in(tc_Message_Omsg),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))))|~sQ1523_spl),
% 20.83/13.13 inference(forward_demodulation,[status(thm)],[f640,f32326])).
% 20.83/13.13 fof(f32336,plain,(
% 20.83/13.13 $false|~sQ1523_spl),
% 20.83/13.13 inference(forward_subsumption_resolution,[status(thm)],[f32335,f839])).
% 20.83/13.13 fof(f32337,plain,(
% 20.83/13.13 ~sQ1523_spl),
% 20.83/13.13 inference(contradiction_clause,[status(thm)],[f32336])).
% 20.83/13.13 fof(f32440,plain,(
% 20.83/13.13 $false|~sQ623_spl),
% 20.83/13.13 inference(forward_subsumption_resolution,[status(thm)],[f1385,f11451])).
% 20.83/13.13 fof(f32441,plain,(
% 20.83/13.13 ~sQ623_spl),
% 20.83/13.13 inference(contradiction_clause,[status(thm)],[f32440])).
% 20.83/13.13 fof(f32442,plain,(
% 20.83/13.13 ~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)))|~hBOOL(hAPP(hAPP(c_in(tc_List_Olist(tc_Event_Oevent)),v_evs),c_NS__Shared__Mirabelle_Ons__shared))|~sQ106_spl),
% 20.83/13.13 inference(resolution,[status(thm)],[f1388,f4931])).
% 20.83/13.13 fof(f32444,plain,(
% 20.83/13.13 ~sQ1_spl|~sQ4_spl|~sQ106_spl),
% 20.83/13.13 inference(split_clause,[status(thm)],[f32442,f1532,f2596,f4930])).
% 20.83/13.13 fof(f32449,plain,(
% 20.83/13.13 $false),
% 20.83/13.13 inference(sat_refutation,[status(thm)],[f1535,f2602,f4936,f4938,f4956,f6233,f6235,f6945,f6947,f7317,f8007,f10659,f10661,f10663,f14755,f16110,f20228,f20230,f20232,f20341,f20472,f21801,f24683,f24940,f26019,f30108,f30278,f30282,f31149,f32337,f32441,f32444])).
% 20.83/13.13 % SZS output end CNFRefutation for theBenchmark.p
% 20.83/13.16 % Elapsed time: 2.817214 seconds
% 20.83/13.16 % CPU time: 22.076058 seconds
% 20.83/13.16 % Total memory used: 685.040 MB
% 20.83/13.16 % Net memory used: 662.652 MB
%------------------------------------------------------------------------------