%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV346-1 : TPTP v9.3.1. Released v3.2.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:50:36 PM UTC 2026
% Result : Unsatisfiable 0.24s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV346-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n006.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 08:41:57 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.24/0.54 % Drodi V4.1.1
% 0.24/0.66 % Refutation found
% 0.24/0.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/0.66 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.66 fof(f2942,axiom,(
% 0.24/0.66 (![V_evs,V_A_H,V_B_H,V_K,V_na_H,V_nb_H,V_X_H,V_A,V_B,V_na,V_nb,V_X]: (( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| V_A = V_A_H ) ))),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2943,axiom,(
% 0.24/0.66 (![V_evs,V_A_H,V_B_H,V_K,V_na_H,V_nb_H,V_X_H,V_A,V_B,V_na,V_nb,V_X]: (( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| V_B = V_B_H ) ))),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2944,axiom,(
% 0.24/0.66 (![V_evs,V_A_H,V_B_H,V_K,V_na_H,V_nb_H,V_X_H,V_A,V_B,V_na,V_nb,V_X]: (( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| V_na = V_na_H ) ))),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2948,negated_conjecture,(
% 0.24/0.66 c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2949,negated_conjecture,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2950,negated_conjecture,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(v_na,v_nb)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OKey(v_K))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent) ),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f2953,negated_conjecture,(
% 0.24/0.66 v_na != c_Message_Omsg_ONonce(v_NA) ),
% 0.24/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.66 fof(f6553,plain,(
% 0.24/0.66 ![V_A_H,V_A]: ((![V_evs,V_K]: ((~c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|(![V_B_H,V_na_H,V_nb_H,V_X_H]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)))|(![V_B,V_na,V_nb,V_X]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))))|V_A=V_A_H)),
% 0.24/0.66 inference(miniscoping,[status(thm)],[f2942])).
% 0.24/0.66 fof(f6554,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X4,X5)))),X6)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X7,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X7),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X9,X10)))),X11)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|X7=X1)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f6553])).
% 0.24/0.66 fof(f6555,plain,(
% 0.24/0.66 ![V_B_H,V_B]: ((![V_evs,V_K]: ((~c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|(![V_A_H,V_na_H,V_nb_H,V_X_H]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)))|(![V_A,V_na,V_nb,V_X]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))))|V_B=V_B_H)),
% 0.24/0.66 inference(miniscoping,[status(thm)],[f2943])).
% 0.24/0.66 fof(f6556,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X4,X5)))),X6)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X7,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X7),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X9,X10)))),X11)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|X8=X2)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f6555])).
% 0.24/0.66 fof(f6557,plain,(
% 0.24/0.66 ![V_na_H,V_na]: ((![V_evs,V_K]: ((~c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|(![V_A_H,V_B_H,V_nb_H,V_X_H]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A_H,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A_H),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B_H),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na_H,V_nb_H)))),V_X_H)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)))|(![V_A,V_B,V_nb,V_X]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(V_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(V_K),c_Message_Omsg_OMPair(V_na,V_nb)))),V_X)),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))))|V_na=V_na_H)),
% 0.24/0.66 inference(miniscoping,[status(thm)],[f2944])).
% 0.24/0.66 fof(f6558,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X4,X5)))),X6)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X7,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X7),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X8),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X9,X10)))),X11)),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|X9=X4)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f6557])).
% 0.24/0.66 fof(f6563,plain,(
% 0.24/0.66 c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f2948])).
% 0.24/0.66 fof(f6564,plain,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f2949])).
% 0.24/0.66 fof(f6565,plain,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(v_na,v_nb)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OKey(v_K))))),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f2950])).
% 0.24/0.66 fof(f6568,plain,(
% 0.24/0.66 ~v_na=c_Message_Omsg_ONonce(v_NA)),
% 0.24/0.66 inference(cnf_transformation,[status(thm)],[f2953])).
% 0.24/0.66 fof(f7101,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X0=v_A)),
% 0.24/0.66 inference(resolution,[status(thm)],[f6554,f6565])).
% 0.24/0.66 fof(f7105,definition,(
% 0.24/0.66 sQ32_spl <=> (c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))),
% 0.24/0.66 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.24/0.66 fof(f7107,plain,(
% 0.24/0.66 ~c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|sQ32_spl),
% 0.24/0.66 inference(component_clause,[status(thm)],[f7105])).
% 0.24/0.66 fof(f7108,definition,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (sQ33_spl <=> (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X0=v_A))),
% 0.24/0.66 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.24/0.66 fof(f7109,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X0=v_A|~sQ33_spl)),
% 0.24/0.66 inference(component_clause,[status(thm)],[f7108])).
% 0.24/0.66 fof(f7111,plain,(
% 0.24/0.66 ~sQ32_spl|sQ33_spl),
% 0.24/0.66 inference(split_clause,[status(thm)],[f7101,f7105,f7108])).
% 0.24/0.66 fof(f7121,plain,(
% 0.24/0.66 $false|sQ32_spl),
% 0.24/0.66 inference(forward_subsumption_resolution,[status(thm)],[f7107,f6563])).
% 0.24/0.66 fof(f7122,plain,(
% 0.24/0.66 sQ32_spl),
% 0.24/0.66 inference(contradiction_clause,[status(thm)],[f7121])).
% 0.24/0.66 fof(f7123,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X1=v_B)),
% 0.24/0.66 inference(resolution,[status(thm)],[f6556,f6565])).
% 0.24/0.66 fof(f7127,definition,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (sQ36_spl <=> (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X1=v_B))),
% 0.24/0.66 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.24/0.66 fof(f7128,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X1=v_B|~sQ36_spl)),
% 0.24/0.66 inference(component_clause,[status(thm)],[f7127])).
% 0.24/0.66 fof(f7130,plain,(
% 0.24/0.66 ~sQ32_spl|sQ36_spl),
% 0.24/0.66 inference(split_clause,[status(thm)],[f7123,f7105,f7127])).
% 0.24/0.66 fof(f7160,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(v_evso,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X2=v_na)),
% 0.24/0.66 inference(resolution,[status(thm)],[f6558,f6565])).
% 0.24/0.66 fof(f7164,definition,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (sQ43_spl <=> (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X2=v_na))),
% 0.24/0.66 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.24/0.66 fof(f7165,plain,(
% 0.24/0.66 ![X0,X1,X2,X3,X4]: (~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(X2,X3)))),X4)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|X2=v_na|~sQ43_spl)),
% 0.24/0.66 inference(component_clause,[status(thm)],[f7164])).
% 0.24/0.66 fof(f7167,plain,(
% 0.24/0.66 ~sQ32_spl|sQ43_spl),
% 0.24/0.66 inference(split_clause,[status(thm)],[f7160,f7105,f7164])).
% 0.24/0.66 fof(f7218,plain,(
% 0.24/0.66 v_Aa=v_A|~sQ33_spl),
% 0.24/0.66 inference(resolution,[status(thm)],[f7109,f6564])).
% 0.24/0.66 fof(f7222,plain,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_Aa,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|~sQ33_spl),
% 0.24/0.66 inference(backward_demodulation,[status(thm)],[f7218,f6564])).
% 0.24/0.66 fof(f7224,plain,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|~sQ33_spl),
% 0.24/0.66 inference(forward_demodulation,[status(thm)],[f7218,f7222])).
% 0.24/0.66 fof(f7387,plain,(
% 0.24/0.66 v_Ba=v_B|~sQ36_spl|~sQ33_spl),
% 0.24/0.66 inference(resolution,[status(thm)],[f7128,f7224])).
% 0.24/0.66 fof(f7389,plain,(
% 0.24/0.66 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evso,tc_Event_Oevent),tc_Event_Oevent)|~sQ36_spl|~sQ33_spl),
% 0.47/0.67 inference(backward_demodulation,[status(thm)],[f7387,f7224])).
% 0.47/0.67 fof(f7552,plain,(
% 0.47/0.67 c_Message_Omsg_ONonce(v_NA)=v_na|~sQ43_spl|~sQ36_spl|~sQ33_spl),
% 0.47/0.67 inference(resolution,[status(thm)],[f7165,f7389])).
% 0.47/0.67 fof(f7554,plain,(
% 0.47/0.67 $false|~sQ43_spl|~sQ36_spl|~sQ33_spl),
% 0.47/0.67 inference(forward_subsumption_resolution,[status(thm)],[f7552,f6568])).
% 0.47/0.67 fof(f7555,plain,(
% 0.47/0.67 ~sQ43_spl|~sQ36_spl|~sQ33_spl),
% 0.47/0.67 inference(contradiction_clause,[status(thm)],[f7554])).
% 0.47/0.67 fof(f7556,plain,(
% 0.47/0.67 $false),
% 0.47/0.67 inference(sat_refutation,[status(thm)],[f7111,f7122,f7130,f7167,f7555])).
% 0.47/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 0.47/0.70 % Elapsed time: 0.349471 seconds
% 0.47/0.70 % CPU time: 1.120260 seconds
% 0.47/0.70 % Total memory used: 238.906 MB
% 0.47/0.70 % Net memory used: 238.008 MB
%------------------------------------------------------------------------------