%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:53:12 PM UTC 2026
% Result : Unsatisfiable 47.27s 6.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:26:28 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.45 % Drodi V4.1.1
% 47.27/6.50 % Refutation found
% 47.27/6.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 47.27/6.50 % SZS output start CNFRefutation for theBenchmark
% 47.27/6.50 fof(f10,axiom,(
% 47.27/6.50 (![V_c,V_A,V_B,T_a]: (( c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| ~ c_in(V_c,V_B,T_a) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f20,axiom,(
% 47.27/6.50 (![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)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f60,axiom,(
% 47.27/6.50 (![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)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f65,axiom,(
% 47.27/6.50 (![V_A,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = V_A ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f72,axiom,(
% 47.27/6.50 (![V_A,V_B,T_a]: (( c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f113,axiom,(
% 47.27/6.50 (![T_a,V_a,V_A]: (c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f116,axiom,(
% 47.27/6.50 (![V_P,V_xs,T_a]: (c_List_Oappend(c_List_OtakeWhile(V_P,V_xs,T_a),c_List_OdropWhile(V_P,V_xs,T_a),T_a) = V_xs ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f117,axiom,(
% 47.27/6.50 (![V_a,V_b,T_a,V_c,V_d]: (( c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a) != c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)| V_b = V_c| V_b = V_d ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f122,axiom,(
% 47.27/6.50 (![T_a,V_a_H,V_list_H]: (c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f132,axiom,(
% 47.27/6.50 (![T_a,V_x]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f137,axiom,(
% 47.27/6.50 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f152,axiom,(
% 47.27/6.50 (![V_P,V_xs,T_a,V_y,V_ys]: (( c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a)| ~ hBOOL(hAPP(V_P,V_y)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f167,axiom,(
% 47.27/6.50 (![V_ys,T_a]: (V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f189,axiom,(
% 47.27/6.50 (![T_a]: (c_List_Oset(c_List_Olist_ONil(T_a),T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f210,axiom,(
% 47.27/6.50 (![V_x,V_A,T_a]: (hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f302,axiom,(
% 47.27/6.50 (![V_X,V_K,V_C,V_A]: (c_Set_Oinsert(c_Message_Omsg_OCrypt(V_X,V_K),c_Set_Oinsert(c_Message_Omsg_OAgent(V_C),V_A,tc_Message_Omsg),tc_Message_Omsg) = c_Set_Oinsert(c_Message_Omsg_OAgent(V_C),c_Set_Oinsert(c_Message_Omsg_OCrypt(V_X,V_K),V_A,tc_Message_Omsg),tc_Message_Omsg) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f352,axiom,(
% 47.27/6.50 (![V_a,V_A,T_a]: (( c_Set_Oinsert(V_a,V_A,T_a) = V_A| ~ c_in(V_a,V_A,T_a) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f385,axiom,(
% 47.27/6.50 (![V_H]: (c_lessequals(V_H,c_Message_Oanalz(V_H),tc_fun(tc_Message_Omsg,tc_bool)) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f398,axiom,(
% 47.27/6.50 (![V_P,T_a]: (c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f399,axiom,(
% 47.27/6.50 (![V_P,V_xs,T_a]: (( c_List_OtakeWhile(V_P,V_xs,T_a) = V_xs| ~ hBOOL(hAPP(V_P,c_List_Osko__List__XtakeWhile__eq__all__conv__1__1(V_P,V_xs,T_a))) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f401,axiom,(
% 47.27/6.50 (![V_P,V_x,T_a,V_Q]: (( c_List_OtakeWhile(V_P,V_x,T_a) = c_List_OtakeWhile(V_Q,V_x,T_a)| hBOOL(hAPP(V_Q,c_List_Osko__List__XtakeWhile__cong__1__1(V_P,V_Q,V_x,T_a)))| hBOOL(hAPP(V_P,c_List_Osko__List__XtakeWhile__cong__1__1(V_P,V_Q,V_x,T_a))) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f414,axiom,(
% 47.27/6.50 (![V_P,V_xs,V_x,V_l,T_a]: (( c_List_OtakeWhile(V_P,c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,V_l,T_a),T_a),T_a) = c_List_OtakeWhile(V_P,V_xs,T_a)| hBOOL(hAPP(V_P,V_x)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f420,axiom,(
% 47.27/6.50 c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f444,axiom,(
% 47.27/6.50 (![V_P,V_x,T_a,V_Q]: (( c_List_OtakeWhile(V_P,V_x,T_a) = c_List_OtakeWhile(V_Q,V_x,T_a)| c_in(c_List_Osko__List__XtakeWhile__cong__1__1(V_P,V_Q,V_x,T_a),c_List_Oset(V_x,T_a),T_a) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f522,axiom,(
% 47.27/6.50 (![V_Y,V_H,V_X]: (( c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)| ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f530,axiom,(
% 47.27/6.50 (![V_nat_H,V_nat]: (hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_ONonce(V_nat) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f534,axiom,(
% 47.27/6.50 (![V_X,V_H]: (( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)| ~ c_in(V_X,V_H,tc_Message_Omsg) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f535,axiom,(
% 47.27/6.50 (![V_X,V_H]: (( c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)| ~ c_in(V_X,V_H,tc_Message_Omsg) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f536,axiom,(
% 47.27/6.50 (![V_X,V_evs,V_A,V_B]: (( c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f553,axiom,(
% 47.27/6.50 (![V_A,V_evs]: (( c_in(V_A,c_Event_Obad,tc_Message_Oagent)| ~ c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,V_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f561,axiom,(
% 47.27/6.50 (![V_X,V_B,V_K,V_A,V_evs,V_NA]: (( 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)))| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))| c_in(V_A,c_Event_Obad,tc_Message_Oagent)| ~ 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) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f569,axiom,(
% 47.27/6.50 (![V_agent,V_nat_H,V_msg_H]: (c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f579,axiom,(
% 47.27/6.50 (![V_x,V_S,T_a]: (( c_in(V_x,V_S,T_a)| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f585,axiom,(
% 47.27/6.50 (![V_nat,V_msg,V_nat_H,V_msg_H]: (( c_Message_Omsg_OCrypt(V_nat,V_msg) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H)| V_msg = V_msg_H ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f589,axiom,(
% 47.27/6.50 (![V_msg1,V_msg2,V_msg1_H,V_msg2_H]: (( c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H)| V_msg1 = V_msg1_H ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f598,axiom,(
% 47.27/6.50 ~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f603,axiom,(
% 47.27/6.50 (![V_P,V_x,V_xs,T_a]: (( hBOOL(hAPP(V_P,V_x))| ~ c_in(V_x,c_List_Oset(c_List_OtakeWhile(V_P,V_xs,T_a),T_a),T_a) ) ))),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f607,negated_conjecture,(
% 47.27/6.50 ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f609,negated_conjecture,(
% 47.27/6.50 c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f611,negated_conjecture,(
% 47.27/6.50 c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f613,negated_conjecture,(
% 47.27/6.50 ~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f614,negated_conjecture,(
% 47.27/6.50 v_A = v_Aa ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f615,negated_conjecture,(
% 47.27/6.50 v_B = v_Ba ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f616,negated_conjecture,(
% 47.27/6.50 c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) = v_X ),
% 47.27/6.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 47.27/6.50 fof(f657,plain,(
% 47.27/6.50 ![V_c,V_B,T_a]: ((![V_A]: c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))|~c_in(V_c,V_B,T_a))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f10])).
% 47.27/6.50 fof(f658,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_in(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X3)|~c_in(X0,X2,X3))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f657])).
% 47.27/6.50 fof(f673,plain,(
% 47.27/6.50 ![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)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f20])).
% 47.27/6.50 fof(f734,plain,(
% 47.27/6.50 ![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)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f60])).
% 47.27/6.50 fof(f735,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3))|~hBOOL(hAPP(X1,X3)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f734])).
% 47.27/6.50 fof(f743,plain,(
% 47.27/6.50 ![X0,X1]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool))=X0)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f65])).
% 47.27/6.50 fof(f751,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool))=X1|~c_lessequals(X0,X1,tc_fun(X2,tc_bool)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f72])).
% 47.27/6.50 fof(f813,plain,(
% 47.27/6.50 ![X0,X1,X2]: (~c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))=c_Set_Oinsert(X1,X2,X0))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f113])).
% 47.27/6.50 fof(f816,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_Oappend(c_List_OtakeWhile(X0,X1,X2),c_List_OdropWhile(X0,X1,X2),X2)=X1)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f116])).
% 47.27/6.50 fof(f817,plain,(
% 47.27/6.50 ![V_b,V_d]: ((![V_c]: ((![V_a,T_a]: ~c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a))|V_b=V_c))|V_b=V_d)),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f117])).
% 47.27/6.50 fof(f818,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (~c_Set_Oinsert(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),X2)=c_Set_Oinsert(X3,c_Set_Oinsert(X4,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),X2)|X1=X3|X1=X4)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f817])).
% 47.27/6.50 fof(f826,plain,(
% 47.27/6.50 ![X0,X1,X2]: (~c_List_Olist_ONil(X0)=c_List_Olist_OCons(X1,X2,X0))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f122])).
% 47.27/6.50 fof(f837,plain,(
% 47.27/6.50 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f132])).
% 47.27/6.50 fof(f845,plain,(
% 47.27/6.50 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f137])).
% 47.27/6.50 fof(f866,plain,(
% 47.27/6.50 ![V_P,V_y]: ((![V_xs,T_a,V_ys]: ~c_List_OdropWhile(V_P,V_xs,T_a)=c_List_Olist_OCons(V_y,V_ys,T_a))|~hBOOL(hAPP(V_P,V_y)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f152])).
% 47.27/6.50 fof(f867,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (~c_List_OdropWhile(X0,X1,X2)=c_List_Olist_OCons(X3,X4,X2)|~hBOOL(hAPP(X0,X3)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f866])).
% 47.27/6.50 fof(f887,plain,(
% 47.27/6.50 ![X0,X1]: (X0=c_List_Oappend(c_List_Olist_ONil(X1),X0,X1))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f167])).
% 47.27/6.50 fof(f919,plain,(
% 47.27/6.50 ![X0]: (c_List_Oset(c_List_Olist_ONil(X0),X0)=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f189])).
% 47.27/6.50 fof(f944,plain,(
% 47.27/6.50 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f210])).
% 47.27/6.50 fof(f1069,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_Set_Oinsert(c_Message_Omsg_OCrypt(X0,X1),c_Set_Oinsert(c_Message_Omsg_OAgent(X2),X3,tc_Message_Omsg),tc_Message_Omsg)=c_Set_Oinsert(c_Message_Omsg_OAgent(X2),c_Set_Oinsert(c_Message_Omsg_OCrypt(X0,X1),X3,tc_Message_Omsg),tc_Message_Omsg))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f302])).
% 47.27/6.50 fof(f1137,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_Set_Oinsert(X0,X1,X2)=X1|~c_in(X0,X1,X2))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f352])).
% 47.27/6.50 fof(f1181,plain,(
% 47.27/6.50 ![X0]: (c_lessequals(X0,c_Message_Oanalz(X0),tc_fun(tc_Message_Omsg,tc_bool)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f385])).
% 47.27/6.50 fof(f1194,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_Olist_ONil(X1))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f398])).
% 47.27/6.50 fof(f1195,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_OtakeWhile(X0,X1,X2)=X1|~hBOOL(hAPP(X0,c_List_Osko__List__XtakeWhile__eq__all__conv__1__1(X0,X1,X2))))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f399])).
% 47.27/6.50 fof(f1197,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|hBOOL(hAPP(X3,c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2)))|hBOOL(hAPP(X0,c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2))))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f401])).
% 47.27/6.50 fof(f1214,plain,(
% 47.27/6.50 ![V_P,V_x]: ((![V_xs,V_l,T_a]: c_List_OtakeWhile(V_P,c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,V_l,T_a),T_a),T_a)=c_List_OtakeWhile(V_P,V_xs,T_a))|hBOOL(hAPP(V_P,V_x)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f414])).
% 47.27/6.50 fof(f1215,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|hBOOL(hAPP(X0,X2)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1214])).
% 47.27/6.50 fof(f1224,plain,(
% 47.27/6.50 c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f420])).
% 47.27/6.50 fof(f1260,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),c_List_Oset(X1,X2),X2))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f444])).
% 47.27/6.50 fof(f1379,plain,(
% 47.27/6.50 ![V_Y,V_H]: (c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg)|(![V_X]: ~c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f522])).
% 47.27/6.50 fof(f1380,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)|~c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oanalz(X1),tc_Message_Omsg))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1379])).
% 47.27/6.50 fof(f1392,plain,(
% 47.27/6.50 ![X0,X1]: (~hAPP(c_Message_Omsg_OKey,X0)=c_Message_Omsg_ONonce(X1))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f530])).
% 47.27/6.50 fof(f1399,plain,(
% 47.27/6.50 ![X0,X1]: (c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)|~c_in(X0,X1,tc_Message_Omsg))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f534])).
% 47.27/6.50 fof(f1400,plain,(
% 47.27/6.50 ![X0,X1]: (c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)|~c_in(X0,X1,tc_Message_Omsg))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f535])).
% 47.27/6.50 fof(f1401,plain,(
% 47.27/6.50 ![V_X,V_evs]: (c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)|(![V_A,V_B]: ~c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f536])).
% 47.27/6.50 fof(f1402,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)|~c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1401])).
% 47.27/6.50 fof(f1426,plain,(
% 47.27/6.50 ![V_evs]: ((![V_A]: (c_in(V_A,c_Event_Obad,tc_Message_Oagent)|~c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,V_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)))|~c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f553])).
% 47.27/6.50 fof(f1427,plain,(
% 47.27/6.50 ![X0,X1]: (c_in(X0,c_Event_Obad,tc_Message_Oagent)|~c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)|~c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1426])).
% 47.27/6.50 fof(f1440,plain,(
% 47.27/6.50 ![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)))|~c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))|c_in(V_A,c_Event_Obad,tc_Message_Oagent))|(![V_NA]: ~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)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f561])).
% 47.27/6.50 fof(f1441,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (X0=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3)))|~c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(X3,c_Event_Obad,tc_Message_Oagent)|~c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1440])).
% 47.27/6.50 fof(f1451,plain,(
% 47.27/6.50 ![X0,X1,X2]: (~c_Message_Omsg_OAgent(X0)=c_Message_Omsg_OCrypt(X1,X2))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f569])).
% 47.27/6.50 fof(f1463,plain,(
% 47.27/6.50 ![V_x,V_S]: ((![T_a]: c_in(V_x,V_S,T_a))|~hBOOL(hAPP(V_S,V_x)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f579])).
% 47.27/6.50 fof(f1464,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_in(X0,X1,X2)|~hBOOL(hAPP(X1,X0)))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1463])).
% 47.27/6.50 fof(f1472,plain,(
% 47.27/6.50 ![V_msg,V_msg_H]: ((![V_nat,V_nat_H]: ~c_Message_Omsg_OCrypt(V_nat,V_msg)=c_Message_Omsg_OCrypt(V_nat_H,V_msg_H))|V_msg=V_msg_H)),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f585])).
% 47.27/6.50 fof(f1473,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (~c_Message_Omsg_OCrypt(X0,X1)=c_Message_Omsg_OCrypt(X2,X3)|X1=X3)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1472])).
% 47.27/6.50 fof(f1478,plain,(
% 47.27/6.50 ![V_msg1,V_msg1_H]: ((![V_msg2,V_msg2_H]: ~c_Message_Omsg_OMPair(V_msg1,V_msg2)=c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H))|V_msg1=V_msg1_H)),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f589])).
% 47.27/6.50 fof(f1479,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (~c_Message_Omsg_OMPair(X0,X1)=c_Message_Omsg_OMPair(X2,X3)|X0=X2)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1478])).
% 47.27/6.50 fof(f1491,plain,(
% 47.27/6.50 ~c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f598])).
% 47.27/6.50 fof(f1497,plain,(
% 47.27/6.50 ![V_P,V_x]: (hBOOL(hAPP(V_P,V_x))|(![V_xs,T_a]: ~c_in(V_x,c_List_Oset(c_List_OtakeWhile(V_P,V_xs,T_a),T_a),T_a)))),
% 47.27/6.50 inference(miniscoping,[status(thm)],[f603])).
% 47.27/6.50 fof(f1498,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|~c_in(X1,c_List_Oset(c_List_OtakeWhile(X0,X2,X3),X3),X3))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f1497])).
% 47.27/6.50 fof(f1502,plain,(
% 47.27/6.50 ~c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f607])).
% 47.27/6.50 fof(f1504,plain,(
% 47.27/6.50 c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f609])).
% 47.27/6.50 fof(f1506,plain,(
% 47.27/6.50 c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f611])).
% 47.27/6.50 fof(f1508,plain,(
% 47.27/6.50 ~c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f613])).
% 47.27/6.50 fof(f1509,plain,(
% 47.27/6.50 v_A=v_Aa),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f614])).
% 47.27/6.50 fof(f1510,plain,(
% 47.27/6.50 v_B=v_Ba),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f615])).
% 47.27/6.50 fof(f1511,plain,(
% 47.27/6.50 c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))=v_X),
% 47.27/6.50 inference(cnf_transformation,[status(thm)],[f616])).
% 47.27/6.50 fof(f1562,plain,(
% 47.27/6.50 ![X0]: (~c_Message_Omsg_OAgent(X0)=v_X)),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f1511,f1451])).
% 47.27/6.50 fof(f1619,plain,(
% 47.27/6.50 c_in(c_Event_Oevent_OSays(v_S,v_Aa,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_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 47.27/6.50 inference(backward_demodulation,[status(thm)],[f1509,f1506])).
% 47.27/6.50 fof(f1621,plain,(
% 47.27/6.50 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_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f1509,f1619])).
% 47.27/6.50 fof(f1701,plain,(
% 47.27/6.50 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_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f1510,f1621])).
% 47.27/6.50 fof(f1774,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|c_in(X2,X0,X5))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1215,f1464])).
% 47.27/6.50 fof(f1834,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|c_Set_Oinsert(X2,X0,X5)=X0)),
% 47.27/6.50 inference(resolution,[status(thm)],[f1774,f1137])).
% 47.27/6.50 fof(f2357,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),c_Lattices_Oupper__semilattice__class_Osup(X4,c_List_Oset(X1,X2),tc_fun(X2,tc_bool)),X2))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1260,f658])).
% 47.27/6.50 fof(f3046,plain,(
% 47.27/6.50 ![X0,X1]: (c_Set_Oinsert(v_X,c_Set_Oinsert(c_Message_Omsg_OAgent(X0),X1,tc_Message_Omsg),tc_Message_Omsg)=c_Set_Oinsert(c_Message_Omsg_OAgent(X0),c_Set_Oinsert(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),X1,tc_Message_Omsg),tc_Message_Omsg))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f1511,f1069])).
% 47.27/6.50 fof(f3076,plain,(
% 47.27/6.50 ![X0,X1]: (c_Set_Oinsert(v_X,c_Set_Oinsert(c_Message_Omsg_OAgent(X0),X1,tc_Message_Omsg),tc_Message_Omsg)=c_Set_Oinsert(c_Message_Omsg_OAgent(X0),c_Set_Oinsert(v_X,X1,tc_Message_Omsg),tc_Message_Omsg))),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f1511,f3046])).
% 47.27/6.50 fof(f3188,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|hBOOL(hAPP(X0,c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2)))|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X3,X4))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1197,f1464])).
% 47.27/6.50 fof(f3527,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X3,X4)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X0,X5))),
% 47.27/6.50 inference(resolution,[status(thm)],[f3188,f1464])).
% 47.27/6.50 fof(f3580,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X0,X4)|c_Set_Oinsert(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X3,X5)=X3)),
% 47.27/6.50 inference(resolution,[status(thm)],[f3527,f1137])).
% 47.27/6.50 fof(f3645,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(X3,X1,X2)|c_Set_Oinsert(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X3,X4)=X3|c_Set_Oinsert(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X3,X1,X2),X0,X5)=X0)),
% 47.27/6.50 inference(resolution,[status(thm)],[f3580,f1137])).
% 47.27/6.50 fof(f5095,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5,X6]: (hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3))|c_List_OtakeWhile(X1,c_List_Oappend(X4,c_List_Olist_OCons(X3,X5,X6),X6),X6)=c_List_OtakeWhile(X1,X4,X6))),
% 47.27/6.50 inference(resolution,[status(thm)],[f735,f1215])).
% 47.27/6.50 fof(f5358,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|c_in(X2,c_Lattices_Oupper__semilattice__class_Osup(X5,X0,tc_fun(X6,tc_bool)),X7))),
% 47.27/6.50 inference(resolution,[status(thm)],[f5095,f1464])).
% 47.27/6.50 fof(f5394,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|c_in(X2,c_Lattices_Oupper__semilattice__class_Osup(X0,X5,tc_fun(X6,tc_bool)),X7))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f673,f5358])).
% 47.27/6.50 fof(f5950,plain,(
% 47.27/6.50 ![X0]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Message_Oanalz(X0),tc_fun(tc_Message_Omsg,tc_bool))=c_Message_Oanalz(X0))),
% 47.27/6.50 inference(resolution,[status(thm)],[f751,f1181])).
% 47.27/6.50 fof(f6224,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(X0,X1,X4)|c_in(X2,c_Message_Oanalz(X0),X5))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f5950,f5394])).
% 47.27/6.50 fof(f7142,definition,(
% 47.27/6.50 ![X2]: (sQ68_spl <=> (c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X2)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f7143,plain,(
% 47.27/6.50 ![X0]: (c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)|~sQ68_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f7142])).
% 47.27/6.50 fof(f8500,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_OtakeWhile(X2,c_List_Olist_ONil(X1),X1)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X2,c_List_Olist_ONil(X1),X1),c_Lattices_Oupper__semilattice__class_Osup(X3,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)),X1))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f919,f2357])).
% 47.27/6.50 fof(f8505,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_OtakeWhile(X2,c_List_Olist_ONil(X1),X1)|c_in(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X2,c_List_Olist_ONil(X1),X1),X3,X1))),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f743,f8500])).
% 47.27/6.50 fof(f8682,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_OtakeWhile(X2,c_List_Olist_ONil(X1),X1)|c_Set_Oinsert(c_List_Osko__List__XtakeWhile__cong__1__1(X0,X2,c_List_Olist_ONil(X1),X1),X3,X1)=X3)),
% 47.27/6.50 inference(resolution,[status(thm)],[f8505,f1137])).
% 47.27/6.50 fof(f8897,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)|c_List_OtakeWhile(X1,c_List_Oappend(X2,c_List_Olist_OCons(c_Message_Omsg_OMPair(X3,X0),X4,X5),X5),X5)=c_List_OtakeWhile(X1,X2,X5))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1380,f6224])).
% 47.27/6.50 fof(f8932,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Oappend(X0,c_List_Olist_OCons(c_Message_Omsg_OMPair(X1,hAPP(c_Message_Omsg_OKey,v_K)),X2,X3),X3),X3)=c_List_OtakeWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0,X3))),
% 47.27/6.50 inference(resolution,[status(thm)],[f8897,f1508])).
% 47.27/6.50 fof(f8992,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_OtakeWhile(X2,c_List_Olist_ONil(X1),X1))),
% 47.27/6.50 inference(resolution,[status(thm)],[f813,f8682])).
% 47.27/6.50 fof(f8996,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,X4))),
% 47.27/6.50 inference(resolution,[status(thm)],[f813,f1834])).
% 47.27/6.50 fof(f8997,plain,(
% 47.27/6.50 ![X0,X1,X2]: (~c_List_Oset(c_List_Olist_ONil(X0),X0)=c_Set_Oinsert(X1,X2,X0))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f919,f813])).
% 47.27/6.50 fof(f9041,definition,(
% 47.27/6.50 ![X2,X3]: (sQ93_spl <=> (c_Set_Oinsert(c_Message_Omsg_OMPair(X2,hAPP(c_Message_Omsg_OKey,v_K)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X3)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f9042,plain,(
% 47.27/6.50 ![X0,X1]: (c_Set_Oinsert(c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X1)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)|~sQ93_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f9041])).
% 47.27/6.50 fof(f9099,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X0),X0),c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,X4))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f919,f8996])).
% 47.27/6.50 fof(f9226,plain,(
% 47.27/6.50 ![X0]: (v_X=v_X|v_X=c_Message_Omsg_OAgent(X0))),
% 47.27/6.50 inference(resolution,[status(thm)],[f818,f3076])).
% 47.27/6.50 fof(f9251,definition,(
% 47.27/6.50 sQ94_spl <=> (v_X=v_X)),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f9258,definition,(
% 47.27/6.50 ![X0]: (sQ96_spl <=> (v_X=c_Message_Omsg_OAgent(X0)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f9259,plain,(
% 47.27/6.50 ![X0]: (v_X=c_Message_Omsg_OAgent(X0)|~sQ96_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f9258])).
% 47.27/6.50 fof(f9261,plain,(
% 47.27/6.50 sQ94_spl|sQ96_spl),
% 47.27/6.50 inference(split_clause,[status(thm)],[f9226,f9251,f9258])).
% 47.27/6.50 fof(f9263,plain,(
% 47.27/6.50 $false|~sQ96_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f9259,f1562])).
% 47.27/6.50 fof(f9264,plain,(
% 47.27/6.50 ~sQ96_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f9263])).
% 47.27/6.50 fof(f9709,plain,(
% 47.27/6.50 ~c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),tc_Message_Omsg)),
% 47.27/6.50 inference(resolution,[status(thm)],[f1400,f1508])).
% 47.27/6.50 fof(f9935,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(X0,X1,X2)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X3),X3),X1,X2)|c_Set_Oinsert(c_List_Osko__List__XtakeWhile__cong__1__1(X0,c_List_Oset(c_List_Olist_ONil(X3),X3),X1,X2),X0,X4)=X0)),
% 47.27/6.50 inference(resolution,[status(thm)],[f3645,f8997])).
% 47.27/6.50 fof(f9976,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X0),X0),X1,X2)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X3),X3),X1,X2))),
% 47.27/6.50 inference(resolution,[status(thm)],[f9935,f8997])).
% 47.27/6.50 fof(f9977,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,X2)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X3),X3),X1,X2))),
% 47.27/6.50 inference(resolution,[status(thm)],[f9935,f813])).
% 47.27/6.50 fof(f10017,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,X2)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X3),X3),c_List_Oappend(X1,c_List_Olist_OCons(X4,X5,X2),X2),X2))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f9099,f9976])).
% 47.27/6.50 fof(f10796,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4,X5]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Oappend(X1,c_List_Olist_OCons(X2,X3,X4),X4),X4)=c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X5,tc_bool)),X1,X4))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f9099,f9977])).
% 47.27/6.50 fof(f11130,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_OtakeWhile(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1,X2)=X1)),
% 47.27/6.50 inference(resolution,[status(thm)],[f837,f1195])).
% 47.27/6.50 fof(f11728,plain,(
% 47.27/6.50 ![X0,X1]: (~hBOOL(hAPP(c_List_Oset(c_List_Olist_ONil(X0),X0),X1)))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f919,f845])).
% 47.27/6.50 fof(f12118,plain,(
% 47.27/6.50 ![X0]: (c_in(X0,c_Event_Obad,tc_Message_Oagent)|~c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1427,f1504])).
% 47.27/6.50 fof(f12193,plain,(
% 47.27/6.50 ![X0]: (c_in(X0,c_Event_Obad,tc_Message_Oagent)|~c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,X0)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),tc_Message_Omsg))),
% 47.27/6.50 inference(resolution,[status(thm)],[f12118,f1399])).
% 47.27/6.50 fof(f12694,plain,(
% 47.27/6.50 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_Ka),v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 47.27/6.50 inference(resolution,[status(thm)],[f1701,f1402])).
% 47.27/6.50 fof(f12850,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Oappend(c_List_Olist_ONil(X1),c_List_Olist_OCons(X2,X3,X1),X1),X1)=c_List_OtakeWhile(X4,c_List_Olist_ONil(X1),X1))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f8992,f10796])).
% 47.27/6.50 fof(f13263,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (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)))|c_in(X3,c_Event_Obad,tc_Message_Oagent)|~c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1441,f1504])).
% 47.27/6.50 fof(f13670,definition,(
% 47.27/6.50 sQ124_spl <=> (c_in(v_A,c_Event_Obad,tc_Message_Oagent))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f13671,plain,(
% 47.27/6.50 c_in(v_A,c_Event_Obad,tc_Message_Oagent)|~sQ124_spl),
% 47.27/6.50 inference(component_clause,[status(thm)],[f13670])).
% 47.27/6.50 fof(f13678,plain,(
% 47.27/6.50 $false|~sQ124_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f13671,f1502])).
% 47.27/6.50 fof(f13679,plain,(
% 47.27/6.50 ~sQ124_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f13678])).
% 47.27/6.50 fof(f14361,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Olist_OCons(X1,X2,X3),X3)=c_List_OtakeWhile(X4,c_List_Olist_ONil(X3),X3))),
% 47.27/6.50 inference(backward_demodulation,[status(thm)],[f887,f12850])).
% 47.27/6.50 fof(f14366,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_OtakeWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Olist_OCons(c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K)),X1,X2),X2)=c_List_OtakeWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Olist_ONil(X2),X2))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f887,f8932])).
% 47.27/6.50 fof(f14378,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Olist_ONil(X1),X1)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X2),X2),c_List_Olist_OCons(X3,X4,X1),X1))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f887,f10017])).
% 47.27/6.50 fof(f14381,plain,(
% 47.27/6.50 ![X0,X1,X2,X3,X4]: (c_List_OtakeWhile(X0,c_List_Olist_OCons(X1,X2,X3),X3)=c_List_OtakeWhile(X0,c_List_Olist_ONil(X3),X3)|c_Set_Oinsert(X1,X0,X4)=X0)),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f887,f1834])).
% 47.27/6.50 fof(f14540,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Olist_OCons(X1,X2,X3),X3)=c_List_Olist_ONil(X3))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f11130,f14361])).
% 47.27/6.50 fof(f14666,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Olist_OCons(X1,X2,X3),X3)=c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),c_List_Olist_ONil(X3),X3))),
% 47.27/6.50 inference(resolution,[status(thm)],[f14381,f813])).
% 47.27/6.50 fof(f14711,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_Olist_ONil(X0)=c_List_OtakeWhile(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),c_List_Olist_ONil(X0),X0))),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f14540,f14666])).
% 47.27/6.50 fof(f14759,plain,(
% 47.27/6.50 ![X0,X1]: (~v_X=c_Message_Omsg_OCrypt(X0,X1)|c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))=X1)),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f1511,f1473])).
% 47.27/6.50 fof(f15059,definition,(
% 47.27/6.50 sQ145_spl <=> (v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f15060,plain,(
% 47.27/6.50 v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A)))|~sQ145_spl),
% 47.27/6.50 inference(component_clause,[status(thm)],[f15059])).
% 47.27/6.50 fof(f15336,plain,(
% 47.27/6.50 ~v_X=v_X|c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))=c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))|~sQ145_spl),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f15060,f14759])).
% 47.27/6.50 fof(f15351,definition,(
% 47.27/6.50 sQ151_spl <=> (c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))=c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f15352,plain,(
% 47.27/6.50 c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))=c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A))|~sQ151_spl),
% 47.27/6.50 inference(component_clause,[status(thm)],[f15351])).
% 47.27/6.50 fof(f15354,plain,(
% 47.27/6.50 ~sQ94_spl|sQ151_spl|~sQ145_spl),
% 47.27/6.50 inference(split_clause,[status(thm)],[f15336,f9251,f15351,f15059])).
% 47.27/6.50 fof(f15486,plain,(
% 47.27/6.50 c_Message_Omsg_ONonce(v_NB)=hAPP(c_Message_Omsg_OKey,v_Ka)|~sQ151_spl),
% 47.27/6.50 inference(resolution,[status(thm)],[f1479,f15352])).
% 47.27/6.50 fof(f15491,plain,(
% 47.27/6.50 $false|~sQ151_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f15486,f1392])).
% 47.27/6.50 fof(f15492,plain,(
% 47.27/6.50 ~sQ151_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f15491])).
% 47.27/6.50 fof(f16287,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (c_List_Olist_ONil(X0)=c_List_OtakeWhile(c_List_Oset(c_List_Olist_ONil(X1),X1),c_List_Olist_OCons(X2,X3,X0),X0))),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f14711,f14378])).
% 47.27/6.50 fof(f16439,plain,(
% 47.27/6.50 ![X0,X1,X2]: (c_List_OtakeWhile(c_Event_Obad,c_List_Oappend(X0,c_List_Olist_OCons(c_Message_Oagent_OServer,X1,X2),X2),X2)=c_List_OtakeWhile(c_Event_Obad,X0,X2))),
% 47.27/6.50 inference(resolution,[status(thm)],[f1491,f1774])).
% 47.27/6.50 fof(f16537,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_OtakeWhile(c_Event_Obad,c_List_Olist_OCons(c_Message_Oagent_OServer,X0,X1),X1)=c_List_OtakeWhile(c_Event_Obad,c_List_Olist_ONil(X1),X1))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f887,f16439])).
% 47.27/6.50 fof(f16696,definition,(
% 47.27/6.50 ![X2]: (sQ159_spl <=> (c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,c_Message_Oagent_OServer)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X2)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f16697,plain,(
% 47.27/6.50 ![X0]: (c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,c_Message_Oagent_OServer)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0)=c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)|~sQ159_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f16696])).
% 47.27/6.50 fof(f16772,plain,(
% 47.27/6.50 ![X0,X1,X2]: (hBOOL(hAPP(c_List_Oset(c_List_Olist_ONil(X0),X0),X1))|~c_in(X1,c_List_Oset(c_List_Olist_ONil(X2),X2),X2))),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f16287,f1498])).
% 47.27/6.50 fof(f16831,plain,(
% 47.27/6.50 ![X0,X1]: (~c_in(X0,c_List_Oset(c_List_Olist_ONil(X1),X1),X1))),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f16772,f11728])).
% 47.27/6.50 fof(f17123,definition,(
% 47.27/6.50 sQ162_spl <=> (c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)),c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f17124,plain,(
% 47.27/6.50 c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)),c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)|~sQ162_spl),
% 47.27/6.50 inference(component_clause,[status(thm)],[f17123])).
% 47.27/6.50 fof(f17129,plain,(
% 47.27/6.50 $false|~sQ162_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f17124,f16831])).
% 47.27/6.50 fof(f17130,plain,(
% 47.27/6.50 ~sQ162_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f17129])).
% 47.27/6.50 fof(f18227,definition,(
% 47.27/6.50 ![X2,X3]: (sQ174_spl <=> (c_List_OtakeWhile(c_Event_Obad,X2,X3)=X2))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f18228,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_OtakeWhile(c_Event_Obad,X0,X1)=X0|~sQ174_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f18227])).
% 47.27/6.50 fof(f18253,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_OtakeWhile(c_Event_Obad,c_List_Olist_OCons(c_Message_Oagent_OServer,X0,X1),X1)=c_List_Olist_ONil(X1)|~sQ174_spl)),
% 47.27/6.50 inference(backward_demodulation,[status(thm)],[f18228,f16537])).
% 47.27/6.50 fof(f18334,plain,(
% 47.27/6.50 ![X0,X1]: (c_List_Olist_OCons(c_Message_Oagent_OServer,X0,X1)=c_List_Olist_ONil(X1)|~sQ174_spl)),
% 47.27/6.50 inference(forward_demodulation,[status(thm)],[f18228,f18253])).
% 47.27/6.50 fof(f18335,plain,(
% 47.27/6.50 $false|~sQ174_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f18334,f826])).
% 47.27/6.50 fof(f18336,plain,(
% 47.27/6.50 ~sQ174_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f18335])).
% 47.27/6.50 fof(f19134,plain,(
% 47.27/6.50 ![X0]: (hBOOL(hAPP(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K))))|~sQ93_spl)),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f9042,f944])).
% 47.27/6.50 fof(f19141,plain,(
% 47.27/6.50 hBOOL(hAPP(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),hAPP(c_Message_Omsg_OKey,v_K)))|~sQ68_spl),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f7143,f944])).
% 47.27/6.50 fof(f19144,plain,(
% 47.27/6.50 hBOOL(hAPP(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,c_Message_Oagent_OServer))))|~sQ159_spl),
% 47.27/6.50 inference(paramodulation,[status(thm)],[f16697,f944])).
% 47.27/6.50 fof(f19430,plain,(
% 47.27/6.50 ![X0]: (c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0)|~sQ68_spl)),
% 47.27/6.50 inference(resolution,[status(thm)],[f19141,f1464])).
% 47.27/6.50 fof(f19431,plain,(
% 47.27/6.50 $false|~sQ68_spl),
% 47.27/6.50 inference(backward_subsumption_resolution,[status(thm)],[f9709,f19430])).
% 47.27/6.50 fof(f19436,plain,(
% 47.27/6.50 ~sQ68_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f19431])).
% 47.27/6.50 fof(f19472,definition,(
% 47.27/6.50 ![X0]: (sQ184_spl <=> (~X0=X0))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f19473,plain,(
% 47.27/6.50 ![X0]: (~X0=X0|~sQ184_spl)),
% 47.27/6.50 inference(component_clause,[status(thm)],[f19472])).
% 47.27/6.50 fof(f19476,plain,(
% 47.27/6.50 $false|~sQ184_spl),
% 47.27/6.50 inference(trivial_equality_resolution,[status(thm)],[f19473])).
% 47.27/6.50 fof(f19477,plain,(
% 47.27/6.50 ~sQ184_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f19476])).
% 47.27/6.50 fof(f21275,definition,(
% 47.27/6.50 sQ199_spl <=> (c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 47.27/6.50 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 47.27/6.50 fof(f21277,plain,(
% 47.27/6.50 ~c_in(c_List_Olist_ONil(tc_Event_Oevent),c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|sQ199_spl),
% 47.27/6.50 inference(component_clause,[status(thm)],[f21275])).
% 47.27/6.50 fof(f21284,plain,(
% 47.27/6.50 $false|sQ199_spl),
% 47.27/6.50 inference(forward_subsumption_resolution,[status(thm)],[f21277,f1224])).
% 47.27/6.50 fof(f21285,plain,(
% 47.27/6.50 sQ199_spl),
% 47.27/6.50 inference(contradiction_clause,[status(thm)],[f21284])).
% 47.27/6.50 fof(f21521,plain,(
% 47.27/6.50 ![X0,X1,X2,X3]: (~c_List_OdropWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0,X1)=c_List_Olist_OCons(c_Message_Omsg_OMPair(X2,hAPP(c_Message_Omsg_OKey,v_K)),X3,X1)|~sQ93_spl)),
% 46.10/6.58 inference(resolution,[status(thm)],[f19134,f867])).
% 46.10/6.58 fof(f21641,plain,(
% 46.10/6.58 ![X0]: (c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,c_Message_Oagent_OServer)),c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),X0)|~sQ159_spl)),
% 46.10/6.58 inference(resolution,[status(thm)],[f19144,f1464])).
% 46.10/6.58 fof(f21643,plain,(
% 46.10/6.58 c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent)|~sQ159_spl),
% 46.10/6.58 inference(resolution,[status(thm)],[f21641,f12193])).
% 46.10/6.58 fof(f21648,plain,(
% 46.10/6.58 $false|~sQ159_spl),
% 46.10/6.58 inference(forward_subsumption_resolution,[status(thm)],[f21643,f1491])).
% 46.10/6.58 fof(f21649,plain,(
% 46.10/6.58 ~sQ159_spl),
% 46.10/6.58 inference(contradiction_clause,[status(thm)],[f21648])).
% 46.10/6.58 fof(f22930,plain,(
% 46.10/6.58 ![X0,X1,X2]: (c_List_OtakeWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Olist_OCons(c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K)),X1,X2),X2)=c_List_Olist_ONil(X2))),
% 46.10/6.58 inference(backward_demodulation,[status(thm)],[f1194,f14366])).
% 46.10/6.58 fof(f23874,plain,(
% 46.10/6.58 ![X0,X1,X2]: (c_List_Oappend(c_List_Olist_ONil(X0),c_List_OdropWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Olist_OCons(c_Message_Omsg_OMPair(X1,hAPP(c_Message_Omsg_OKey,v_K)),X2,X0),X0),X0)=c_List_Olist_OCons(c_Message_Omsg_OMPair(X1,hAPP(c_Message_Omsg_OKey,v_K)),X2,X0))),
% 46.10/6.58 inference(paramodulation,[status(thm)],[f22930,f816])).
% 46.10/6.58 fof(f23884,plain,(
% 46.10/6.58 ![X0,X1,X2]: (c_List_OdropWhile(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),c_List_Olist_OCons(c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K)),X1,X2),X2)=c_List_Olist_OCons(c_Message_Omsg_OMPair(X0,hAPP(c_Message_Omsg_OKey,v_K)),X1,X2))),
% 46.10/6.58 inference(forward_demodulation,[status(thm)],[f887,f23874])).
% 46.10/6.58 fof(f23885,plain,(
% 46.10/6.58 $false|~sQ93_spl),
% 46.10/6.58 inference(forward_subsumption_resolution,[status(thm)],[f23884,f21521])).
% 46.10/6.58 fof(f23886,plain,(
% 46.10/6.58 ~sQ93_spl),
% 46.10/6.58 inference(contradiction_clause,[status(thm)],[f23885])).
% 46.10/6.58 fof(f25618,plain,(
% 46.10/6.58 v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_A)))|c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 46.10/6.58 inference(resolution,[status(thm)],[f13263,f12694])).
% 46.10/6.58 fof(f25626,plain,(
% 46.10/6.58 sQ145_spl|sQ124_spl),
% 46.10/6.58 inference(split_clause,[status(thm)],[f25618,f15059,f13670])).
% 46.10/6.58 fof(f25627,plain,(
% 46.10/6.58 $false),
% 46.10/6.58 inference(sat_refutation,[status(thm)],[f9261,f9264,f13679,f15354,f15492,f17130,f18336,f19436,f19477,f21285,f21649,f23886,f25626])).
% 46.10/6.58 % SZS output end CNFRefutation for theBenchmark.p
% 5.27/6.65 % Elapsed time: 6.257831 seconds
% 5.27/6.65 % CPU time: 48.781598 seconds
% 5.27/6.65 % Total memory used: 619.735 MB
% 5.27/6.65 % Net memory used: 594.691 MB
%------------------------------------------------------------------------------