%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV756-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 : 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:53:07 PM UTC 2026
% Result : Unsatisfiable 29.13s 4.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV756-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:23:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 29.13/4.21 % Refutation found
% 29.13/4.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 29.13/4.21 % SZS output start CNFRefutation for theBenchmark
% 29.13/4.21 fof(f248,axiom,(
% 29.13/4.21 (![V_K]: (( hAPP(c_Message_OinvKey,V_K) = V_K| ~ hBOOL(c_in(V_K,c_Message_OsymKeys,tc_nat)) ) ))),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f273,axiom,(
% 29.13/4.21 (![V_K,V_H,V_X]: (( hBOOL(c_in(hAPP(c_Message_OinvKey,V_K),c_Message_OkeysFor(V_H),tc_nat))| ~ hBOOL(c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)) ) ))),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f470,axiom,(
% 29.13/4.21 (![V_K,V_evs]: (( ~ hBOOL(c_in(V_K,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs))),tc_nat))| ~ hBOOL(c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))| ~ hBOOL(c_in(V_K,c_Message_OsymKeys,tc_nat))| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Event_Oused(V_evs),tc_Message_Omsg)) ) ))),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f527,axiom,(
% 29.13/4.21 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f528,axiom,(
% 29.13/4.21 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f549,negated_conjecture,(
% 29.13/4.21 hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) ),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f550,negated_conjecture,(
% 29.13/4.21 ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)) ),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f551,negated_conjecture,(
% 29.13/4.21 hBOOL(c_in(v_KAB,c_Message_OsymKeys,tc_nat)) ),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f559,negated_conjecture,(
% 29.13/4.21 hBOOL(c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) ),
% 29.13/4.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.13/4.21 fof(f931,plain,(
% 29.13/4.21 ![X0]: (hAPP(c_Message_OinvKey,X0)=X0|~hBOOL(c_in(X0,c_Message_OsymKeys,tc_nat)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f248])).
% 29.13/4.21 fof(f961,plain,(
% 29.13/4.21 ![V_K,V_H]: (hBOOL(c_in(hAPP(c_Message_OinvKey,V_K),c_Message_OkeysFor(V_H),tc_nat))|(![V_X]: ~hBOOL(c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg))))),
% 29.13/4.21 inference(miniscoping,[status(thm)],[f273])).
% 29.13/4.21 fof(f962,plain,(
% 29.13/4.21 ![X0,X1,X2]: (hBOOL(c_in(hAPP(c_Message_OinvKey,X0),c_Message_OkeysFor(X1),tc_nat))|~hBOOL(c_in(c_Message_Omsg_OCrypt(X0,X2),X1,tc_Message_Omsg)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f961])).
% 29.13/4.21 fof(f1249,plain,(
% 29.13/4.21 ![X0,X1]: (~hBOOL(c_in(X0,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1))),tc_nat))|~hBOOL(c_in(X1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))|~hBOOL(c_in(X0,c_Message_OsymKeys,tc_nat))|hBOOL(c_in(hAPP(c_Message_Omsg_OKey,X0),c_Event_Oused(X1),tc_Message_Omsg)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f470])).
% 29.13/4.21 fof(f1332,plain,(
% 29.13/4.21 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 29.13/4.21 inference(miniscoping,[status(thm)],[f527])).
% 29.13/4.21 fof(f1333,plain,(
% 29.13/4.21 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f1332])).
% 29.13/4.21 fof(f1334,plain,(
% 29.13/4.21 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 29.13/4.21 inference(miniscoping,[status(thm)],[f528])).
% 29.13/4.21 fof(f1335,plain,(
% 29.13/4.21 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f1334])).
% 29.13/4.21 fof(f1362,plain,(
% 29.13/4.21 hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f549])).
% 29.13/4.21 fof(f1363,plain,(
% 29.13/4.21 ~hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f550])).
% 29.13/4.21 fof(f1364,plain,(
% 29.13/4.21 hBOOL(c_in(v_KAB,c_Message_OsymKeys,tc_nat))),
% 29.13/4.21 inference(cnf_transformation,[status(thm)],[f551])).
% 29.13/4.21 fof(f1372,plain,(
% 29.13/4.21 hBOOL(c_in(c_Message_Omsg_OCrypt(v_KAB,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))),
% 30.02/4.27 inference(cnf_transformation,[status(thm)],[f559])).
% 30.02/4.27 fof(f1494,plain,(
% 30.02/4.27 hAPP(c_Message_OinvKey,v_KAB)=v_KAB),
% 30.02/4.27 inference(resolution,[status(thm)],[f931,f1364])).
% 30.02/4.27 fof(f1507,definition,(
% 30.02/4.27 sQ5_spl <=> (hBOOL(c_in(v_KAB,c_Message_OsymKeys,tc_nat)))),
% 30.02/4.27 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 30.02/4.27 fof(f1509,plain,(
% 30.02/4.27 ~hBOOL(c_in(v_KAB,c_Message_OsymKeys,tc_nat))|sQ5_spl),
% 30.02/4.27 inference(component_clause,[status(thm)],[f1507])).
% 30.02/4.27 fof(f3326,plain,(
% 30.02/4.27 hBOOL(hAPP(c_Message_OsymKeys,v_KAB))),
% 30.02/4.27 inference(resolution,[status(thm)],[f1335,f1364])).
% 30.02/4.27 fof(f3327,plain,(
% 30.02/4.27 hBOOL(hAPP(c_NS__Shared__Mirabelle_Ons__shared,v_evs2))),
% 30.02/4.27 inference(resolution,[status(thm)],[f1335,f1362])).
% 30.02/4.27 fof(f3335,plain,(
% 30.02/4.27 ![X0]: (hBOOL(c_in(v_KAB,c_Message_OsymKeys,X0)))),
% 30.02/4.27 inference(resolution,[status(thm)],[f3326,f1333])).
% 30.02/4.27 fof(f3344,plain,(
% 30.02/4.27 ![X0]: (hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,X0)))),
% 30.02/4.27 inference(resolution,[status(thm)],[f3327,f1333])).
% 30.02/4.27 fof(f4201,plain,(
% 30.02/4.27 $false|sQ5_spl),
% 30.02/4.27 inference(forward_subsumption_resolution,[status(thm)],[f1509,f3335])).
% 30.02/4.27 fof(f4202,plain,(
% 30.02/4.27 sQ5_spl),
% 30.02/4.27 inference(contradiction_clause,[status(thm)],[f4201])).
% 30.02/4.27 fof(f4705,definition,(
% 30.02/4.27 sQ87_spl <=> (hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))))),
% 30.02/4.27 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 30.02/4.27 fof(f4707,plain,(
% 30.02/4.27 ~hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))|sQ87_spl),
% 30.02/4.27 inference(component_clause,[status(thm)],[f4705])).
% 30.02/4.27 fof(f4709,plain,(
% 30.02/4.27 $false|sQ87_spl),
% 30.02/4.27 inference(forward_subsumption_resolution,[status(thm)],[f4707,f3344])).
% 30.02/4.27 fof(f4710,plain,(
% 30.02/4.27 sQ87_spl),
% 30.02/4.27 inference(contradiction_clause,[status(thm)],[f4709])).
% 30.02/4.27 fof(f15096,plain,(
% 30.02/4.27 hBOOL(c_in(hAPP(c_Message_OinvKey,v_KAB),c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat))),
% 30.02/4.27 inference(resolution,[status(thm)],[f962,f1372])).
% 30.02/4.27 fof(f15107,plain,(
% 30.02/4.27 hBOOL(c_in(v_KAB,c_Message_OkeysFor(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_nat))),
% 30.02/4.27 inference(forward_demodulation,[status(thm)],[f1494,f15096])).
% 30.02/4.27 fof(f33776,plain,(
% 30.02/4.27 ~hBOOL(c_in(v_evs2,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))|~hBOOL(c_in(v_KAB,c_Message_OsymKeys,tc_nat))|hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg))),
% 30.02/4.27 inference(resolution,[status(thm)],[f1249,f15107])).
% 30.02/4.27 fof(f33782,definition,(
% 30.02/4.27 sQ1394_spl <=> (hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)))),
% 30.02/4.27 introduced(definition,[new_symbols(definition,[sQ1394_spl])],[split_symbol_definition])).
% 30.02/4.27 fof(f33783,plain,(
% 30.02/4.27 hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg))|~sQ1394_spl),
% 30.02/4.27 inference(component_clause,[status(thm)],[f33782])).
% 30.02/4.27 fof(f33785,plain,(
% 30.02/4.27 ~sQ87_spl|~sQ5_spl|sQ1394_spl),
% 30.02/4.27 inference(split_clause,[status(thm)],[f33776,f4705,f1507,f33782])).
% 30.02/4.27 fof(f33791,plain,(
% 30.02/4.27 $false|~sQ1394_spl),
% 30.02/4.27 inference(forward_subsumption_resolution,[status(thm)],[f33783,f1363])).
% 30.02/4.27 fof(f33792,plain,(
% 30.02/4.27 ~sQ1394_spl),
% 30.02/4.27 inference(contradiction_clause,[status(thm)],[f33791])).
% 30.02/4.27 fof(f33793,plain,(
% 30.02/4.27 $false),
% 30.02/4.27 inference(sat_refutation,[status(thm)],[f4202,f4710,f33785,f33792])).
% 30.02/4.27 % SZS output end CNFRefutation for theBenchmark.p
% 3.05/4.32 % Elapsed time: 3.934749 seconds
% 3.05/4.32 % CPU time: 30.628009 seconds
% 3.05/4.32 % Total memory used: 629.639 MB
% 3.05/4.32 % Net memory used: 608.730 MB
%------------------------------------------------------------------------------