%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV792-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:10 PM UTC 2026
% Result : Unsatisfiable 29.68s 4.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV792-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n008.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 09:25:54 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.27/0.53 % Drodi V4.1.1
% 29.68/4.44 % Refutation found
% 29.68/4.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 29.68/4.44 % SZS output start CNFRefutation for theBenchmark
% 29.68/4.44 fof(f7,axiom,(
% 29.68/4.44 (![V_c,V_B,T_a,V_A]: (( c_in(V_c,V_B,T_a)| c_in(V_c,V_A,T_a)| ~ c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ) ))),
% 29.68/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.68/4.44 fof(f8,axiom,(
% 29.68/4.44 (![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) ) ))),
% 29.68/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.68/4.44 fof(f395,axiom,(
% 29.68/4.44 (![V_P,T_a]: (c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ))),
% 29.68/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.68/4.44 fof(f494,axiom,(
% 29.68/4.44 (![V_xs,V_x,T_a]: (V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ))),
% 29.68/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.68/4.44 fof(f523,axiom,(
% 29.68/4.44 (![V_P,V_xs,T_a,V_x]: (( c_List_OtakeWhile(V_P,V_xs,T_a) != V_xs| hBOOL(hAPP(V_P,V_x))| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f533,axiom,(
% 26.72/4.44 (![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) ) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f558,axiom,(
% 26.72/4.44 (![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) ) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f567,axiom,(
% 26.72/4.44 (![V_nat,V_msg1_H,V_msg2_H]: (c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f582,axiom,(
% 26.72/4.44 (![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 ) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f605,negated_conjecture,(
% 26.72/4.44 ~ c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f606,negated_conjecture,(
% 26.72/4.44 c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f608,negated_conjecture,(
% 26.72/4.44 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) ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f611,negated_conjecture,(
% 26.72/4.44 v_B = v_Aa ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f612,negated_conjecture,(
% 26.72/4.44 v_A = v_Ba ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f613,negated_conjecture,(
% 26.72/4.44 c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)) = v_X ),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f642,axiom,(
% 26.72/4.44 (![V_X,V_Y,T_a]: (( V_X = V_Y| ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ))),
% 26.72/4.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.72/4.44 fof(f650,plain,(
% 26.72/4.44 ![X0,X1,X2,X3]: (c_in(X0,X1,X2)|c_in(X0,X3,X2)|~c_in(X0,c_Lattices_Oupper__semilattice__class_Osup(X3,X1,tc_fun(X2,tc_bool)),X2))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f7])).
% 26.72/4.44 fof(f651,plain,(
% 26.72/4.44 ![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))),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f8])).
% 26.72/4.44 fof(f652,plain,(
% 26.72/4.44 ![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))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f651])).
% 26.72/4.44 fof(f1187,plain,(
% 26.72/4.44 ![X0,X1]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_Olist_ONil(X1))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f395])).
% 26.72/4.44 fof(f1332,plain,(
% 26.72/4.44 ![X0,X1,X2]: (~X0=c_List_Olist_OCons(X1,X0,X2))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f494])).
% 26.72/4.44 fof(f1379,plain,(
% 26.72/4.44 ![V_xs,T_a,V_x]: ((![V_P]: (~c_List_OtakeWhile(V_P,V_xs,T_a)=V_xs|hBOOL(hAPP(V_P,V_x))))|~c_in(V_x,c_List_Oset(V_xs,T_a),T_a))),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f523])).
% 26.72/4.44 fof(f1380,plain,(
% 26.72/4.44 ![X0,X1,X2,X3]: (~c_List_OtakeWhile(X0,X1,X2)=X1|hBOOL(hAPP(X0,X3))|~c_in(X3,c_List_Oset(X1,X2),X2))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f1379])).
% 26.72/4.44 fof(f1393,plain,(
% 26.72/4.44 ![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)))),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f533])).
% 26.72/4.44 fof(f1394,plain,(
% 26.72/4.44 ![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))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f1393])).
% 26.72/4.44 fof(f1432,plain,(
% 26.72/4.44 ![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)))),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f558])).
% 26.72/4.44 fof(f1433,plain,(
% 26.72/4.44 ![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))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f1432])).
% 26.72/4.44 fof(f1444,plain,(
% 26.72/4.44 ![X0,X1,X2]: (~c_Message_Omsg_ONonce(X0)=c_Message_Omsg_OMPair(X1,X2))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f567])).
% 26.72/4.44 fof(f1464,plain,(
% 26.72/4.44 ![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)),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f582])).
% 26.72/4.44 fof(f1465,plain,(
% 26.72/4.44 ![X0,X1,X2,X3]: (~c_Message_Omsg_OCrypt(X0,X1)=c_Message_Omsg_OCrypt(X2,X3)|X1=X3)),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f1464])).
% 26.72/4.44 fof(f1495,plain,(
% 26.72/4.44 ~c_in(v_B,c_Event_Obad,tc_Message_Oagent)),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f605])).
% 26.72/4.44 fof(f1496,plain,(
% 26.72/4.44 c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f606])).
% 26.72/4.44 fof(f1498,plain,(
% 26.72/4.44 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)),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f608])).
% 26.72/4.44 fof(f1501,plain,(
% 26.72/4.44 v_B=v_Aa),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f611])).
% 26.72/4.44 fof(f1502,plain,(
% 26.72/4.44 v_A=v_Ba),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f612])).
% 26.72/4.44 fof(f1503,plain,(
% 26.72/4.44 c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))=v_X),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f613])).
% 26.72/4.44 fof(f1540,plain,(
% 26.72/4.44 ![V_X,V_Y]: (V_X=V_Y|(![T_a]: ~hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y))))),
% 26.72/4.44 inference(miniscoping,[status(thm)],[f642])).
% 26.72/4.44 fof(f1541,plain,(
% 26.72/4.44 ![X0,X1,X2]: (X0=X1|~hBOOL(hAPP(hAPP(c_fequal(X2),X0),X1)))),
% 26.72/4.44 inference(cnf_transformation,[status(thm)],[f1540])).
% 26.72/4.44 fof(f1589,plain,(
% 26.72/4.44 ![X0]: (c_in(v_evs3,c_Lattices_Oupper__semilattice__class_Osup(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_fun(tc_List_Olist(tc_Event_Oevent),tc_bool)),tc_List_Olist(tc_Event_Oevent)))),
% 26.72/4.44 inference(resolution,[status(thm)],[f1496,f652])).
% 26.72/4.44 fof(f1590,plain,(
% 26.72/4.44 c_in(c_Event_Oevent_OSays(v_S,v_B,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)),
% 26.72/4.44 inference(forward_demodulation,[status(thm)],[f1501,f1498])).
% 26.72/4.44 fof(f1591,plain,(
% 26.72/4.44 c_in(c_Event_Oevent_OSays(v_S,v_B,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),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)),
% 26.72/4.44 inference(forward_demodulation,[status(thm)],[f1501,f1590])).
% 26.72/4.44 fof(f1592,plain,(
% 26.72/4.44 c_in(c_Event_Oevent_OSays(v_S,v_B,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 26.72/4.44 inference(forward_demodulation,[status(thm)],[f1502,f1591])).
% 26.72/4.44 fof(f1671,plain,(
% 26.72/4.44 ![X0]: (c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(v_evs3,X0,tc_List_Olist(tc_Event_Oevent)))),
% 26.72/4.44 inference(resolution,[status(thm)],[f1589,f650])).
% 26.72/4.44 fof(f1675,definition,(
% 26.72/4.44 sQ2_spl <=> (c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 26.72/4.44 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 26.72/4.44 fof(f1678,definition,(
% 26.72/4.44 ![X0]: (sQ3_spl <=> (c_in(v_evs3,X0,tc_List_Olist(tc_Event_Oevent))))),
% 26.72/4.44 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 26.72/4.44 fof(f1679,plain,(
% 26.72/4.44 ![X0]: (c_in(v_evs3,X0,tc_List_Olist(tc_Event_Oevent))|~sQ3_spl)),
% 26.72/4.44 inference(component_clause,[status(thm)],[f1678])).
% 26.72/4.44 fof(f1681,plain,(
% 26.72/4.44 sQ2_spl|sQ3_spl),
% 26.72/4.44 inference(split_clause,[status(thm)],[f1671,f1675,f1678])).
% 26.72/4.44 fof(f3122,plain,(
% 26.72/4.44 ![X0,X1]: (~v_X=c_Message_Omsg_OCrypt(X0,X1)|c_Message_Omsg_ONonce(v_Nb)=X1)),
% 26.72/4.44 inference(paramodulation,[status(thm)],[f1503,f1465])).
% 26.72/4.44 fof(f5077,definition,(
% 26.72/4.44 ![X1]: (sQ121_spl <=> (v_evs3=X1))),
% 26.72/4.44 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 26.72/4.44 fof(f5078,plain,(
% 26.72/4.44 ![X0]: (v_evs3=X0|~sQ121_spl)),
% 26.72/4.44 inference(component_clause,[status(thm)],[f5077])).
% 26.72/4.44 fof(f5083,plain,(
% 26.72/4.44 $false|~sQ121_spl),
% 26.72/4.44 inference(resolution,[status(thm)],[f5078,f1332])).
% 26.72/4.44 fof(f5100,plain,(
% 26.72/4.44 ~sQ121_spl),
% 26.72/4.44 inference(contradiction_clause,[status(thm)],[f5083])).
% 26.72/4.44 fof(f5779,plain,(
% 26.72/4.44 ![X0,X1]: (~c_List_OtakeWhile(X0,X1,tc_List_Olist(tc_Event_Oevent))=X1|hBOOL(hAPP(X0,v_evs3))|~sQ3_spl)),
% 26.72/4.44 inference(resolution,[status(thm)],[f1380,f1679])).
% 26.72/4.44 fof(f5812,plain,(
% 26.72/4.44 ![X0]: (~c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent))=c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent))|hBOOL(hAPP(X0,v_evs3))|~sQ3_spl)),
% 26.72/4.44 inference(paramodulation,[status(thm)],[f1187,f5779])).
% 26.72/4.44 fof(f5813,definition,(
% 26.72/4.44 sQ154_spl <=> (c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent))=c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent)))),
% 26.72/4.44 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 26.72/4.44 fof(f5815,plain,(
% 26.72/4.44 ~c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent))=c_List_Olist_ONil(tc_List_Olist(tc_Event_Oevent))|sQ154_spl),
% 26.72/4.44 inference(component_clause,[status(thm)],[f5813])).
% 26.72/4.44 fof(f5816,definition,(
% 26.72/4.44 ![X0]: (sQ155_spl <=> (hBOOL(hAPP(X0,v_evs3))))),
% 26.72/4.44 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 26.72/4.51 fof(f5817,plain,(
% 26.72/4.51 ![X0]: (hBOOL(hAPP(X0,v_evs3))|~sQ155_spl)),
% 26.72/4.51 inference(component_clause,[status(thm)],[f5816])).
% 26.72/4.51 fof(f5819,plain,(
% 26.72/4.51 ~sQ154_spl|sQ155_spl|~sQ3_spl),
% 26.72/4.51 inference(split_clause,[status(thm)],[f5812,f5813,f5816,f1678])).
% 26.72/4.51 fof(f5822,plain,(
% 26.72/4.51 ![X0]: (X0=v_evs3|~sQ155_spl)),
% 26.72/4.51 inference(resolution,[status(thm)],[f5817,f1541])).
% 26.72/4.51 fof(f5827,plain,(
% 26.72/4.51 sQ121_spl|~sQ155_spl),
% 26.72/4.51 inference(split_clause,[status(thm)],[f5822,f5077,f5816])).
% 26.72/4.51 fof(f5829,plain,(
% 26.72/4.51 $false|sQ154_spl),
% 26.72/4.51 inference(trivial_equality_resolution,[status(thm)],[f5815])).
% 26.72/4.51 fof(f5830,plain,(
% 26.72/4.51 sQ154_spl),
% 26.72/4.51 inference(contradiction_clause,[status(thm)],[f5829])).
% 26.72/4.51 fof(f5832,plain,(
% 26.72/4.51 c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),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)),
% 26.72/4.51 inference(resolution,[status(thm)],[f1394,f1592])).
% 26.72/4.51 fof(f7272,definition,(
% 26.72/4.51 sQ209_spl <=> (v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_B))))),
% 26.72/4.51 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 26.72/4.51 fof(f7273,plain,(
% 26.72/4.51 v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_B)))|~sQ209_spl),
% 26.72/4.51 inference(component_clause,[status(thm)],[f7272])).
% 26.72/4.51 fof(f9935,plain,(
% 26.72/4.51 v_X=c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_B)))|~c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(v_B,c_Event_Obad,tc_Message_Oagent)),
% 26.72/4.51 inference(resolution,[status(thm)],[f5832,f1433])).
% 26.72/4.51 fof(f9953,definition,(
% 26.72/4.51 sQ321_spl <=> (c_in(v_B,c_Event_Obad,tc_Message_Oagent))),
% 26.72/4.51 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 26.72/4.51 fof(f9954,plain,(
% 26.72/4.51 c_in(v_B,c_Event_Obad,tc_Message_Oagent)|~sQ321_spl),
% 26.72/4.51 inference(component_clause,[status(thm)],[f9953])).
% 26.72/4.51 fof(f9957,plain,(
% 26.72/4.51 sQ209_spl|~sQ2_spl|sQ321_spl),
% 26.72/4.51 inference(split_clause,[status(thm)],[f9935,f7272,f1675,f9953])).
% 26.72/4.51 fof(f9964,plain,(
% 26.72/4.51 $false|~sQ321_spl),
% 26.72/4.51 inference(forward_subsumption_resolution,[status(thm)],[f9954,f1495])).
% 26.72/4.51 fof(f9965,plain,(
% 26.72/4.51 ~sQ321_spl),
% 26.72/4.51 inference(contradiction_clause,[status(thm)],[f9964])).
% 26.72/4.51 fof(f13182,plain,(
% 26.72/4.51 c_Message_Omsg_ONonce(v_Nb)=c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_B))|~sQ209_spl),
% 26.72/4.51 inference(resolution,[status(thm)],[f7273,f3122])).
% 26.72/4.51 fof(f13206,plain,(
% 26.72/4.51 $false|~sQ209_spl),
% 26.72/4.51 inference(forward_subsumption_resolution,[status(thm)],[f13182,f1444])).
% 26.72/4.51 fof(f13207,plain,(
% 26.72/4.51 ~sQ209_spl),
% 26.72/4.51 inference(contradiction_clause,[status(thm)],[f13206])).
% 26.72/4.51 fof(f13208,plain,(
% 26.72/4.51 $false),
% 26.72/4.51 inference(sat_refutation,[status(thm)],[f1681,f5100,f5819,f5827,f5830,f9957,f9965,f13207])).
% 26.72/4.51 % SZS output end CNFRefutation for theBenchmark.p
% 1.61/4.53 % Elapsed time: 4.060364 seconds
% 1.61/4.53 % CPU time: 30.966622 seconds
% 1.61/4.53 % Total memory used: 448.587 MB
% 1.61/4.53 % Net memory used: 427.323 MB
%------------------------------------------------------------------------------