%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV801-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 : n016.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:11 PM UTC 2026
% Result : Unsatisfiable 24.41s 4.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV801-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.96 % Computer : n016.cluster.edu
% 0.07/0.96 % Model : x86_64 x86_64
% 0.07/0.96 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.96 % Memory : 8046.5625MB
% 0.07/0.96 % OS : Linux 6.8.0-71-generic
% 0.07/0.96 % CPULimit : 300
% 0.07/0.96 % WCLimit : 300
% 0.07/0.96 % DateTime : Mon Sep 21 09:30:40 UTC 2026
% 0.07/0.97 % CPUTime :
% 0.07/1.01 % Drodi V4.1.1
% 24.41/4.36 % Refutation found
% 24.41/4.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 24.41/4.36 % SZS output start CNFRefutation for theBenchmark
% 24.41/4.36 fof(f56,axiom,(
% 24.41/4.36 c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f69,axiom,(
% 24.41/4.36 (![V_B,V_a,T_a]: (c_lessequals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f237,axiom,(
% 24.41/4.36 (![V_K]: (( c_Message_OinvKey(V_K) = V_K| ~ c_in(V_K,c_Message_OsymKeys,tc_nat) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f388,axiom,(
% 24.41/4.36 (![V_K,V_H,V_X]: (( c_in(c_Message_OinvKey(V_K),c_Message_OkeysFor(V_H),tc_nat)| ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f444,axiom,(
% 24.41/4.36 (![V_K,V_evs]: (( ~ c_in(V_K,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs))),tc_nat)| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))| ~ c_in(V_K,c_Message_OsymKeys,tc_nat)| c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Event_Oused(V_evs),tc_Message_Omsg) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f457,axiom,(
% 24.41/4.36 (![V_H]: (c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f471,axiom,(
% 24.41/4.36 (![V_X,V_H]: (( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)| ~ c_in(V_X,V_H,tc_Message_Omsg) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f472,axiom,(
% 24.41/4.36 (![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) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f481,axiom,(
% 24.41/4.36 (![V_H]: (c_Message_Oanalz(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f513,axiom,(
% 24.41/4.36 (![V_x,V_S,T_a]: (( c_in(V_x,V_S,T_a)| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f514,axiom,(
% 24.41/4.36 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ c_in(V_x,V_S,T_a) ) ))),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f539,negated_conjecture,(
% 24.41/4.36 ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f540,negated_conjecture,(
% 24.41/4.36 ~ c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f541,negated_conjecture,(
% 24.41/4.36 c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f542,negated_conjecture,(
% 24.41/4.36 ~ c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f543,negated_conjecture,(
% 24.41/4.36 c_in(v_KAB,c_Message_OsymKeys,tc_nat) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f551,negated_conjecture,(
% 24.41/4.36 c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg) ),
% 24.41/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.41/4.36 fof(f656,plain,(
% 24.41/4.36 c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f56])).
% 24.41/4.36 fof(f678,plain,(
% 24.41/4.36 ![X0,X1,X2]: (c_lessequals(X0,c_Set_Oinsert(X1,X0,X2),tc_fun(X2,tc_bool)))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f69])).
% 24.41/4.36 fof(f912,plain,(
% 24.41/4.36 ![X0]: (c_Message_OinvKey(X0)=X0|~c_in(X0,c_Message_OsymKeys,tc_nat))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f237])).
% 24.41/4.36 fof(f1126,plain,(
% 24.41/4.36 ![V_K,V_H]: (c_in(c_Message_OinvKey(V_K),c_Message_OkeysFor(V_H),tc_nat)|(![V_X]: ~c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)))),
% 24.41/4.36 inference(miniscoping,[status(thm)],[f388])).
% 24.41/4.36 fof(f1127,plain,(
% 24.41/4.36 ![X0,X1,X2]: (c_in(c_Message_OinvKey(X0),c_Message_OkeysFor(X1),tc_nat)|~c_in(c_Message_Omsg_OCrypt(X0,X2),X1,tc_Message_Omsg))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f1126])).
% 24.41/4.36 fof(f1217,plain,(
% 24.41/4.36 ![X0,X1]: (~c_in(X0,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1))),tc_nat)|~c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|~c_in(X0,c_Message_OsymKeys,tc_nat)|c_in(hAPP(c_Message_Omsg_OKey,X0),c_Event_Oused(X1),tc_Message_Omsg))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f444])).
% 24.41/4.36 fof(f1237,plain,(
% 24.41/4.36 ![X0]: (c_Message_Oanalz(c_Message_Oanalz(X0))=c_Message_Oanalz(X0))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f457])).
% 24.41/4.36 fof(f1260,plain,(
% 24.41/4.36 ![X0,X1]: (c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)|~c_in(X0,X1,tc_Message_Omsg))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f471])).
% 24.41/4.36 fof(f1261,plain,(
% 24.41/4.36 ![X0,X1]: (c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)|~c_in(X0,X1,tc_Message_Omsg))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f472])).
% 24.41/4.36 fof(f1273,plain,(
% 24.41/4.36 ![X0]: (c_Message_Oanalz(c_Message_Oparts(X0))=c_Message_Oparts(X0))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f481])).
% 24.41/4.36 fof(f1321,plain,(
% 24.41/4.36 ![V_x,V_S]: ((![T_a]: c_in(V_x,V_S,T_a))|~hBOOL(hAPP(V_S,V_x)))),
% 24.41/4.36 inference(miniscoping,[status(thm)],[f513])).
% 24.41/4.36 fof(f1322,plain,(
% 24.41/4.36 ![X0,X1,X2]: (c_in(X0,X1,X2)|~hBOOL(hAPP(X1,X0)))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f1321])).
% 24.41/4.36 fof(f1323,plain,(
% 24.41/4.36 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~c_in(V_x,V_S,T_a)))),
% 24.41/4.36 inference(miniscoping,[status(thm)],[f514])).
% 24.41/4.36 fof(f1324,plain,(
% 24.41/4.36 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~c_in(X1,X0,X2))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f1323])).
% 24.41/4.36 fof(f1356,plain,(
% 24.41/4.36 ~c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f539])).
% 24.41/4.36 fof(f1357,plain,(
% 24.41/4.36 ~c_in(v_B,c_Event_Obad,tc_Message_Oagent)),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f540])).
% 24.41/4.36 fof(f1358,plain,(
% 24.41/4.36 c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f541])).
% 24.41/4.36 fof(f1359,plain,(
% 24.41/4.36 ~c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f542])).
% 24.41/4.36 fof(f1360,plain,(
% 24.41/4.36 c_in(v_KAB,c_Message_OsymKeys,tc_nat)),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f543])).
% 24.41/4.36 fof(f1368,plain,(
% 24.41/4.36 c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)),
% 24.41/4.36 inference(cnf_transformation,[status(thm)],[f551])).
% 24.41/4.36 fof(f1561,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB)))))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1324,f1368])).
% 24.41/4.36 fof(f1568,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_OsymKeys,v_KAB))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1324,f1360])).
% 24.41/4.36 fof(f1569,plain,(
% 24.41/4.36 hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs2))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1324,f1358])).
% 24.41/4.36 fof(f2227,plain,(
% 24.41/4.36 c_Message_OinvKey(v_KAB)=v_KAB),
% 24.41/4.36 inference(resolution,[status(thm)],[f912,f1360])).
% 24.41/4.36 fof(f2442,plain,(
% 24.41/4.36 ![X0]: (c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1561,f1322])).
% 24.41/4.36 fof(f2443,plain,(
% 24.41/4.36 ![X0]: (c_in(v_KAB,c_Message_OsymKeys,X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1568,f1322])).
% 24.41/4.36 fof(f2444,plain,(
% 24.41/4.36 ![X0]: (c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f1569,f1322])).
% 24.41/4.36 fof(f2447,plain,(
% 24.41/4.36 c_in(v_KAB,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg)),
% 24.41/4.36 inference(resolution,[status(thm)],[f2443,f1261])).
% 24.41/4.36 fof(f2448,plain,(
% 24.41/4.36 c_in(v_KAB,c_Message_Oparts(c_Message_OsymKeys),tc_Message_Omsg)),
% 24.41/4.36 inference(resolution,[status(thm)],[f2443,f1260])).
% 24.41/4.36 fof(f2451,plain,(
% 24.41/4.36 c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)),
% 24.41/4.36 inference(resolution,[status(thm)],[f2444,f1261])).
% 24.41/4.36 fof(f2452,plain,(
% 24.41/4.36 c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)),
% 24.41/4.36 inference(resolution,[status(thm)],[f2444,f1260])).
% 24.41/4.36 fof(f2457,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_Oanalz(c_Message_OsymKeys),v_KAB))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2447,f1324])).
% 24.41/4.36 fof(f2465,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_Oparts(c_Message_OsymKeys),v_KAB))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2448,f1324])).
% 24.41/4.36 fof(f2471,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),v_evs2))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2451,f1324])).
% 24.41/4.36 fof(f2479,plain,(
% 24.41/4.36 hBOOL(hAPP(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),v_evs2))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2452,f1324])).
% 24.41/4.36 fof(f3841,definition,(
% 24.41/4.36 sQ143_spl <=> (c_in(v_KAB,c_Message_OsymKeys,tc_nat))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f3843,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_OsymKeys,tc_nat)|sQ143_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f3841])).
% 24.41/4.36 fof(f3845,plain,(
% 24.41/4.36 $false|sQ143_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f3843,f2443])).
% 24.41/4.36 fof(f3846,plain,(
% 24.41/4.36 sQ143_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f3845])).
% 24.41/4.36 fof(f3852,definition,(
% 24.41/4.36 sQ145_spl <=> (c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f3854,plain,(
% 24.41/4.36 ~c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|sQ145_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f3852])).
% 24.41/4.36 fof(f3856,plain,(
% 24.41/4.36 $false|sQ145_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f3854,f2444])).
% 24.41/4.36 fof(f3857,plain,(
% 24.41/4.36 sQ145_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f3856])).
% 24.41/4.36 fof(f5504,definition,(
% 24.41/4.36 sQ209_spl <=> (c_in(v_B,c_Event_Obad,tc_Message_Oagent))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f5505,plain,(
% 24.41/4.36 c_in(v_B,c_Event_Obad,tc_Message_Oagent)|~sQ209_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f5504])).
% 24.41/4.36 fof(f8741,definition,(
% 24.41/4.36 sQ349_spl <=> (c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f8742,plain,(
% 24.41/4.36 c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)|~sQ349_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f8741])).
% 24.41/4.36 fof(f8746,plain,(
% 24.41/4.36 $false|~sQ349_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f8742,f1359])).
% 24.41/4.36 fof(f8747,plain,(
% 24.41/4.36 ~sQ349_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f8746])).
% 24.41/4.36 fof(f13189,definition,(
% 24.41/4.36 sQ531_spl <=> (c_in(v_KAB,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ531_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f13191,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg)|sQ531_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f13189])).
% 24.41/4.36 fof(f13200,plain,(
% 24.41/4.36 $false|sQ531_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f13191,f2447])).
% 24.41/4.36 fof(f13201,plain,(
% 24.41/4.36 sQ531_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f13200])).
% 24.41/4.36 fof(f13404,definition,(
% 24.41/4.36 sQ541_spl <=> (c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f13406,plain,(
% 24.41/4.36 ~c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)|sQ541_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f13404])).
% 24.41/4.36 fof(f13415,plain,(
% 24.41/4.36 $false|sQ541_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f13406,f2451])).
% 24.41/4.36 fof(f13416,plain,(
% 24.41/4.36 sQ541_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f13415])).
% 24.41/4.36 fof(f13420,plain,(
% 24.41/4.36 ![X0]: (c_in(v_KAB,c_Message_Oanalz(c_Message_OsymKeys),X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2457,f1322])).
% 24.41/4.36 fof(f13491,definition,(
% 24.41/4.36 sQ549_spl <=> (c_in(v_KAB,c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f13493,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_Oanalz(c_Message_Oanalz(c_Message_OsymKeys)),tc_Message_Omsg)|sQ549_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f13491])).
% 24.41/4.36 fof(f13516,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_Oanalz(c_Message_OsymKeys),tc_Message_Omsg)|sQ549_spl),
% 24.41/4.36 inference(forward_demodulation,[status(thm)],[f1237,f13493])).
% 24.41/4.36 fof(f13517,plain,(
% 24.41/4.36 $false|sQ549_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f13516,f13420])).
% 24.41/4.36 fof(f13518,plain,(
% 24.41/4.36 sQ549_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f13517])).
% 24.41/4.36 fof(f14143,definition,(
% 24.41/4.36 sQ572_spl <=> (c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent)))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f14145,plain,(
% 24.41/4.36 ~c_NS__Shared__Mirabelle_Ons__sharedp(c_List_Olist_ONil(tc_Event_Oevent))|sQ572_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f14143])).
% 24.41/4.36 fof(f14147,plain,(
% 24.41/4.36 $false|sQ572_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f14145,f656])).
% 24.41/4.36 fof(f14148,plain,(
% 24.41/4.36 sQ572_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f14147])).
% 24.41/4.36 fof(f14267,plain,(
% 24.41/4.36 ![X0]: (c_in(v_KAB,c_Message_Oparts(c_Message_OsymKeys),X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2465,f1322])).
% 24.41/4.36 fof(f14952,plain,(
% 24.41/4.36 c_in(c_Message_OinvKey(v_KAB),c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat)),
% 24.41/4.36 inference(resolution,[status(thm)],[f1127,f2442])).
% 24.41/4.36 fof(f14967,plain,(
% 24.41/4.36 c_in(v_KAB,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat)),
% 24.41/4.36 inference(forward_demodulation,[status(thm)],[f2227,f14952])).
% 24.41/4.36 fof(f15088,definition,(
% 24.41/4.36 sQ615_spl <=> (c_in(v_KAB,c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f15090,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_Oanalz(c_Message_Oparts(c_Message_OsymKeys)),tc_Message_Omsg)|sQ615_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f15088])).
% 24.41/4.36 fof(f15120,plain,(
% 24.41/4.36 ~c_in(v_KAB,c_Message_Oparts(c_Message_OsymKeys),tc_Message_Omsg)|sQ615_spl),
% 24.41/4.36 inference(forward_demodulation,[status(thm)],[f1273,f15090])).
% 24.41/4.36 fof(f15121,plain,(
% 24.41/4.36 $false|sQ615_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f15120,f14267])).
% 24.41/4.36 fof(f15122,plain,(
% 24.41/4.36 sQ615_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f15121])).
% 24.41/4.36 fof(f15128,plain,(
% 24.41/4.36 ![X0]: (c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),X0))),
% 24.41/4.36 inference(resolution,[status(thm)],[f2471,f1322])).
% 24.41/4.36 fof(f15203,definition,(
% 24.41/4.36 sQ625_spl <=> (c_in(v_evs2,c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f15205,plain,(
% 24.41/4.36 ~c_in(v_evs2,c_Message_Oanalz(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)|sQ625_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f15203])).
% 24.41/4.36 fof(f15228,plain,(
% 24.41/4.36 ~c_in(v_evs2,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)|sQ625_spl),
% 24.41/4.36 inference(forward_demodulation,[status(thm)],[f1237,f15205])).
% 24.41/4.36 fof(f15229,plain,(
% 24.41/4.36 $false|sQ625_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f15228,f15128])).
% 24.41/4.36 fof(f15230,plain,(
% 24.41/4.36 sQ625_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f15229])).
% 24.41/4.36 fof(f16172,definition,(
% 24.41/4.36 sQ630_spl <=> (c_in(v_A,c_Event_Obad,tc_Message_Oagent))),
% 24.41/4.36 introduced(definition,[new_symbols(definition,[sQ630_spl])],[split_symbol_definition])).
% 24.41/4.36 fof(f16173,plain,(
% 24.41/4.36 c_in(v_A,c_Event_Obad,tc_Message_Oagent)|~sQ630_spl),
% 24.41/4.36 inference(component_clause,[status(thm)],[f16172])).
% 24.41/4.36 fof(f16192,plain,(
% 24.41/4.36 $false|~sQ630_spl),
% 24.41/4.36 inference(forward_subsumption_resolution,[status(thm)],[f16173,f1356])).
% 24.41/4.36 fof(f16193,plain,(
% 24.41/4.36 ~sQ630_spl),
% 24.41/4.36 inference(contradiction_clause,[status(thm)],[f16192])).
% 24.41/4.36 fof(f16295,plain,(
% 24.41/4.36 ![X0]: (c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),X0))),
% 26.29/4.40 inference(resolution,[status(thm)],[f2479,f1322])).
% 26.29/4.40 fof(f17591,definition,(
% 26.29/4.40 sQ668_spl <=> (c_in(v_evs2,c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg))),
% 26.29/4.40 introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition])).
% 26.29/4.40 fof(f17593,plain,(
% 26.29/4.40 ~c_in(v_evs2,c_Message_Oanalz(c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared)),tc_Message_Omsg)|sQ668_spl),
% 26.29/4.40 inference(component_clause,[status(thm)],[f17591])).
% 26.29/4.40 fof(f17623,plain,(
% 26.29/4.40 ~c_in(v_evs2,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),tc_Message_Omsg)|sQ668_spl),
% 26.29/4.40 inference(forward_demodulation,[status(thm)],[f1273,f17593])).
% 26.29/4.40 fof(f17624,plain,(
% 26.29/4.40 $false|sQ668_spl),
% 26.29/4.40 inference(forward_subsumption_resolution,[status(thm)],[f17623,f16295])).
% 26.29/4.40 fof(f17625,plain,(
% 26.29/4.40 sQ668_spl),
% 26.29/4.40 inference(contradiction_clause,[status(thm)],[f17624])).
% 26.29/4.40 fof(f19243,definition,(
% 26.29/4.40 sQ683_spl <=> (c_lessequals(c_Message_Osynth(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),c_Set_Oinsert(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Osynth(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)))),
% 26.29/4.40 introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition])).
% 26.29/4.40 fof(f19245,plain,(
% 26.29/4.40 ~c_lessequals(c_Message_Osynth(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),c_Set_Oinsert(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_ONonce(v_NB))),c_Message_Osynth(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool))|sQ683_spl),
% 26.29/4.40 inference(component_clause,[status(thm)],[f19243])).
% 26.29/4.40 fof(f19282,plain,(
% 26.29/4.40 $false|sQ683_spl),
% 26.29/4.40 inference(forward_subsumption_resolution,[status(thm)],[f19245,f678])).
% 26.29/4.40 fof(f19283,plain,(
% 26.29/4.40 sQ683_spl),
% 26.29/4.40 inference(contradiction_clause,[status(thm)],[f19282])).
% 26.29/4.40 fof(f20564,plain,(
% 26.29/4.40 $false|~sQ209_spl),
% 26.29/4.40 inference(forward_subsumption_resolution,[status(thm)],[f5505,f1357])).
% 26.29/4.40 fof(f20565,plain,(
% 26.29/4.40 ~sQ209_spl),
% 26.29/4.40 inference(contradiction_clause,[status(thm)],[f20564])).
% 26.29/4.40 fof(f20566,plain,(
% 26.29/4.40 ~c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|~c_in(v_KAB,c_Message_OsymKeys,tc_nat)|c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)),
% 26.29/4.40 inference(resolution,[status(thm)],[f1217,f14967])).
% 26.29/4.40 fof(f20575,plain,(
% 26.29/4.40 ~sQ145_spl|~sQ143_spl|sQ349_spl),
% 26.29/4.40 inference(split_clause,[status(thm)],[f20566,f3852,f3841,f8741])).
% 26.29/4.40 fof(f20585,plain,(
% 26.29/4.40 $false),
% 26.29/4.40 inference(sat_refutation,[status(thm)],[f3846,f3857,f8747,f13201,f13416,f13518,f14148,f15122,f15230,f16193,f17625,f19283,f20565,f20575])).
% 26.29/4.40 % SZS output end CNFRefutation for theBenchmark.p
% 26.29/4.45 % Elapsed time: 3.468289 seconds
% 26.29/4.45 % CPU time: 26.977670 seconds
% 26.29/4.45 % Total memory used: 557.265 MB
% 26.29/4.45 % Net memory used: 535.822 MB
%------------------------------------------------------------------------------