%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:49:36 PM UTC 2026
% Result : Unsatisfiable 26.71s 4.03s
% Output : CNFRefutation 26.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 16
% Syntax : Number of formulae : 55 ( 23 unt; 5 def)
% Number of atoms : 97 ( 35 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 78 ( 36 ~; 37 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-3 aty)
% Number of functors : 29 ( 29 usr; 19 con; 0-3 aty)
% Number of variables : 60 ( 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f536,axiom,
! [V_X,V_evs,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)
| c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f561,axiom,
! [V_X,V_B,V_K,V_A,V_evs,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)
| c_in(V_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| 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))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f585,axiom,
! [V_nat,V_msg,V_nat_H,V_msg_H] :
( V_msg = V_msg_H
| c_Message_Omsg_OCrypt(V_nat,V_msg) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f588,axiom,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f590,axiom,
! [V_msg1,V_msg2,V_msg1_H,V_msg2_H] :
( V_msg2 = V_msg2_H
| c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f607,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f609,negated_conjecture,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f611,negated_conjecture,
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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f614,negated_conjecture,
v_A = v_Aa,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f615,negated_conjecture,
v_B = v_Ba,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f616,negated_conjecture,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))) = v_X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1401,plain,
! [V_X,V_evs] :
( ! [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)
| c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ),
inference(miniscoping,[status(thm)],[f536]) ).
fof(f1402,plain,
! [X0,X1,X2,X3] :
( c_in(X2,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[status(thm)],[f1401]) ).
fof(f1440,plain,
! [V_X,V_B,V_K,V_A,V_evs] :
( ! [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)
| c_in(V_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| 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))) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f1441,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X2),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X3),c_Message_Omsg_OAgent(X0))) = X4
| ~ c_in(X5,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X3),X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X5)),tc_Message_Omsg)
| c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
inference(cnf_transformation,[status(thm)],[f1440]) ).
fof(f1472,plain,
! [V_msg,V_msg_H] :
( 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) ),
inference(miniscoping,[status(thm)],[f585]) ).
fof(f1473,plain,
! [X0,X1,X2,X3] :
( c_Message_Omsg_OCrypt(X2,X0) != c_Message_Omsg_OCrypt(X3,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f1472]) ).
fof(f1477,plain,
! [X0,X1] : c_Message_Omsg_OAgent(X0) != c_Message_Omsg_ONonce(X1),
inference(cnf_transformation,[status(thm)],[f588]) ).
fof(f1480,plain,
! [V_msg2,V_msg2_H] :
( V_msg2 = V_msg2_H
| ! [V_msg1,V_msg1_H] : c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) ),
inference(miniscoping,[status(thm)],[f590]) ).
fof(f1481,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OMPair(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f1480]) ).
fof(f1502,plain,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(thm)],[f607]) ).
fof(f1504,plain,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[status(thm)],[f609]) ).
fof(f1506,plain,
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),
inference(cnf_transformation,[status(thm)],[f611]) ).
fof(f1509,plain,
v_A = v_Aa,
inference(cnf_transformation,[status(thm)],[f614]) ).
fof(f1510,plain,
v_Ba = v_B,
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f1511,plain,
v_X = c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),
inference(cnf_transformation,[status(thm)],[f616]) ).
fof(f1580,plain,
c_in(c_Event_Oevent_OSays(v_S,v_A,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),
inference(forward_demodulation,[status(thm)],[f1509,f1506]) ).
fof(f1581,plain,
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),
inference(forward_demodulation,[status(thm)],[f1509,f1580]) ).
fof(f1582,plain,
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),
inference(forward_demodulation,[status(thm)],[f1510,f1581]) ).
fof(f1606,definition,
( sQ5_spl
<=> c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1608,plain,
( sQ5_spl
| ~ c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
inference(component_clause,[status(thm)],[f1606]) ).
fof(f1609,definition,
( sQ6_spl
<=> 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))) = v_X ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1610,plain,
( ~ sQ6_spl
| 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))) = v_X ),
inference(component_clause,[status(thm)],[f1609]) ).
fof(f1665,plain,
! [X0,X1] :
( c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)) = X1
| c_Message_Omsg_OCrypt(X0,X1) != v_X ),
inference(paramodulation,[status(thm)],[f1511,f1473]) ).
fof(f1671,plain,
( ~ sQ6_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))
| v_X != v_X ),
inference(paramodulation,[status(thm)],[f1610,f1665]) ).
fof(f1673,definition,
( sQ11_spl
<=> v_X = v_X ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1675,plain,
( sQ11_spl
| v_X != v_X ),
inference(component_clause,[status(thm)],[f1673]) ).
fof(f1680,definition,
( sQ13_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)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1681,plain,
( ~ sQ13_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)) ),
inference(component_clause,[status(thm)],[f1680]) ).
fof(f1683,plain,
( ~ sQ6_spl
| sQ13_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1671,f1673,f1680,f1609]) ).
fof(f1684,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1608,f1504]) ).
fof(f1685,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1684]) ).
fof(f1686,plain,
( sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1675]) ).
fof(f1687,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1686]) ).
fof(f1804,plain,
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),
inference(resolution,[status(thm)],[f1402,f1582]) ).
fof(f1817,plain,
( ~ sQ13_spl
| c_Message_Omsg_ONonce(v_NB) = c_Message_Omsg_OAgent(v_A) ),
inference(resolution,[status(thm)],[f1681,f1481]) ).
fof(f1833,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1817,f1477]) ).
fof(f1834,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1833]) ).
fof(f1905,plain,
( 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))) = v_X
| ~ c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(resolution,[status(thm)],[f1804,f1441]) ).
fof(f1910,definition,
( sQ21_spl
<=> c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1911,plain,
( ~ sQ21_spl
| c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
inference(component_clause,[status(thm)],[f1910]) ).
fof(f1913,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1905,f1910,f1606,f1609]) ).
fof(f1914,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1911,f1502]) ).
fof(f1915,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1914]) ).
fof(f1916,plain,
$false,
inference(sat_refutation,[status(thm)],[f1683,f1685,f1687,f1834,f1913,f1915]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n019.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 09:26:50 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.28/0.52 % Drodi V4.1.1
% 26.71/4.03 % Refutation found
% 26.71/4.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 26.71/4.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.08/4.16 % Elapsed time: 3.699038 seconds
% 6.08/4.16 % CPU time: 28.102697 seconds
% 6.08/4.16 % Total memory used: 427.318 MB
% 6.08/4.16 % Net memory used: 414.995 MB
%------------------------------------------------------------------------------