%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV360-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:47:29 PM UTC 2026
% Result : Unsatisfiable 0.44s 0.76s
% Output : CNFRefutation 0.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 51 ( 14 unt; 5 def)
% Number of atoms : 100 ( 2 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 94 ( 45 ~; 44 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 12 con; 0-2 aty)
% Number of variables : 40 ( 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2833,axiom,
! [V_X,V_Y,V_H] :
( 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2847,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2854,axiom,
! [V_H] : c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2936,axiom,
! [V_evs,V_B,V_X] :
( c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OGets(V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2938,axiom,
! [V_A,V_evs] :
( 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)
| ~ c_in(V_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(V_A,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2954,axiom,
! [V_A,V_X,V_H] :
( c_in(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(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),V_X),c_Message_Oanalz(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2970,negated_conjecture,
c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2973,negated_conjecture,
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_NAa),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2976,negated_conjecture,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2977,negated_conjecture,
c_in(v_Ba,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6446,plain,
! [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) ),
inference(miniscoping,[status(thm)],[f2833]) ).
fof(f6447,plain,
! [X0,X1,X2] :
( c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6446]) ).
fof(f6467,plain,
! [X0,X1] :
( c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f2847]) ).
fof(f6476,plain,
! [X0] : c_Message_Oanalz(c_Message_Oanalz(X0)) = c_Message_Oanalz(X0),
inference(cnf_transformation,[status(thm)],[f2854]) ).
fof(f6568,plain,
! [V_evs,V_X] :
( c_in(V_X,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)
| ! [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_evs,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(miniscoping,[status(thm)],[f2936]) ).
fof(f6569,plain,
! [X0,X1,X2] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OGets(X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(cnf_transformation,[status(thm)],[f6568]) ).
fof(f6572,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(X1,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(cnf_transformation,[status(thm)],[f2938]) ).
fof(f6598,plain,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg)
| ! [V_A] :
( ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Message_Oanalz(V_H),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(V_A),V_X),c_Message_Oanalz(V_H),tc_Message_Omsg) ) ),
inference(miniscoping,[status(thm)],[f2954]) ).
fof(f6599,plain,
! [X0,X1,X2] :
( c_in(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(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),X1),c_Message_Oanalz(X2),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f6598]) ).
fof(f6627,plain,
c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f2970]) ).
fof(f6630,plain,
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_NAa),c_Message_Omsg_ONonce(v_NB)))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(thm)],[f2973]) ).
fof(f6633,plain,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(cnf_transformation,[status(thm)],[f2976]) ).
fof(f6634,plain,
c_in(v_Ba,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(thm)],[f2977]) ).
fof(f6820,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X2,X0),X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f6447,f6467]) ).
fof(f7006,plain,
( 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_NAa),c_Message_Omsg_ONonce(v_NB))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[status(thm)],[f6569,f6630]) ).
fof(f7009,definition,
( sQ24_spl
<=> c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f7011,plain,
( sQ24_spl
| ~ c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f7009]) ).
fof(f7012,definition,
( sQ25_spl
<=> 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_NAa),c_Message_Omsg_ONonce(v_NB))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f7013,plain,
( ~ sQ25_spl
| 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_NAa),c_Message_Omsg_ONonce(v_NB))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7012]) ).
fof(f7015,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f7006,f7009,f7012]) ).
fof(f7023,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7011,f6627]) ).
fof(f7024,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f7023]) ).
fof(f7046,plain,
( ~ sQ25_spl
| 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_NAa),c_Message_Omsg_ONonce(v_NB)))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f7013,f6447]) ).
fof(f7173,plain,
( ~ sQ25_spl
| c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NB))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ 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) ),
inference(resolution,[status(thm)],[f6599,f7046]) ).
fof(f7180,definition,
( sQ42_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) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f7182,plain,
( sQ42_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) ),
inference(component_clause,[status(thm)],[f7180]) ).
fof(f7183,definition,
( sQ43_spl
<=> c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NB))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f7184,plain,
( ~ sQ43_spl
| c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NB))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f7183]) ).
fof(f7186,plain,
( ~ sQ25_spl
| sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f7173,f7180,f7183,f7012]) ).
fof(f7227,plain,
( sQ42_spl
| ~ c_in(v_evs3,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(v_Ba,c_Event_Obad,tc_Message_Oagent) ),
inference(resolution,[status(thm)],[f7182,f6572]) ).
fof(f7229,definition,
( sQ46_spl
<=> c_in(v_Ba,c_Event_Obad,tc_Message_Oagent) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f7231,plain,
( sQ46_spl
| ~ c_in(v_Ba,c_Event_Obad,tc_Message_Oagent) ),
inference(component_clause,[status(thm)],[f7229]) ).
fof(f7232,plain,
( sQ42_spl
| ~ sQ24_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f7227,f7229,f7009,f7180]) ).
fof(f7233,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7231,f6634]) ).
fof(f7234,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f7233]) ).
fof(f7504,plain,
( ~ sQ43_spl
| c_in(c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NAa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f7184,f6447]) ).
fof(f7569,plain,
( ~ sQ43_spl
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3))),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f7504,f6820]) ).
fof(f7573,plain,
( ~ sQ43_spl
| c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f6476,f7569]) ).
fof(f7574,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7573,f6633]) ).
fof(f7575,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f7574]) ).
fof(f7576,plain,
$false,
inference(sat_refutation,[status(thm)],[f7015,f7024,f7186,f7232,f7234,f7575]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV360-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n002.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.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 08:45:33 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.40/0.67 % Drodi V4.1.1
% 0.44/0.76 % Refutation found
% 0.44/0.76 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.44/0.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.46/0.87 % Elapsed time: 0.381813 seconds
% 0.46/0.87 % CPU time: 0.990651 seconds
% 0.46/0.87 % Total memory used: 170.000 MB
% 0.46/0.87 % Net memory used: 169.454 MB
%------------------------------------------------------------------------------