%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV359-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:50:38 PM UTC 2026
% Result : Unsatisfiable 2.57s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV359-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Mon Sep 21 08:42:53 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 2.57/0.73 % Refutation found
% 2.57/0.73 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.57/0.73 % SZS output start CNFRefutation for theBenchmark
% 2.57/0.73 fof(f2833,axiom,(
% 2.57/0.73 (![V_X,V_Y,V_H]: (( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)| c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ))),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2834,axiom,(
% 2.57/0.73 (![V_X,V_Y,V_H]: (( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)| c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ))),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2936,axiom,(
% 2.57/0.73 (![V_evs,V_B,V_X]: (( ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))| ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ))),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2938,axiom,(
% 2.57/0.73 (![V_A,V_evs]: (( ~ c_in(V_A,c_Event_Obad,tc_Message_Oagent)| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))| c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ) ))),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2954,axiom,(
% 2.57/0.73 (![V_A,V_X,V_H]: (( ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),V_X),c_Message_Oanalz(V_H),tc_Message_Omsg)| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Message_Oanalz(V_H),tc_Message_Omsg)| c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ))),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2970,negated_conjecture,(
% 2.57/0.73 c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2973,negated_conjecture,(
% 2.57/0.73 c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent) ),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2976,negated_conjecture,(
% 2.57/0.73 ~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f2977,negated_conjecture,(
% 2.57/0.73 c_in(v_Ba,c_Event_Obad,tc_Message_Oagent) ),
% 2.57/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.57/0.73 fof(f6446,plain,(
% 2.57/0.73 ![V_Y,V_H]: ((![V_X]: ~c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))|c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg))),
% 2.57/0.73 inference(miniscoping,[status(thm)],[f2833])).
% 2.57/0.73 fof(f6447,plain,(
% 2.57/0.73 ![X0,X1,X2]: (~c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)|c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f6446])).
% 2.57/0.73 fof(f6448,plain,(
% 2.57/0.73 ![V_X,V_H]: ((![V_Y]: ~c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg))|c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg))),
% 2.57/0.73 inference(miniscoping,[status(thm)],[f2834])).
% 2.57/0.73 fof(f6449,plain,(
% 2.57/0.73 ![X0,X1,X2]: (~c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg)|c_in(X0,c_Message_Oanalz(X2),tc_Message_Omsg))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f6448])).
% 2.57/0.73 fof(f6568,plain,(
% 2.57/0.73 ![V_evs,V_X]: ((~c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|(![V_B]: ~c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)))|c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg))),
% 2.57/0.73 inference(miniscoping,[status(thm)],[f2936])).
% 2.57/0.73 fof(f6569,plain,(
% 2.57/0.73 ![X0,X1,X2]: (~c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|~c_in(c_Event_Oevent_OGets(X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)|c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f6568])).
% 2.57/0.73 fof(f6572,plain,(
% 2.57/0.73 ![X0,X1]: (~c_in(X0,c_Event_Obad,tc_Message_Oagent)|~c_in(X1,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))|c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f2938])).
% 2.57/0.73 fof(f6598,plain,(
% 2.57/0.73 ![V_X,V_H]: ((![V_A]: (~c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),V_X),c_Message_Oanalz(V_H),tc_Message_Omsg)|~c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Message_Oanalz(V_H),tc_Message_Omsg)))|c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg))),
% 2.57/0.73 inference(miniscoping,[status(thm)],[f2954])).
% 2.57/0.73 fof(f6599,plain,(
% 2.57/0.73 ![X0,X1,X2]: (~c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),X1),c_Message_Oanalz(X2),tc_Message_Omsg)|~c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oanalz(X2),tc_Message_Omsg)|c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f6598])).
% 2.57/0.73 fof(f6627,plain,(
% 2.57/0.73 c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f2970])).
% 2.57/0.73 fof(f6630,plain,(
% 2.57/0.73 c_in(c_Event_Oevent_OGets(c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f2973])).
% 2.57/0.73 fof(f6633,plain,(
% 2.57/0.73 ~c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f2976])).
% 2.57/0.73 fof(f6634,plain,(
% 2.57/0.73 c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)),
% 2.57/0.73 inference(cnf_transformation,[status(thm)],[f2977])).
% 2.57/0.73 fof(f7060,plain,(
% 2.57/0.73 ![X0,X1]: (~c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent)|c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 2.57/0.73 inference(resolution,[status(thm)],[f6569,f6627])).
% 2.57/0.73 fof(f7109,plain,(
% 2.57/0.73 ![X0]: (~c_in(X0,c_Event_Obad,tc_Message_Oagent)|c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 2.57/0.73 inference(resolution,[status(thm)],[f6572,f6627])).
% 2.57/0.73 fof(f7117,plain,(
% 2.57/0.73 c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 2.57/0.73 inference(resolution,[status(thm)],[f7060,f6630])).
% 2.57/0.73 fof(f8803,plain,(
% 2.57/0.73 c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 2.57/0.73 inference(resolution,[status(thm)],[f7117,f6447])).
% 2.57/0.73 fof(f10004,plain,(
% 2.57/0.73 ~c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_Ba)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)|c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)),
% 2.57/0.73 inference(resolution,[status(thm)],[f8803,f6599])).
% 2.57/0.73 fof(f10005,definition,(
% 2.57/0.73 sQ52_spl <=> (c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_Ba)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 2.57/0.73 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 2.57/0.73 fof(f10007,plain,(
% 2.57/0.73 ~c_in(c_Message_Omsg_OKey(c_Public_OshrK(v_Ba)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)|sQ52_spl),
% 2.57/0.73 inference(component_clause,[status(thm)],[f10005])).
% 2.57/0.73 fof(f10008,definition,(
% 2.57/0.73 sQ53_spl <=> (c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg))),
% 2.57/0.75 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 2.57/0.75 fof(f10009,plain,(
% 2.57/0.75 c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)|~sQ53_spl),
% 2.57/0.75 inference(component_clause,[status(thm)],[f10008])).
% 2.57/0.75 fof(f10011,plain,(
% 2.57/0.75 ~sQ52_spl|sQ53_spl),
% 2.57/0.75 inference(split_clause,[status(thm)],[f10004,f10005,f10008])).
% 2.57/0.75 fof(f10012,plain,(
% 2.57/0.75 ~c_in(v_Ba,c_Event_Obad,tc_Message_Oagent)|sQ52_spl),
% 2.57/0.75 inference(resolution,[status(thm)],[f10007,f7109])).
% 2.57/0.75 fof(f10014,plain,(
% 2.57/0.75 $false|sQ52_spl),
% 2.57/0.75 inference(forward_subsumption_resolution,[status(thm)],[f10012,f6634])).
% 2.57/0.75 fof(f10015,plain,(
% 2.57/0.75 sQ52_spl),
% 2.57/0.75 inference(contradiction_clause,[status(thm)],[f10014])).
% 2.57/0.75 fof(f10078,plain,(
% 2.57/0.75 c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NBa)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)|~sQ53_spl),
% 2.57/0.75 inference(resolution,[status(thm)],[f10009,f6447])).
% 2.57/0.75 fof(f10096,plain,(
% 2.57/0.75 c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)|~sQ53_spl),
% 2.57/0.75 inference(resolution,[status(thm)],[f10078,f6449])).
% 2.57/0.75 fof(f10100,plain,(
% 2.57/0.75 $false|~sQ53_spl),
% 2.57/0.75 inference(forward_subsumption_resolution,[status(thm)],[f10096,f6633])).
% 2.57/0.75 fof(f10101,plain,(
% 2.57/0.75 ~sQ53_spl),
% 2.57/0.75 inference(contradiction_clause,[status(thm)],[f10100])).
% 2.57/0.75 fof(f10102,plain,(
% 2.57/0.75 $false),
% 2.57/0.75 inference(sat_refutation,[status(thm)],[f10011,f10015,f10101])).
% 2.57/0.75 % SZS output end CNFRefutation for theBenchmark.p
% 2.57/0.76 % Elapsed time: 0.454957 seconds
% 2.57/0.76 % CPU time: 2.970086 seconds
% 2.57/0.76 % Total memory used: 298.321 MB
% 2.57/0.76 % Net memory used: 295.560 MB
%------------------------------------------------------------------------------