%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV794-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 : Tue Sep 29 01:26:26 PM UTC 2026
% Result : Unsatisfiable 66.79s 18.42s
% Output : Refutation 66.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 56 ( 28 unt; 1 def)
% Number of atoms : 119 ( 8 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 115 ( 52 ~; 62 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-4 aty)
% Number of functors : 28 ( 28 usr; 16 con; 0-4 aty)
% Number of variables : 78 ( 0 sgn 78 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f538,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,X1,X2,X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(X1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_B__trusts__NS3_0) ).
fof(f555,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( 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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_A__trusts__NS4__lemma_0) ).
fof(f563,axiom,
! [X2,X3,X0,X1,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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_B__Issues__A_0) ).
fof(f574,axiom,
! [X2,X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts_OSnd_0) ).
fof(f593,axiom,
! [X2,X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts_OBody_0) ).
fof(f598,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X0 = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3)))
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(X3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cert__A__form_1) ).
fof(f599,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3))) = X0
| ~ c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(X3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
inference(reorient_equations,[],[f598]) ).
fof(f638,negated_conjecture,
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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f639,negated_conjecture,
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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f640,negated_conjecture,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f641,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f642,negated_conjecture,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f643,negated_conjecture,
c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f644,negated_conjecture,
~ c_NS__Shared__Mirabelle_OIssues(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),v_evs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f879,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Event_Obad,tc_Message_Oagent)
| c_in(X3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X0),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X0,X1,X2,X3),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0)))))))),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X0))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(consistent_polarity_flipping,[],[f538]) ).
fof(f896,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ 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)) ),
inference(consistent_polarity_flipping,[],[f555]) ).
fof(f903,plain,
! [X2,X3,X0,X1,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) ),
inference(consistent_polarity_flipping,[],[f563]) ).
fof(f908,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(consistent_polarity_flipping,[],[f574]) ).
fof(f913,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_OCrypt(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(consistent_polarity_flipping,[],[f593]) ).
fof(f918,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X3,c_Event_Obad,tc_Message_Oagent)
| c_in(X4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X3))) = X0
| c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X3),c_Message_Omsg_OMPair(X5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
inference(consistent_polarity_flipping,[],[f599]) ).
fof(f930,plain,
~ 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),
inference(consistent_polarity_flipping,[],[f638]) ).
fof(f931,plain,
~ 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),
inference(consistent_polarity_flipping,[],[f639]) ).
fof(f932,plain,
c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(consistent_polarity_flipping,[],[f640]) ).
fof(f933,plain,
c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(consistent_polarity_flipping,[],[f641]) ).
fof(f934,plain,
c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(consistent_polarity_flipping,[],[f642]) ).
fof(f935,plain,
~ c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
inference(consistent_polarity_flipping,[],[f643]) ).
fof(f936,plain,
c_NS__Shared__Mirabelle_OIssues(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_NB)),v_evs),
inference(consistent_polarity_flipping,[],[f644]) ).
fof(f1318,plain,
~ c_in(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),
inference(resolution,[],[f913,f931]) ).
fof(f1359,plain,
~ c_in(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),
inference(resolution,[],[f1318,f908]) ).
fof(f6073,plain,
~ c_in(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),
inference(resolution,[],[f1359,f908]) ).
fof(f6096,plain,
~ c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(resolution,[],[f6073,f908]) ).
fof(f6998,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(X4,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(v_A))) = X3
| c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[],[f918,f933]) ).
fof(f7012,plain,
( 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) ),
inference(resolution,[],[f903,f936]) ).
fof(f7013,plain,
( ~ 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) ),
inference(forward_subsumption_resolution,[],[f7012,f935]) ).
fof(f7014,plain,
( ~ 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) ),
inference(forward_subsumption_resolution,[],[f7013,f934]) ).
fof(f7015,plain,
( ~ 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) ),
inference(forward_subsumption_resolution,[],[f7014,f933]) ).
fof(f7016,plain,
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),
inference(forward_subsumption_resolution,[],[f7015,f932]) ).
fof(f7213,plain,
! [X0,X1] :
( 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(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),X1))))),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)) ),
inference(resolution,[],[f896,f7016]) ).
fof(f7222,plain,
! [X0,X1] :
( 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(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),X1))))),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)) ),
inference(forward_subsumption_resolution,[],[f7213,f930]) ).
fof(f7225,plain,
! [X0,X1] :
( 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(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),X1))))),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)) ),
inference(forward_subsumption_resolution,[],[f7222,f932]) ).
fof(f7227,plain,
! [X0,X1] : 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(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),X1))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent),
inference(forward_subsumption_resolution,[],[f7225,f935]) ).
fof(f7308,plain,
! [X2,X0,X1] :
( ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,X1),c_Message_Omsg_OMPair(v_sko__NS__Shared__Mirabelle__XB__trusts__NS3__1(X1,v_B,X2,X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X1)))))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X0,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,X2),c_Message_Omsg_OAgent(X1))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg) ),
inference(resolution,[],[f879,f934]) ).
fof(f7886,plain,
( 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)))
| c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)) ),
inference(resolution,[],[f6998,f931]) ).
fof(f7903,plain,
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(forward_subsumption_resolution,[],[f7886,f935]) ).
fof(f390304,definition,
( spl0_814
<=> 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))) ),
introduced(definition,[new_symbols(definition,[spl0_814])],[avatar_definition]) ).
fof(f390306,plain,
( 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)))
| ~ spl0_814 ),
inference(avatar_component_clause,[],[f390304]) ).
fof(f450609,plain,
spl0_814,
inference(avatar_split_clause,[],[f7903,f390304]) ).
fof(f466690,plain,
( c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_in(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))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) ),
inference(resolution,[],[f7227,f7308]) ).
fof(f466714,plain,
c_in(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))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f466690,f935]) ).
fof(f466727,plain,
( c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)
| ~ spl0_814 ),
inference(forward_demodulation,[],[f466714,f390306]) ).
fof(f466735,plain,
( $false
| ~ spl0_814 ),
inference(forward_subsumption_resolution,[],[f466727,f6096]) ).
fof(f466736,plain,
~ spl0_814,
inference(avatar_contradiction_clause,[],[f466735]) ).
cnf(s6455,plain,
spl0_814,
inference(sat_conversion,[],[f450609]) ).
cnf(s6733,plain,
~ spl0_814,
inference(sat_conversion,[],[f466736]) ).
cnf(s6743,plain,
$false,
inference(rat,[],[s6455,s6733]) ).
fof(f466743,plain,
$false,
inference(avatar_sat_refutation,[],[s6743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV794-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 12:34:22 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.59/2.68 % (323008)Will run a generic schedule for satisfiability detection.
% 16.59/2.68 % (323017)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3602339928:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.59/2.68 % (323014)% WARNING: option uhcvi not known.
% 16.59/2.68 % (323015)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2338035287:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.59/2.68 % (323013)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3896818204_2999 on theBenchmark for (2999ds/0Mi)
% 16.59/2.68 % (323014)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3936987648:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.59/2.68 % (323016)dis+10_1_sil=32000:sp=arity:random_seed=2285815606:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.59/2.68 % (323018)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2181411082:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.59/2.68 % (323019)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1989063689:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.59/2.68 % (323017)Instruction limit reached!
% 16.59/2.68 % (323017)------------------------------
% 16.59/2.68 % (323017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.59/2.68 % (323017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/2.68 % (323017)CaDiCaL version: 2.1.3
% 16.59/2.68 % (323017)Termination reason: Instruction limit
% 16.59/2.68 % (323017)Termination phase: Saturation
% 16.59/2.68 % (323017)Time elapsed: 0.039 s
% 16.59/2.68 % (323017)Peak memory usage: 13 MB
% 16.59/2.68 % (323017)Instructions burned: 117 (million)
% 16.59/2.68 % (323027)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2778528662:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.59/2.68 % (323016)Instruction limit reached!
% 16.59/2.68 % (323016)------------------------------
% 16.59/2.68 % (323016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.59/2.68 % (323016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/2.68 % (323016)CaDiCaL version: 2.1.3
% 16.59/2.68 % (323016)Termination reason: Instruction limit
% 16.59/2.68 % (323016)Termination phase: Saturation
% 16.59/2.68 % (323016)Time elapsed: 0.066 s
% 16.59/2.68 % (323016)Peak memory usage: 12 MB
% 16.59/2.68 % (323016)Instructions burned: 103 (million)
% 16.59/2.68 % (323019)Instruction limit reached!
% 16.59/2.68 % (323019)------------------------------
% 16.59/2.68 % (323019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.59/2.68 % (323019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/2.68 % (323019)CaDiCaL version: 2.1.3
% 16.59/2.68 % (323019)Termination reason: Instruction limit
% 16.59/2.68 % (323019)Termination phase: Saturation
% 16.59/2.68 % (323019)Time elapsed: 0.078 s
% 16.59/2.68 % (323019)Peak memory usage: 12 MB
% 16.59/2.68 % (323019)Instructions burned: 159 (million)
% 16.59/2.68 % (323029)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2465532267:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.59/2.68 % (323018)Instruction limit reached!
% 16.59/2.68 % (323018)------------------------------
% 16.59/2.68 % (323018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.59/2.68 % (323018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/2.68 % (323018)CaDiCaL version: 2.1.3
% 16.59/2.68 % (323018)Termination reason: Instruction limit
% 16.59/2.68 % (323018)Termination phase: Saturation
% 16.59/2.68 % (323018)Time elapsed: 0.087 s
% 16.59/2.68 % (323018)Peak memory usage: 13 MB
% 16.59/2.68 % (323018)Instructions burned: 131 (million)
% 16.59/2.68 % (323030)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2135926432:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.59/2.68 % (323032)ott-21_1_sil=16000:fs=off:random_seed=2595374154:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.59/2.68 % TRYING [1]
% 16.59/2.68 % TRYING [2]
% 16.59/2.68 % TRYING [1]
% 16.59/2.68 % (323029)Instruction limit reached!
% 16.59/2.68 % (323029)------------------------------
% 16.59/2.68 % (323029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.59/2.68 % (323029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.59/2.68 % (323029)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323029)Termination reason: Instruction limit
% 44.13/6.51 % (323029)Termination phase: Saturation
% 44.13/6.51 % (323029)Time elapsed: 0.082 s
% 44.13/6.51 % (323029)Peak memory usage: 14 MB
% 44.13/6.51 % (323029)Instructions burned: 131 (million)
% 44.13/6.51 % TRYING [3]
% 44.13/6.51 % TRYING [2]
% 44.13/6.51 % (323032)Instruction limit reached!
% 44.13/6.51 % (323032)------------------------------
% 44.13/6.51 % (323032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323032)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323032)Termination reason: Instruction limit
% 44.13/6.51 % (323032)Termination phase: Saturation
% 44.13/6.51 % (323032)Time elapsed: 0.069 s
% 44.13/6.51 % (323032)Peak memory usage: 12 MB
% 44.13/6.51 % (323032)Instructions burned: 181 (million)
% 44.13/6.51 % (323035)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1764031215:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.13/6.51 % (323036)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2368144681:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.13/6.51 % (323027)Instruction limit reached!
% 44.13/6.51 % (323027)------------------------------
% 44.13/6.51 % (323027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323027)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323027)Termination reason: Instruction limit
% 44.13/6.51 % (323027)Termination phase: Finite model building constraint generation
% 44.13/6.51 % (323027)Time elapsed: 0.162 s
% 44.13/6.51 % (323027)Peak memory usage: 28 MB
% 44.13/6.51 % (323027)Instructions burned: 719 (million)
% 44.13/6.51 % (323039)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1591204126:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 44.13/6.51 % TRYING [3]
% 44.13/6.51 % TRYING [1]
% 44.13/6.51 % TRYING [2]
% 44.13/6.51 % (323035)Instruction limit reached!
% 44.13/6.51 % (323035)------------------------------
% 44.13/6.51 % (323035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323035)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323035)Termination reason: Instruction limit
% 44.13/6.51 % (323035)Termination phase: Saturation
% 44.13/6.51 % (323035)Time elapsed: 0.310 s
% 44.13/6.51 % (323035)Peak memory usage: 14 MB
% 44.13/6.51 % (323035)Instructions burned: 479 (million)
% 44.13/6.51 % (323030)Instruction limit reached!
% 44.13/6.51 % (323030)------------------------------
% 44.13/6.51 % (323030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323030)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323030)Termination reason: Instruction limit
% 44.13/6.51 % (323030)Termination phase: Saturation
% 44.13/6.51 % (323030)Time elapsed: 0.419 s
% 44.13/6.51 % (323030)Peak memory usage: 17 MB
% 44.13/6.51 % (323030)Instructions burned: 685 (million)
% 44.13/6.51 % (323041)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3801099328:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.13/6.51 % (323043)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3453027924:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 44.13/6.51 % (323039)Instruction limit reached!
% 44.13/6.51 % (323039)------------------------------
% 44.13/6.51 % (323039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323039)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323039)Termination reason: Instruction limit
% 44.13/6.51 % (323039)Termination phase: Saturation
% 44.13/6.51 % (323039)Time elapsed: 0.384 s
% 44.13/6.51 % (323039)Peak memory usage: 23 MB
% 44.13/6.51 % (323039)Instructions burned: 1181 (million)
% 44.13/6.51 % (323036)Instruction limit reached!
% 44.13/6.51 % (323036)------------------------------
% 44.13/6.51 % (323036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.13/6.51 % (323036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.13/6.51 % (323036)CaDiCaL version: 2.1.3
% 44.13/6.51 % (323036)Termination reason: Instruction limit
% 44.13/6.51 % (323036)Termination phase: Finite model building SAT solving
% 44.13/6.51 % (323036)Time elapsed: 0.409 s
% 107.48/15.46 % (323036)Peak memory usage: 29 MB
% 107.48/15.46 % (323036)Instructions burned: 865 (million)
% 107.48/15.46 % (323045)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2197047818:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 107.48/15.46 % (323046)fmb+10_1_sil=64000:random_seed=710419342:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 107.48/15.46 % TRYING [4]
% 107.48/15.46 % TRYING [1]
% 107.48/15.46 % TRYING [2]
% 107.48/15.46 % (323045)Instruction limit reached!
% 107.48/15.46 % (323045)------------------------------
% 107.48/15.46 % (323045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.48/15.46 % (323045)CaDiCaL version: 2.1.3
% 107.48/15.46 % (323045)Termination reason: Instruction limit
% 107.48/15.46 % (323045)Termination phase: Saturation
% 107.48/15.46 % (323045)Time elapsed: 0.267 s
% 107.48/15.46 % (323045)Peak memory usage: 20 MB
% 107.48/15.46 % (323045)Instructions burned: 880 (million)
% 107.48/15.46 % (323049)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1580153823:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 107.48/15.46 % (323041)Instruction limit reached!
% 107.48/15.46 % (323041)------------------------------
% 107.48/15.46 % (323041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.48/15.46 % (323041)CaDiCaL version: 2.1.3
% 107.48/15.46 % (323041)Termination reason: Instruction limit
% 107.48/15.46 % (323041)Termination phase: Finite model building constraint generation
% 107.48/15.46 % (323041)Time elapsed: 0.428 s
% 107.48/15.46 % (323041)Peak memory usage: 83 MB
% 107.48/15.46 % (323041)Instructions burned: 891 (million)
% 107.48/15.46 % (323043)Instruction limit reached!
% 107.48/15.46 % (323043)------------------------------
% 107.48/15.46 % (323043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.48/15.46 % (323043)CaDiCaL version: 2.1.3
% 107.48/15.46 % (323043)Termination reason: Instruction limit
% 107.48/15.46 % (323043)Termination phase: Saturation
% 107.48/15.46 % (323043)Time elapsed: 0.415 s
% 107.48/15.46 % (323043)Peak memory usage: 18 MB
% 107.48/15.46 % (323043)Instructions burned: 694 (million)
% 107.48/15.46 % (323051)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1475872115:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 107.48/15.46 % (323052)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3104543645:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 107.48/15.46 % TRYING [20]
% 107.48/15.46 % TRYING [3]
% 107.48/15.46 % TRYING [8]
% 107.48/15.46 % (323051)Instruction limit reached!
% 107.48/15.46 % (323051)------------------------------
% 107.48/15.46 % (323051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.48/15.46 % (323051)CaDiCaL version: 2.1.3
% 107.48/15.46 % (323051)Termination reason: Instruction limit
% 107.48/15.46 % (323051)Termination phase: Finite model building constraint generation
% 107.48/15.46 % (323051)Time elapsed: 0.362 s
% 107.48/15.46 % (323051)Peak memory usage: 56 MB
% 107.48/15.46 % (323051)Instructions burned: 921 (million)
% 107.48/15.46 % (323055)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=368024939:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 107.48/15.46 % (323055)Instruction limit reached!
% 107.48/15.46 % (323055)------------------------------
% 107.48/15.46 % (323055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.48/15.46 % (323055)CaDiCaL version: 2.1.3
% 107.48/15.46 % (323055)Termination reason: Instruction limit
% 107.48/15.46 % (323055)Termination phase: Saturation
% 107.48/15.46 % (323055)Time elapsed: 0.837 s
% 107.48/15.46 % (323055)Peak memory usage: 29 MB
% 107.48/15.46 % (323055)Instructions burned: 1472 (million)
% 107.48/15.46 % (323058)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4238329981:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 107.48/15.46 % (323058)Cannot represent all propositional literals internally
% 107.48/15.46 % (323058)Refutation not found, incomplete strategy
% 107.48/15.46 % (323058)------------------------------
% 107.48/15.46 % (323058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.48/15.46 % (323058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323058)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323058)Termination reason: Refutation not found, incomplete strategy
% 66.79/18.42 % (323058)Time elapsed: 0.171 s
% 66.79/18.42 % (323058)Peak memory usage: 17 MB
% 66.79/18.42 % (323058)Instructions burned: 342 (million)
% 66.79/18.42 % (323058)------------------------------
% 66.79/18.42 % (323058)------------------------------
% 66.79/18.42 % (323060)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=838599961:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi)
% 66.79/18.42 % TRYING [4]
% 66.79/18.42 % TRYING [5]
% 66.79/18.42 % (323049)Instruction limit reached!
% 66.79/18.42 % (323049)------------------------------
% 66.79/18.42 % (323049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323049)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323049)Termination reason: Instruction limit
% 66.79/18.42 % (323049)Termination phase: Finite model building constraint generation
% 66.79/18.42 % (323049)Time elapsed: 1.905 s
% 66.79/18.42 % (323049)Peak memory usage: 662 MB
% 66.79/18.42 % (323049)Instructions burned: 9518 (million)
% 66.79/18.42 % (323062)ott-2_1_sil=16000:newcnf=on:random_seed=1431821333:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 66.79/18.42 % (323060)Cannot represent all propositional literals internally
% 66.79/18.42 % (323060)Refutation not found, incomplete strategy
% 66.79/18.42 % (323060)------------------------------
% 66.79/18.42 % (323060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323060)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323060)Termination reason: Refutation not found, incomplete strategy
% 66.79/18.42 % (323060)Time elapsed: 0.575 s
% 66.79/18.42 % (323060)Peak memory usage: 23 MB
% 66.79/18.42 % (323060)Instructions burned: 1197 (million)
% 66.79/18.42 % (323060)------------------------------
% 66.79/18.42 % (323060)------------------------------
% 66.79/18.42 % (323064)ott+10_1_sil=32000:tgt=ground:random_seed=136582024:i=5114:av=off_2969 on theBenchmark for (2969ds/5114Mi)
% 66.79/18.42 % (323062)Instruction limit reached!
% 66.79/18.42 % (323062)------------------------------
% 66.79/18.42 % (323062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323062)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323062)Termination reason: Instruction limit
% 66.79/18.42 % (323062)Termination phase: Saturation
% 66.79/18.42 % (323062)Time elapsed: 0.251 s
% 66.79/18.42 % (323062)Peak memory usage: 16 MB
% 66.79/18.42 % (323062)Instructions burned: 872 (million)
% 66.79/18.42 % (323066)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1567220072:i=54282_2968 on theBenchmark for (2968ds/54282Mi)
% 66.79/18.42 % TRYING [1]
% 66.79/18.42 % TRYING [2]
% 66.79/18.42 % TRYING [3]
% 66.79/18.42 % TRYING [4]
% 66.79/18.42 % (323052)Instruction limit reached!
% 66.79/18.42 % (323052)------------------------------
% 66.79/18.42 % (323052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323052)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323052)Termination reason: Instruction limit
% 66.79/18.42 % (323052)Termination phase: Saturation
% 66.79/18.42 % (323052)Time elapsed: 2.916 s
% 66.79/18.42 % (323052)Peak memory usage: 45 MB
% 66.79/18.42 % (323052)Instructions burned: 5132 (million)
% 66.79/18.42 % (323068)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2208760761:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 66.79/18.42 % TRYING [5]
% 66.79/18.42 % (323068)Instruction limit reached!
% 66.79/18.42 % (323068)------------------------------
% 66.79/18.42 % (323068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323068)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323068)Termination reason: Instruction limit
% 66.79/18.42 % (323068)Termination phase: Saturation
% 66.79/18.42 % (323068)Time elapsed: 2.076 s
% 66.79/18.42 % (323068)Peak memory usage: 45 MB
% 66.79/18.42 % (323068)Instructions burned: 3512 (million)
% 66.79/18.42 % (323070)dis+21_1_sil=32000:sas=cadical:random_seed=4179303200:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 66.79/18.42 % (323064)Instruction limit reached!
% 66.79/18.42 % (323064)------------------------------
% 66.79/18.42 % (323064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323064)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323064)Termination reason: Instruction limit
% 66.79/18.42 % (323064)Termination phase: Saturation
% 66.79/18.42 % (323064)Time elapsed: 3.218 s
% 66.79/18.42 % (323064)Peak memory usage: 52 MB
% 66.79/18.42 % (323064)Instructions burned: 5114 (million)
% 66.79/18.42 % (323072)ott+11_1_sil=16000:gs=on:random_seed=2733168302:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 66.79/18.42 % (323072)Instruction limit reached!
% 66.79/18.42 % (323072)------------------------------
% 66.79/18.42 % (323072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323072)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323072)Termination reason: Instruction limit
% 66.79/18.42 % (323072)Termination phase: Saturation
% 66.79/18.42 % (323072)Time elapsed: 1.266 s
% 66.79/18.42 % (323072)Peak memory usage: 25 MB
% 66.79/18.42 % (323072)Instructions burned: 2251 (million)
% 66.79/18.42 % (323074)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2806026566:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 66.79/18.42 % (323070)Instruction limit reached!
% 66.79/18.42 % (323070)------------------------------
% 66.79/18.42 % (323070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323070)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323070)Termination reason: Instruction limit
% 66.79/18.42 % (323070)Termination phase: Saturation
% 66.79/18.42 % (323070)Time elapsed: 2.229 s
% 66.79/18.42 % (323070)Peak memory usage: 39 MB
% 66.79/18.42 % (323070)Instructions burned: 3774 (million)
% 66.79/18.42 % (323076)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3412878518:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 66.79/18.42 % TRYING [7]
% 66.79/18.42 % TRYING [6]
% 66.79/18.42 % TRYING [5]
% 66.79/18.42 % (323046)Instruction limit reached!
% 66.79/18.42 % (323046)------------------------------
% 66.79/18.42 % (323046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323046)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323046)Termination reason: Instruction limit
% 66.79/18.42 % (323046)Termination phase: Finite model building constraint generation
% 66.79/18.42 % (323046)Time elapsed: 8.799 s
% 66.79/18.42 % (323046)Peak memory usage: 275 MB
% 66.79/18.42 % (323046)Instructions burned: 22064 (million)
% 66.79/18.42 % (323078)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3767364181:i=29340_2904 on theBenchmark for (2904ds/29340Mi)
% 66.79/18.42 % (323076)Instruction limit reached!
% 66.79/18.42 % (323076)------------------------------
% 66.79/18.42 % (323076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323076)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323076)Termination reason: Instruction limit
% 66.79/18.42 % (323076)Termination phase: Saturation
% 66.79/18.42 % (323076)Time elapsed: 2.122 s
% 66.79/18.42 % (323076)Peak memory usage: 42 MB
% 66.79/18.42 % (323076)Instructions burned: 4593 (million)
% 66.79/18.42 % (323080)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3977728257:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 66.79/18.42 % TRYING [6]
% 66.79/18.42 % (323080)Instruction limit reached!
% 66.79/18.42 % (323080)------------------------------
% 66.79/18.42 % (323080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323080)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323080)Termination reason: Instruction limit
% 66.79/18.42 % (323080)Termination phase: Saturation
% 66.79/18.42 % (323080)Time elapsed: 2.760 s
% 66.79/18.42 % (323080)Peak memory usage: 51 MB
% 66.79/18.42 % (323080)Instructions burned: 5213 (million)
% 66.79/18.42 % (323082)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2936605798:i=5497:nm=2_2867 on theBenchmark for (2867ds/5497Mi)
% 66.79/18.42 % TRYING [17]
% 66.79/18.42 % (323082)Instruction limit reached!
% 66.79/18.42 % (323082)------------------------------
% 66.79/18.42 % (323082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323082)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323082)Termination reason: Instruction limit
% 66.79/18.42 % (323082)Termination phase: Finite model building constraint generation
% 66.79/18.42 % (323082)Time elapsed: 1.976 s
% 66.79/18.42 % (323082)Peak memory usage: 364 MB
% 66.79/18.42 % (323082)Instructions burned: 5498 (million)
% 66.79/18.42 % (323084)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2556424446:fmbsr=2:i=46332_2847 on theBenchmark for (2847ds/46332Mi)
% 66.79/18.42 % (323066)Instruction limit reached!
% 66.79/18.42 % (323066)------------------------------
% 66.79/18.42 % (323066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.42 % (323066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.42 % (323066)CaDiCaL version: 2.1.3
% 66.79/18.42 % (323066)Termination reason: Instruction limit
% 66.79/18.42 % (323066)Termination phase: Finite model building constraint generation
% 66.79/18.42 % (323066)Time elapsed: 12.164 s
% 66.79/18.42 % (323066)Peak memory usage: 1979 MB
% 66.79/18.42 % (323066)Instructions burned: 54284 (million)
% 66.79/18.42 % TRYING [15]
% 66.79/18.42 % (323086)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3426621893:i=14071_2845 on theBenchmark for (2845ds/14071Mi)
% 66.79/18.42 % TRYING [12]
% 66.79/18.42 % (323014) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-323008-323014"...
% 66.79/18.42 % (323014)...printing done.
% 66.79/18.42 % (323014)Refutation found. Thanks to Tanya!
% 66.79/18.42 % SZS status Unsatisfiable for theBenchmark
% 66.79/18.42 % SZS output start Proof for theBenchmark
% See solution above
% 66.79/18.43 % (323014)------------------------------
% 66.79/18.43 % (323014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.79/18.43 % (323014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.79/18.43 % (323014)CaDiCaL version: 2.1.3
% 66.79/18.43 % (323014)Termination reason: Refutation
% 66.79/18.43 % (323014)Time elapsed: 17.852 s
% 66.79/18.43 % (323014)Peak memory usage: 179 MB
% 66.79/18.43 % (323014)Instructions burned: 30879 (million)
% 66.79/18.43 % (323008)Success in time 18.198 s
% 66.79/18.43 % Vampire exiting
%------------------------------------------------------------------------------