%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV794-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:10 PM UTC 2026
% Result : Unsatisfiable 13.64s 12.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV794-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/10.62 % Computer : n010.cluster.edu
% 0.12/10.62 % Model : x86_64 x86_64
% 0.12/10.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.62 % Memory : 8046.5625MB
% 0.12/10.62 % OS : Linux 6.8.0-71-generic
% 0.12/10.62 % CPULimit : 300
% 0.12/10.62 % WCLimit : 300
% 0.12/10.62 % DateTime : Mon Sep 21 09:26:09 UTC 2026
% 0.12/10.62 % CPUTime :
% 0.12/10.66 % Drodi V4.1.1
% 13.64/12.51 % Refutation found
% 13.64/12.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 13.64/12.51 % SZS output start CNFRefutation for theBenchmark
% 13.64/12.51 fof(f477,axiom,(
% 13.64/12.51 (![V_B,V_A,V_K,V_NB,V_evs,V_NA,V_X]: (( c_in(c_Event_Oevent_OSays(V_B,V_A,c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_NB))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| ~ c_in(c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,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_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ) ))),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f478,axiom,(
% 13.64/12.51 (![V_A,V_NA,V_B,V_K,V_X,V_evs]: (( c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,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_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))| c_in(V_A,c_Event_Obad,tc_Message_Oagent)| ~ 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) ) ))),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f484,axiom,(
% 13.64/12.51 (![V_B,V_A,V_K,V_Nb,V_evs]: (( c_NS__Shared__Mirabelle_OIssues(V_B,V_A,c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_Nb)),V_evs)| ~ c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))| c_in(V_B,c_Event_Obad,tc_Message_Oagent)| c_in(V_A,c_Event_Obad,tc_Message_Oagent)| c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)| ~ c_in(c_Event_Oevent_OSays(V_B,V_A,c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_Nb))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent) ) ))),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f543,negated_conjecture,(
% 13.64/12.51 c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f544,negated_conjecture,(
% 13.64/12.51 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) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f545,negated_conjecture,(
% 13.64/12.51 ~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f546,negated_conjecture,(
% 13.64/12.51 ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f547,negated_conjecture,(
% 13.64/12.51 ~ c_in(v_B,c_Event_Obad,tc_Message_Oagent) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f548,negated_conjecture,(
% 13.64/12.51 c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f549,negated_conjecture,(
% 13.64/12.51 ~ c_NS__Shared__Mirabelle_OIssues(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),v_evs) ),
% 13.64/12.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.64/12.51 fof(f1249,plain,(
% 13.64/12.51 ![V_evs]: ((![V_K]: ((![V_B,V_A]: ((![V_NB]: (c_in(c_Event_Oevent_OSays(V_B,V_A,c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_NB))),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Message_Omsg_OCrypt(V_K,c_Message_Omsg_ONonce(V_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)))|(![V_NA,V_X]: ~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,V_A,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_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent))))|c_in(hAPP(c_Message_Omsg_OKey,V_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg)))|~c_in(V_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 13.64/12.51 inference(miniscoping,[status(thm)],[f477])).
% 13.64/12.51 fof(f1250,plain,(
% 13.64/12.51 ![X0,X1,X2,X3,X4,X5,X6]: (c_in(c_Event_Oevent_OSays(X0,X1,c_Message_Omsg_OCrypt(X2,c_Message_Omsg_ONonce(X3))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Message_Omsg_OCrypt(X2,c_Message_Omsg_ONonce(X3)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)|~c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X6))))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent)|c_in(hAPP(c_Message_Omsg_OKey,X2),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)|~c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f1249])).
% 13.64/12.51 fof(f1251,plain,(
% 13.64/12.51 ![X0,X1,X2,X3,X4,X5]: (c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,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_List_Oset(X5,tc_Event_Oevent),tc_Event_Oevent)|~c_in(X5,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(X0,c_Event_Obad,tc_Message_Oagent)|~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))),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f478])).
% 13.64/12.51 fof(f1259,plain,(
% 13.64/12.51 ![X0,X1,X2,X3,X4]: (c_NS__Shared__Mirabelle_OIssues(X0,X1,c_Message_Omsg_OCrypt(X2,c_Message_Omsg_ONonce(X3)),X4)|~c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(X0,c_Event_Obad,tc_Message_Oagent)|c_in(X1,c_Event_Obad,tc_Message_Oagent)|c_in(hAPP(c_Message_Omsg_OKey,X2),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)|~c_in(c_Event_Oevent_OSays(X0,X1,c_Message_Omsg_OCrypt(X2,c_Message_Omsg_ONonce(X3))),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent))),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f484])).
% 13.64/12.51 fof(f1336,plain,(
% 13.64/12.51 c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f543])).
% 13.64/12.51 fof(f1337,plain,(
% 13.64/12.51 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)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f544])).
% 13.64/12.51 fof(f1338,plain,(
% 13.64/12.51 ~c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f545])).
% 13.64/12.51 fof(f1339,plain,(
% 13.64/12.51 ~c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f546])).
% 13.64/12.51 fof(f1340,plain,(
% 13.64/12.51 ~c_in(v_B,c_Event_Obad,tc_Message_Oagent)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f547])).
% 13.64/12.51 fof(f1341,plain,(
% 13.64/12.51 c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f548])).
% 13.64/12.51 fof(f1342,plain,(
% 13.64/12.51 ~c_NS__Shared__Mirabelle_OIssues(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),v_evs)),
% 13.64/12.51 inference(cnf_transformation,[status(thm)],[f549])).
% 13.64/12.51 fof(f1667,plain,(
% 13.64/12.51 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,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_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)|~c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 13.64/12.51 inference(resolution,[status(thm)],[f1337,f1251])).
% 13.64/12.51 fof(f1671,plain,(
% 13.64/12.51 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,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_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)|c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 13.64/12.51 inference(forward_subsumption_resolution,[status(thm)],[f1667,f1341])).
% 13.64/12.51 fof(f1840,plain,(
% 13.64/12.51 c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,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_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)),
% 13.64/12.51 inference(forward_subsumption_resolution,[status(thm)],[f1671,f1339])).
% 13.64/12.51 fof(f1841,plain,(
% 13.64/12.51 ![X0]: (c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)|c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)|~c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 13.64/12.51 inference(resolution,[status(thm)],[f1840,f1250])).
% 13.64/12.51 fof(f1844,plain,(
% 13.64/12.51 ![X0]: (c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)|~c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))),
% 13.64/12.51 inference(forward_subsumption_resolution,[status(thm)],[f1841,f1338])).
% 13.64/12.51 fof(f2169,plain,(
% 13.64/12.51 ![X0]: (c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)|~c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg))),
% 13.64/12.51 inference(forward_subsumption_resolution,[status(thm)],[f1844,f1341])).
% 13.64/12.51 fof(f2170,plain,(
% 13.64/12.51 c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent)),
% 13.64/12.51 inference(resolution,[status(thm)],[f2169,f1336])).
% 13.64/12.51 fof(f3548,plain,(
% 13.64/12.51 c_NS__Shared__Mirabelle_OIssues(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),v_evs)|~c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(v_B,c_Event_Obad,tc_Message_Oagent)|c_in(v_A,c_Event_Obad,tc_Message_Oagent)|c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
% 13.64/12.51 inference(resolution,[status(thm)],[f2170,f1259])).
% 13.64/12.51 fof(f3549,plain,(
% 13.64/12.51 ~c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))|c_in(v_B,c_Event_Obad,tc_Message_Oagent)|c_in(v_A,c_Event_Obad,tc_Message_Oagent)|c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
% 13.64/12.51 inference(forward_subsumption_resolution,[status(thm)],[f3548,f1342])).
% 13.64/12.51 fof(f6236,plain,(
% 13.64/12.51 c_in(v_B,c_Event_Obad,tc_Message_Oagent)|c_in(v_A,c_Event_Obad,tc_Message_Oagent)|c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
% 14.11/12.54 inference(forward_subsumption_resolution,[status(thm)],[f3549,f1341])).
% 14.11/12.54 fof(f6237,plain,(
% 14.11/12.54 c_in(v_B,c_Event_Obad,tc_Message_Oagent)|c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 14.11/12.54 inference(resolution,[status(thm)],[f6236,f1338])).
% 14.11/12.54 fof(f6239,plain,(
% 14.11/12.54 c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
% 14.11/12.54 inference(forward_subsumption_resolution,[status(thm)],[f6237,f1340])).
% 14.11/12.54 fof(f6850,plain,(
% 14.11/12.54 $false),
% 14.11/12.54 inference(forward_subsumption_resolution,[status(thm)],[f6239,f1339])).
% 14.11/12.54 % SZS output end CNFRefutation for theBenchmark.p
% 14.11/12.57 % Elapsed time: 1.939423 seconds
% 14.11/12.57 % CPU time: 14.900053 seconds
% 14.11/12.57 % Total memory used: 443.533 MB
% 14.11/12.57 % Net memory used: 431.056 MB
%------------------------------------------------------------------------------