%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV732-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 110.97s 14.66s
% Output : CNFRefutation 110.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 73
% Syntax : Number of formulae : 267 ( 82 unt; 36 def)
% Number of atoms : 475 ( 21 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 401 ( 193 ~; 172 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 46 ( 44 usr; 37 prp; 0-4 aty)
% Number of functors : 41 ( 41 usr; 20 con; 0-4 aty)
% Number of variables : 273 ( 273 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f150,axiom,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [T_a] : c_List_Odistinct(c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,axiom,
! [V_x,V_A,T_a] : hBOOL(c_in(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,axiom,
! [V_x,V_xs,T_a] : c_List_Oset(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_Set_Oinsert(V_x,c_List_Oset(V_xs,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f439,axiom,
hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f519,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/sandbox/benchmark/theBenchmark.p') ).
fof(f526,axiom,
! [V_X] : hBOOL(c_in(hAPP(c_Public_OshrK,V_X),c_Message_OsymKeys,tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f581,axiom,
! [V_X,V_H] :
( ~ hBOOL(c_in(V_X,V_H,tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f592,axiom,
~ hBOOL(c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f611,axiom,
hBOOL(c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f647,axiom,
! [V_X,V_B,V_K,V_A,V_evs,V_NA] :
( ~ hBOOL(c_in(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))
| hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f652,axiom,
! [V_A,V_evs] :
( ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,V_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f657,axiom,
! [V_K,V_evs,V_A,V_NA,V_B,V_X] :
( ~ hBOOL(c_in(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))
| hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(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),tc_nat)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f664,axiom,
! [V_X,V_evs,V_A,V_B] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f673,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f674,axiom,
! [V_Y,V_H,V_X] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f675,axiom,
! [V_X,V_H,V_Y] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f682,axiom,
! [V_X,V_H] :
( ~ hBOOL(c_in(V_X,V_H,tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f683,axiom,
! [V_X,V_evs,V_A,V_B] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f686,axiom,
! [T_a,V_x] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f689,axiom,
! [V_X,V_H,V_A] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_A),V_X),c_Message_Oanalz(V_H),tc_Message_Omsg))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,V_A)),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f690,axiom,
! [V_x,T_a] : hBOOL(c_in(V_x,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f691,axiom,
! [V_X,V_evs,V_A,V_B] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f702,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(c_in(V_x,V_S,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f703,axiom,
! [V_S,V_x,T_a] :
( ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f721,negated_conjecture,
hBOOL(c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f722,negated_conjecture,
hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f723,negated_conjecture,
~ hBOOL(c_in(v_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f724,negated_conjecture,
( hBOOL(c_in(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),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/sandbox/benchmark/theBenchmark.p') ).
fof(f725,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f726,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f728,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Obounded__lattice(T_1)
| class_Lattices_Obounded__lattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f729,axiom,
! [T_2,T_1] :
( ~ class_Orderings_Opreorder(T_1)
| class_Orderings_Opreorder(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f730,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Olattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f747,axiom,
class_Lattices_Obounded__lattice(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f748,axiom,
class_Orderings_Opreorder(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f749,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f981,plain,
hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f1014,plain,
! [X0] : c_List_Odistinct(c_List_Olist_ONil(X0),X0),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f1173,plain,
! [X0,X1,X2] : hBOOL(c_in(X0,c_Set_Oinsert(X0,X1,X2),X2)),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f1330,plain,
! [X0,X1,X2] : c_Set_Oinsert(X0,c_List_Oset(X1,X2),X2) = c_List_Oset(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f1402,plain,
hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f1519,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)],[f519]) ).
fof(f1532,plain,
! [X0] : hBOOL(c_in(hAPP(c_Public_OshrK,X0),c_Message_OsymKeys,tc_nat)),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f1605,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X0,X1,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f581]) ).
fof(f1621,plain,
~ hBOOL(c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f1647,plain,
hBOOL(c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent)),
inference(cnf_transformation,[status(thm)],[f611]) ).
fof(f1696,plain,
! [V_X,V_B,V_K,V_A,V_evs] :
( ! [V_NA] : ~ hBOOL(c_in(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))
| hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| V_X = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,V_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Omsg_OAgent(V_A))) ),
inference(miniscoping,[status(thm)],[f647]) ).
fof(f1697,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(c_in(X5,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| hBOOL(c_in(X2,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X1),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X5)),tc_Message_Omsg))
| 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)],[f1696]) ).
fof(f1704,plain,
! [V_evs] :
( ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ! [V_A] :
( ~ hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,V_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ) ),
inference(miniscoping,[status(thm)],[f652]) ).
fof(f1705,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X1,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X1)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(cnf_transformation,[status(thm)],[f1704]) ).
fof(f1713,plain,
! [V_K,V_evs,V_A] :
( ! [V_NA,V_B,V_X] : ~ hBOOL(c_in(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))
| hBOOL(c_in(V_A,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(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),tc_nat)) ),
inference(miniscoping,[status(thm)],[f657]) ).
fof(f1714,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,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_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))
| hBOOL(c_in(X2,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(X0,c_Set_Oimage(c_Public_OshrK,c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Oagent,tc_bool)),tc_Message_Oagent,tc_nat),tc_nat)) ),
inference(cnf_transformation,[status(thm)],[f1713]) ).
fof(f1725,plain,
! [V_X,V_evs] :
( ! [V_A,V_B] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f664]) ).
fof(f1726,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1725]) ).
fof(f1742,plain,
! [X0] : c_Message_Oanalz(c_Message_Oanalz(X0)) = c_Message_Oanalz(X0),
inference(cnf_transformation,[status(thm)],[f673]) ).
fof(f1743,plain,
! [V_Y,V_H] :
( ! [V_X] : ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f674]) ).
fof(f1744,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1743]) ).
fof(f1745,plain,
! [V_X,V_H] :
( ! [V_Y] : ~ hBOOL(c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))
| hBOOL(c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f675]) ).
fof(f1746,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X2),c_Message_Oanalz(X1),tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1745]) ).
fof(f1756,plain,
! [X0,X1] :
( hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f1757,plain,
! [V_X,V_evs] :
( ! [V_A,V_B] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f683]) ).
fof(f1758,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1757]) ).
fof(f1761,plain,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(thm)],[f686]) ).
fof(f1764,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oanalz(X2),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),X1),c_Message_Oanalz(X2),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f689]) ).
fof(f1765,plain,
! [X0,X1] : hBOOL(c_in(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(thm)],[f690]) ).
fof(f1766,plain,
! [V_X,V_evs] :
( ! [V_A,V_B] : ~ hBOOL(c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)) ),
inference(miniscoping,[status(thm)],[f691]) ).
fof(f1767,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)) ),
inference(cnf_transformation,[status(thm)],[f1766]) ).
fof(f1778,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : hBOOL(c_in(V_x,V_S,T_a)) ),
inference(miniscoping,[status(thm)],[f702]) ).
fof(f1779,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X1,X0))
| hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f1778]) ).
fof(f1780,plain,
! [V_S,V_x] :
( ! [T_a] : ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f703]) ).
fof(f1781,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X1,X0))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f1780]) ).
fof(f1807,plain,
hBOOL(c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f721]) ).
fof(f1808,plain,
hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
inference(cnf_transformation,[status(thm)],[f722]) ).
fof(f1809,plain,
~ hBOOL(c_in(v_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f1810,plain,
( hBOOL(c_in(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),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)],[f724]) ).
fof(f1811,plain,
! [T_1] :
( ~ class_Lattices_Olattice(T_1)
| ! [T_2] : class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f725]) ).
fof(f1812,plain,
! [X0,X1] :
( ~ class_Lattices_Olattice(X1)
| class_Lattices_Oupper__semilattice(tc_fun(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1811]) ).
fof(f1813,plain,
! [T_1] :
( ~ class_Lattices_Olattice(T_1)
| ! [T_2] : class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f726]) ).
fof(f1814,plain,
! [X0,X1] :
( class_Lattices_Olower__semilattice(tc_fun(X1,X0))
| ~ class_Lattices_Olattice(X0) ),
inference(cnf_transformation,[status(thm)],[f1813]) ).
fof(f1817,plain,
! [T_1] :
( ~ class_Lattices_Obounded__lattice(T_1)
| ! [T_2] : class_Lattices_Obounded__lattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f728]) ).
fof(f1818,plain,
! [X0,X1] :
( ~ class_Lattices_Obounded__lattice(X1)
| class_Lattices_Obounded__lattice(tc_fun(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1817]) ).
fof(f1819,plain,
! [T_1] :
( ~ class_Orderings_Opreorder(T_1)
| ! [T_2] : class_Orderings_Opreorder(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f729]) ).
fof(f1820,plain,
! [X0,X1] :
( class_Orderings_Opreorder(tc_fun(X1,X0))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1819]) ).
fof(f1821,plain,
! [T_1] :
( ~ class_Lattices_Olattice(T_1)
| ! [T_2] : class_Lattices_Olattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f730]) ).
fof(f1822,plain,
! [X0,X1] :
( class_Lattices_Olattice(tc_fun(X1,X0))
| ~ class_Lattices_Olattice(X0) ),
inference(cnf_transformation,[status(thm)],[f1821]) ).
fof(f1843,plain,
class_Lattices_Obounded__lattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f747]) ).
fof(f1844,plain,
class_Orderings_Opreorder(tc_bool),
inference(cnf_transformation,[status(thm)],[f748]) ).
fof(f1845,plain,
class_Lattices_Olattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f749]) ).
fof(f1860,definition,
( sQ2_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,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1863,definition,
( sQ3_spl
<=> hBOOL(c_in(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),tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1866,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1810,f1860,f1863]) ).
fof(f1889,plain,
hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs)),
inference(resolution,[status(thm)],[f1781,f1808]) ).
fof(f1921,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X2),X1,tc_Message_Omsg))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1756,f1746]) ).
fof(f1922,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Oanalz(X1),X0))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1756,f1781]) ).
fof(f1954,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg))
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),X2,tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1744,f1756]) ).
fof(f1973,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1767,f1807]) ).
fof(f1975,plain,
hBOOL(hAPP(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))),
inference(resolution,[status(thm)],[f1973,f1781]) ).
fof(f1985,definition,
( sQ13_spl
<=> class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1987,plain,
( sQ13_spl
| ~ class_Orderings_Opreorder(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f1985]) ).
fof(f2134,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_Message_Oanalz(X1),c_Message_Omsg_OMPair(X2,X0)))
| hBOOL(c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1779,f1744]) ).
fof(f2137,plain,
! [X0,X1,X2] :
( hBOOL(c_in(X1,c_Message_Oanalz(X0),tc_Message_Omsg))
| ~ hBOOL(hAPP(X0,c_Message_Omsg_OMPair(X1,X2))) ),
inference(resolution,[status(thm)],[f1779,f1921]) ).
fof(f2298,plain,
( hBOOL(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1764,f1973]) ).
fof(f2304,definition,
( sQ26_spl
<=> hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f2306,plain,
( sQ26_spl
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f2304]) ).
fof(f2307,definition,
( sQ27_spl
<=> hBOOL(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f2308,plain,
( ~ sQ27_spl
| hBOOL(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f2307]) ).
fof(f2310,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f2298,f2304,f2307]) ).
fof(f2318,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1726,f1807]) ).
fof(f2794,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_Message_Oanalz(c_Message_Oanalz(X0)),X1))
| ~ hBOOL(hAPP(X0,c_Message_Omsg_OMPair(X1,X2))) ),
inference(resolution,[status(thm)],[f2137,f1922]) ).
fof(f2800,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_Message_Oanalz(X0),X1))
| ~ hBOOL(hAPP(X0,c_Message_Omsg_OMPair(X1,X2))) ),
inference(forward_demodulation,[status(thm)],[f1742,f2794]) ).
fof(f2955,definition,
( sQ44_spl
<=> hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f2961,plain,
( ~ sQ27_spl
| hBOOL(c_in(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_Oanalz(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs))),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f2308,f1954]) ).
fof(f2967,plain,
( ~ sQ27_spl
| hBOOL(c_in(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_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(forward_demodulation,[status(thm)],[f1742,f2961]) ).
fof(f2968,plain,
( ~ sQ27_spl
| hBOOL(c_in(c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f2967,f1744]) ).
fof(f2977,plain,
( ~ sQ27_spl
| hBOOL(c_in(v_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f2968,f1744]) ).
fof(f2984,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2977,f1809]) ).
fof(f2985,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f2984]) ).
fof(f3006,definition,
! [X1] :
( sQ46_spl
<=> X1 != X1 ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f3007,plain,
! [X0] :
( ~ sQ46_spl
| X0 != X0 ),
inference(component_clause,[status(thm)],[f3006]) ).
fof(f3185,definition,
! [X1] :
( sQ47_spl
<=> ~ class_Lattices_Oupper__semilattice(tc_fun(X1,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f3186,plain,
! [X0] :
( ~ sQ47_spl
| ~ class_Lattices_Oupper__semilattice(tc_fun(X0,tc_bool)) ),
inference(component_clause,[status(thm)],[f3185]) ).
fof(f3237,plain,
hBOOL(hAPP(c_Event_Obad,c_Message_Oagent_OSpy)),
inference(resolution,[status(thm)],[f1647,f1781]) ).
fof(f3465,plain,
( ~ hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| 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
| hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolution,[status(thm)],[f1697,f2318]) ).
fof(f3469,definition,
( sQ52_spl
<=> hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f3471,plain,
( sQ52_spl
| ~ hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f3469]) ).
fof(f3472,plain,
( ~ sQ52_spl
| sQ2_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f3465,f2955,f1860,f3469]) ).
fof(f3473,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3471,f1808]) ).
fof(f3474,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f3473]) ).
fof(f3509,definition,
( sQ56_spl
<=> hBOOL(c_in(hAPP(c_Public_OshrK,v_B),c_Message_OsymKeys,tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f3511,plain,
( sQ56_spl
| ~ hBOOL(c_in(hAPP(c_Public_OshrK,v_B),c_Message_OsymKeys,tc_nat)) ),
inference(component_clause,[status(thm)],[f3509]) ).
fof(f3534,definition,
( sQ58_spl
<=> hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3536,plain,
( sQ58_spl
| ~ hBOOL(c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f3534]) ).
fof(f3548,definition,
( sQ59_spl
<=> class_Lattices_Oupper__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f3550,plain,
( sQ59_spl
| ~ class_Lattices_Oupper__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f3548]) ).
fof(f3555,plain,
( sQ59_spl
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolution,[status(thm)],[f3550,f1812]) ).
fof(f3556,plain,
( sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3555,f1845]) ).
fof(f3557,plain,
sQ59_spl,
inference(contradiction_clause,[status(thm)],[f3556]) ).
fof(f3626,definition,
( sQ62_spl
<=> v_X = v_X ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f3628,plain,
( sQ62_spl
| v_X != v_X ),
inference(component_clause,[status(thm)],[f3626]) ).
fof(f3684,plain,
( sQ62_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3628]) ).
fof(f3685,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f3684]) ).
fof(f3820,plain,
( sQ13_spl
| ~ class_Orderings_Opreorder(tc_bool) ),
inference(resolution,[status(thm)],[f1987,f1820]) ).
fof(f3821,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3820,f1844]) ).
fof(f3822,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f3821]) ).
fof(f3897,definition,
( sQ67_spl
<=> class_Lattices_Olattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f3899,plain,
( sQ67_spl
| ~ class_Lattices_Olattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f3897]) ).
fof(f3950,plain,
( sQ67_spl
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolution,[status(thm)],[f3899,f1822]) ).
fof(f3951,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3950,f1845]) ).
fof(f3952,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f3951]) ).
fof(f4154,plain,
! [X0,X1,X2] : hBOOL(c_in(X0,c_List_Oset(c_List_Olist_OCons(X0,X1,X2),X2),X2)),
inference(paramodulation,[status(thm)],[f1330,f1173]) ).
fof(f5043,definition,
! [X1] :
( sQ79_spl
<=> ~ class_Lattices_Obounded__lattice(tc_fun(X1,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f5044,plain,
! [X0] :
( ~ sQ79_spl
| ~ class_Lattices_Obounded__lattice(tc_fun(X0,tc_bool)) ),
inference(component_clause,[status(thm)],[f5043]) ).
fof(f5047,plain,
( ~ sQ79_spl
| ~ class_Lattices_Obounded__lattice(tc_bool) ),
inference(resolution,[status(thm)],[f5044,f1818]) ).
fof(f5048,plain,
( ~ sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5047,f1843]) ).
fof(f5049,plain,
~ sQ79_spl,
inference(contradiction_clause,[status(thm)],[f5048]) ).
fof(f5431,plain,
hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1758,f1807]) ).
fof(f6030,definition,
( sQ99_spl
<=> hBOOL(c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f6031,plain,
( ~ sQ99_spl
| hBOOL(c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)) ),
inference(component_clause,[status(thm)],[f6030]) ).
fof(f6092,definition,
( sQ105_spl
<=> v_K = v_K ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f6094,plain,
( sQ105_spl
| v_K != v_K ),
inference(component_clause,[status(thm)],[f6092]) ).
fof(f6096,plain,
( sQ105_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6094]) ).
fof(f6097,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f6096]) ).
fof(f6852,definition,
( sQ123_spl
<=> hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f6854,plain,
( sQ123_spl
| ~ hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs)) ),
inference(component_clause,[status(thm)],[f6852]) ).
fof(f6859,definition,
( sQ125_spl
<=> hBOOL(hAPP(c_Event_Obad,c_Message_Oagent_OSpy)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f6861,plain,
( sQ125_spl
| ~ hBOOL(hAPP(c_Event_Obad,c_Message_Oagent_OSpy)) ),
inference(component_clause,[status(thm)],[f6859]) ).
fof(f6863,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6861,f3237]) ).
fof(f6864,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f6863]) ).
fof(f6865,plain,
( sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6854,f1889]) ).
fof(f6866,plain,
sQ123_spl,
inference(contradiction_clause,[status(thm)],[f6865]) ).
fof(f6907,definition,
( sQ127_spl
<=> c_Public_OshrK = c_Public_OshrK ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f6909,plain,
( sQ127_spl
| c_Public_OshrK != c_Public_OshrK ),
inference(component_clause,[status(thm)],[f6907]) ).
fof(f6911,plain,
( sQ127_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6909]) ).
fof(f6912,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f6911]) ).
fof(f6939,plain,
( sQ56_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3511,f1532]) ).
fof(f6941,plain,
! [X0] : hBOOL(hAPP(c_Message_OsymKeys,hAPP(c_Public_OshrK,X0))),
inference(resolution,[status(thm)],[f1532,f1781]) ).
fof(f6943,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f6939]) ).
fof(f7124,plain,
( sQ26_spl
| ~ hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolution,[status(thm)],[f1705,f2306]) ).
fof(f7133,plain,
( sQ26_spl
| ~ sQ52_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f7124,f2955,f3469,f2304]) ).
fof(f7142,plain,
( ~ sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6031,f1621]) ).
fof(f7143,plain,
~ sQ99_spl,
inference(contradiction_clause,[status(thm)],[f7142]) ).
fof(f7144,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3536,f1402]) ).
fof(f7145,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f7144]) ).
fof(f7211,definition,
! [X0] :
( sQ141_spl
<=> ~ hBOOL(hAPP(c_Message_OsymKeys,hAPP(c_Public_OshrK,X0))) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f7212,plain,
! [X0] :
( ~ sQ141_spl
| ~ hBOOL(hAPP(c_Message_OsymKeys,hAPP(c_Public_OshrK,X0))) ),
inference(component_clause,[status(thm)],[f7211]) ).
fof(f7215,plain,
( ~ sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7212,f6941]) ).
fof(f7216,plain,
~ sQ141_spl,
inference(contradiction_clause,[status(thm)],[f7215]) ).
fof(f7361,definition,
( sQ145_spl
<=> class_Lattices_Obounded__lattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f7363,plain,
( sQ145_spl
| ~ class_Lattices_Obounded__lattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f7361]) ).
fof(f7368,plain,
( sQ145_spl
| ~ class_Lattices_Obounded__lattice(tc_bool) ),
inference(resolution,[status(thm)],[f7363,f1818]) ).
fof(f7369,plain,
( sQ145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7368,f1843]) ).
fof(f7370,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f7369]) ).
fof(f7440,definition,
( sQ146_spl
<=> class_Lattices_Olower__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f7442,plain,
( sQ146_spl
| ~ class_Lattices_Olower__semilattice(tc_fun(tc_Message_Omsg,tc_bool)) ),
inference(component_clause,[status(thm)],[f7440]) ).
fof(f7511,plain,
( sQ146_spl
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolution,[status(thm)],[f7442,f1814]) ).
fof(f7512,plain,
( sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7511,f1845]) ).
fof(f7513,plain,
sQ146_spl,
inference(contradiction_clause,[status(thm)],[f7512]) ).
fof(f7752,definition,
( sQ150_spl
<=> c_Message_OinvKey = c_Message_OinvKey ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f7754,plain,
( sQ150_spl
| c_Message_OinvKey != c_Message_OinvKey ),
inference(component_clause,[status(thm)],[f7752]) ).
fof(f7756,plain,
( sQ150_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7754]) ).
fof(f7757,plain,
sQ150_spl,
inference(contradiction_clause,[status(thm)],[f7756]) ).
fof(f7938,definition,
( sQ153_spl
<=> hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f7940,plain,
( sQ153_spl
| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f7938]) ).
fof(f7945,definition,
( sQ155_spl
<=> hBOOL(hAPP(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f7947,plain,
( sQ155_spl
| ~ hBOOL(hAPP(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),v_X)))))) ),
inference(component_clause,[status(thm)],[f7945]) ).
fof(f7950,plain,
( sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7947,f1975]) ).
fof(f7951,plain,
sQ155_spl,
inference(contradiction_clause,[status(thm)],[f7950]) ).
fof(f7955,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7940,f5431]) ).
fof(f7956,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f7955]) ).
fof(f9027,definition,
! [X1,X2,X3] :
( sQ170_spl
<=> ~ c_Fun_Oinj__on(X1,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)),X2,X3) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f9028,plain,
! [X0,X1,X2] :
( ~ sQ170_spl
| ~ c_Fun_Oinj__on(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2) ),
inference(component_clause,[status(thm)],[f9027]) ).
fof(f9031,plain,
( ~ sQ170_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1519,f9028]) ).
fof(f9032,plain,
~ sQ170_spl,
inference(contradiction_clause,[status(thm)],[f9031]) ).
fof(f9992,definition,
! [X1,X2] :
( sQ182_spl
<=> ~ hBOOL(c_in(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X1,X2),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f9993,plain,
! [X0,X1] :
( ~ sQ182_spl
| ~ hBOOL(c_in(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f9992]) ).
fof(f9996,plain,
( ~ sQ182_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9993,f1765]) ).
fof(f9997,plain,
~ sQ182_spl,
inference(contradiction_clause,[status(thm)],[f9996]) ).
fof(f10070,definition,
! [X1,X2,X3] :
( sQ183_spl
<=> ~ hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),c_Message_Omsg_OMPair(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X1,X2),X3))) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f10071,plain,
! [X0,X1,X2] :
( ~ sQ183_spl
| ~ hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)),c_Message_Omsg_OMPair(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),X2))) ),
inference(component_clause,[status(thm)],[f10070]) ).
fof(f10074,plain,
( ~ sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10071,f1761]) ).
fof(f10075,plain,
~ sQ183_spl,
inference(contradiction_clause,[status(thm)],[f10074]) ).
fof(f11644,definition,
! [X0,X1,X2] :
( sQ217_spl
<=> ~ hBOOL(c_in(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),c_List_Oset(X2,tc_Message_Omsg),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f11645,plain,
! [X0,X1,X2] :
( ~ sQ217_spl
| ~ hBOOL(c_in(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),c_List_Oset(X2,tc_Message_Omsg),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f11644]) ).
fof(f11669,plain,
( ~ sQ217_spl
| $false ),
inference(resolution,[status(thm)],[f11645,f4154]) ).
fof(f11673,plain,
~ sQ217_spl,
inference(contradiction_clause,[status(thm)],[f11669]) ).
fof(f11733,definition,
! [X0,X1,X2,X3] :
( sQ226_spl
<=> ~ hBOOL(c_in(c_Message_Omsg_OMPair(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),X2),c_List_Oset(X3,tc_Message_Omsg),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f11734,plain,
! [X0,X1,X2,X3] :
( ~ sQ226_spl
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X0,X1),X2),c_List_Oset(X3,tc_Message_Omsg),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f11733]) ).
fof(f11742,plain,
( ~ sQ226_spl
| $false ),
inference(resolution,[status(thm)],[f11734,f4154]) ).
fof(f11746,plain,
~ sQ226_spl,
inference(contradiction_clause,[status(thm)],[f11742]) ).
fof(f11810,definition,
! [X0,X1,X2,X3] :
( sQ227_spl
<=> ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X1,X2)),c_List_Oset(X3,tc_Message_Omsg),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f11811,plain,
! [X0,X1,X2,X3] :
( ~ sQ227_spl
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,c_ATP__Linkup_Osko__Set__XrangeE__1__1(v_K,c_Public_OshrK,X1,X2)),c_List_Oset(X3,tc_Message_Omsg),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f11810]) ).
fof(f11822,plain,
( ~ sQ227_spl
| $false ),
inference(resolution,[status(thm)],[f11811,f4154]) ).
fof(f11827,plain,
~ sQ227_spl,
inference(contradiction_clause,[status(thm)],[f11822]) ).
fof(f12288,plain,
! [X0,X1] :
( ~ hBOOL(c_in(X1,X0,tc_Message_Omsg))
| hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(X0)),X1)) ),
inference(resolution,[status(thm)],[f1605,f1922]) ).
fof(f12290,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Message_Osynth(X1),X0))
| ~ hBOOL(c_in(X0,X1,tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1605,f1781]) ).
fof(f12382,plain,
! [X0] : hBOOL(hAPP(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool))),X0)),
inference(resolution,[status(thm)],[f12290,f1765]) ).
fof(f12390,plain,
! [X0] : hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))),X0)),
inference(resolution,[status(thm)],[f12382,f2800]) ).
fof(f12415,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(c_Message_Oanalz(c_Message_Oanalz(c_Message_Osynth(X2))),X0))
| ~ hBOOL(c_in(c_Message_Omsg_OMPair(X0,X1),X2,tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f12288,f2800]) ).
fof(f12419,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(c_Message_Omsg_OMPair(X1,X2),X0,tc_Message_Omsg))
| hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(X0)),X1)) ),
inference(forward_demodulation,[status(thm)],[f1742,f12415]) ).
fof(f12639,plain,
! [X0] : hBOOL(c_in(X0,c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f2134,f12390]) ).
fof(f12701,plain,
! [X0] : hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))))),X0)),
inference(resolution,[status(thm)],[f12639,f12419]) ).
fof(f12710,definition,
! [X0] :
( sQ251_spl
<=> ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f12711,plain,
! [X0] :
( ~ sQ251_spl
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f12710]) ).
fof(f12726,plain,
( ~ sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12711,f12639]) ).
fof(f12727,plain,
~ sQ251_spl,
inference(contradiction_clause,[status(thm)],[f12726]) ).
fof(f12937,plain,
! [X0] : hBOOL(c_in(X0,c_Message_Oanalz(c_Message_Osynth(c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))))),tc_Message_Omsg)),
inference(resolution,[status(thm)],[f12701,f2134]) ).
fof(f13598,definition,
! [X0] :
( sQ255_spl
<=> ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oanalz(c_Message_Osynth(c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))))),tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f13599,plain,
! [X0] :
( ~ sQ255_spl
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oanalz(c_Message_Osynth(c_Message_Oanalz(c_Message_Osynth(c_Orderings_Otop__class_Otop(tc_fun(tc_Message_Omsg,tc_bool)))))),tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f13598]) ).
fof(f13615,plain,
( ~ sQ255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13599,f12937]) ).
fof(f13616,plain,
~ sQ255_spl,
inference(contradiction_clause,[status(thm)],[f13615]) ).
fof(f14709,definition,
( sQ261_spl
<=> hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f14711,plain,
( sQ261_spl
| ~ hBOOL(c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))) ),
inference(component_clause,[status(thm)],[f14709]) ).
fof(f14716,plain,
( sQ261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14711,f981]) ).
fof(f14717,plain,
sQ261_spl,
inference(contradiction_clause,[status(thm)],[f14716]) ).
fof(f16748,definition,
( sQ312_spl
<=> c_List_Odistinct(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f16750,plain,
( sQ312_spl
| ~ c_List_Odistinct(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent) ),
inference(component_clause,[status(thm)],[f16748]) ).
fof(f16791,plain,
( ~ sQ46_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3007]) ).
fof(f16792,plain,
~ sQ46_spl,
inference(contradiction_clause,[status(thm)],[f16791]) ).
fof(f16793,plain,
( sQ312_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16750,f1014]) ).
fof(f16794,plain,
sQ312_spl,
inference(contradiction_clause,[status(thm)],[f16793]) ).
fof(f16836,plain,
( ~ sQ47_spl
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolution,[status(thm)],[f3186,f1812]) ).
fof(f16837,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16836,f1845]) ).
fof(f16838,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f16837]) ).
fof(f16937,plain,
( hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(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),tc_nat)) ),
inference(resolution,[status(thm)],[f1714,f2318]) ).
fof(f16958,plain,
( sQ44_spl
| ~ sQ52_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f16937,f1863,f3469,f2955]) ).
fof(f16959,plain,
$false,
inference(sat_refutation,[status(thm)],[f1866,f2310,f2985,f3472,f3474,f3557,f3685,f3822,f3952,f5049,f6097,f6864,f6866,f6912,f6943,f7133,f7143,f7145,f7216,f7370,f7513,f7757,f7951,f7956,f9032,f9997,f10075,f11673,f11746,f11827,f12727,f13616,f14717,f16792,f16794,f16838,f16958]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV732-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n006.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.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 09:22:27 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.28/0.58 % Drodi V4.1.1
% 110.97/14.66 % Refutation found
% 110.97/14.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 110.97/14.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.88/18.08 % Elapsed time: 17.615700 seconds
% 6.88/18.08 % CPU time: 115.670428 seconds
% 6.88/18.08 % Total memory used: 846.831 MB
% 6.88/18.08 % Net memory used: 801.473 MB
%------------------------------------------------------------------------------